Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17 rests on unproved material (inherited)
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.

Rests on 3 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are Cohen's first model: an infinite Dedekind-finite set of reals, Sierpiński 1947: the generalised continuum hypothesis implies the Axiom of Choice and The continuum hypothesis and its generalisation are independent of ZFC. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

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.

[L1]

The covariant power-set monad has singleton unit and union multiplication (Singleton and union define the covariant power-set monad), while an algebra map a:TXX satisfies aηX=1X and aT(a)=aμX, and a homomorphism f satisfies fa=bT(f) (Algebra and algebra homomorphism for a monad).

[L2]

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).

[L3]

Antisymmetry is the condition that xy and yx imply x=y (Partial order and partially ordered set).

Proof

technique · direct
1.1

Given an algebra a, define xy when a({x,y})=y. The singleton law gives reflexivity; symmetry of the set {x,y} gives antisymmetry; and the flattening law makes the induced binary join associative, from which transitivity follows. Thus this is a partial order.

L1L3
2.1

For every AX, put supA=a(A). Applying the flattening law to families formed from A, its singleton subsets, and an arbitrary common upper bound proves respectively that every member of A lies below a(A) and that a(A) lies below every upper bound; this includes A=. The algebra-homomorphism equation fa=bP(f) says exactly that f(supA)=supf[A].

L1L2step 1.1
3.1

Conversely, on a poset with all small suprema define a(A)=supA. Singleton suprema give the unit law, and sup(A)=sup{supA:AA} gives the multiplication law. A map satisfies the algebra-homomorphism equation exactly when it preserves these suprema.

L1L2step 2.1

Depends on

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