Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
A preorder is a category with at most one morphism between any two objects, and its functors are exactly monotone maps
Statement
A preorder determines a category with at most one morphism between any two objects, and functors between such categories are exactly monotone maps.
Facts & Assumptions
Given: Preorders and .
A preorder is reflexive and transitive, and a monotone map preserves its relation (Preorder and monotone map).
Category identities and composition have the meanings of Category, object, morphism, domain, codomain, identity, composition, and hom-collection. In this proposition, a functor is an assignment on objects and arrows that preserves identities and composition.
Proof
Make the elements of objects and put one morphism when , and none otherwise; reflexivity supplies identities and transitivity supplies the unique possible composites, so [L1] gives a category.
A function extends to a functor exactly when guarantees a target morphism , which is exactly .
Thus the functors between the associated categories are precisely the monotone maps, with no extra arrow choices because every relevant hom-collection has at most one member.
Depends on
Used by
- A limit in a full subcategory need not be the ambient limit Counterexample
- A monotone functor between poset categories preserves every monomorphism but need not preserve pullbacks Counterexample
- A two-object indiscrete preorder is equivalent but not isomorphic to its one-object poset reflection Counterexample
- Galois connection between preorders Definition
- A left Kan extension along a full subcategory inclusion of preorders Example
- A left Kan extension along the inclusion of the rationals in the reals Example
- A representable presheaf on a poset is the indicator of a principal down-set Example
- Ceiling ⊣ inclusion ⊣ floor: an adjoint triple between (ℝ,≤) and (ℤ,≤) Example
- In a poset regarded as a category, products are infima, coproducts are suprema, and equalizers are automatic Example
- The adjoint functor theorem for ordered sets Example
- Every equivalence of categories is an isomorphism of categories False statement
- FALSE: every functor preserves the ends that exist in its domain False statement
- A poset category is complete exactly when every small family has an infimum, and cocomplete exactly when every small family has a supremum Proposition
- In a poset adjunction the triangle identities are automatic Proposition
- A cartesian closed preorder has relative implications Theorem
- A poset with finite meets is a strict monoidal category Theorem
- Assuming Choice, a small category with products or coproducts indexed by the cardinality of its morphism set is a preorder Theorem
- On a preorder the monads are exactly the monotone extensive maps with T(Tp) below Tp; on a poset they are exactly the closure operators Theorem
Dependency tree · two levels
5 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Emily Riehl, Category Theory in Context, Chapter 1 (standard reference, not scraped)