How 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.
Algebras for the covariant power-set monad are posets with all small suprema and their morphisms preserve every small supremum
Statement
The Eilenberg–Moore category of the covariant power-set monad is isomorphic to the category of posets admitting every small supremum and maps preserving every small supremum.
Facts & Assumptions
Given: The covariant power-set monad with singleton unit and union multiplication.
The covariant power-set monad has singleton unit and union multiplication (Singleton and union define the covariant power-set monad), while an algebra map satisfies and , and a homomorphism satisfies (Algebra and algebra homomorphism for a monad).
A poset has all small suprema exactly when every set of its elements has a least upper bound (A poset category is complete exactly when every small family has an infimum, and cocomplete exactly when every small family has a supremum).
Antisymmetry is the condition that and imply (Partial order and partially ordered set).
Proof
Given an algebra , define when . The singleton law gives reflexivity; symmetry of the set gives antisymmetry; and the flattening law makes the induced binary join associative, from which transitivity follows. Thus this is a partial order.
For every , put . Applying the flattening law to families formed from , its singleton subsets, and an arbitrary common upper bound proves respectively that every member of lies below and that lies below every upper bound; this includes . The algebra-homomorphism equation says exactly that .
Conversely, on a poset with all small suprema define . Singleton suprema give the unit law, and gives the multiplication law. A map satisfies the algebra-homomorphism equation exactly when it preserves these suprema.
Depends on
- Singleton and union define the covariant power-set monad
- Eilenberg–Moore category of a monad
- Algebra and algebra homomorphism for a monad
- Preorder and monotone map
- A poset category is complete exactly when every small family has an infimum, and cocomplete exactly when every small family has a supremum
- Partial order and partially ordered set
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 38 results over 14 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- S. Mac Lane, Categories for the Working Mathematician, 2nd ed., Exercise VI.2.2 (standard reference, not scraped)