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.
Preorder and monotone map
Definition
A preorder on a set is a relation that is reflexive and transitive. Unlike a partial order (Partial order and partially ordered set), it need not be antisymmetric.
A map between preorders is monotone when implies . Every partial order is a preorder, and the definition of monotone map agrees with the usual one for partially ordered sets.
Depends on
Used by
- Algebras for a preorder monad are exactly its fixed objects up to preorder equivalence; on a poset they are its fixed points Corollary
- An abelian category that is a preorder is trivial Corollary
- On a preorder the comonads are exactly the monotone contractive maps with Gp below G(Gp); on a poset they are exactly the interior operators Corollary
- Galois connection between preorders Definition
- A representable presheaf on a poset is the indicator of a principal down-set Example
- Ceiling ⊣ inclusion ⊣ floor: an adjoint triple between (ℝ,≤) and (ℤ,≤) Example
- FALSE: every functor preserves the ends that exist in its domain False statement
- A preorder is a category with at most one morphism between any two objects, and its functors are exactly monotone maps Proposition
- A category enriched in the two-element lattice is a preordered set Theorem
- Algebras for the covariant power-set monad are posets with all small suprema and their morphisms preserve every small supremum Theorem
- Assuming Choice, a small category with products or coproducts indexed by the cardinality of its morphism set is a preorder Theorem
- Enrichment in a preorder recovers a preorder, and enrichment in sets recovers a small ordinary category 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 · one level
1 result within one dependency step 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)