Alphabeta Math
Session-authored (Fable 5 assisted)
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.

36 results · all verified · 29 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 7 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Monadicity and Beck's Theorem

1 · Prerequisites

2 · Summary

Monads and their Eilenberg–Moore algebras provide the comparison functor attached to a right adjoint, while Monadic and strictly monadic functors distinguishes equivalences from isomorphisms and Conservative functor defines reflection of isomorphisms. Coequalizers, creation of colimits, filtered colimits, compactness, Hausdorff separation, filters, and the ultrafilter monad supply the categorical and topological language used in the development.

Split and U-split coequalizers lead to the ordinary and strict forms of Beck's theorem and to the reflexive criterion. Applications establish monadicity for familiar algebraic categories, the contravariant power-set functor, finitary algebra categories, and compact Hausdorff spaces. The compact Hausdorff result follows by constructing mutually inverse topological and ultrafilter-algebra structures, with the ultrafilter lemma and dependent-choice costs stated where they enter.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Absolute colimits

Definition

A colimit of a diagram in a category C is absolute when every functor with domain C preserves that colimit (Limits and colimits as terminal cones and initial cocones, with existence and uniqueness in their universal properties, Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors). Equivalently, a colimit is absolute when every functor preserves it.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Split coequalizer diagrams

Definition

A split coequalizer diagram consists of morphisms

xfgyhz,t:yx,s:zy

such that

hf=hg,hs=1z,gt=1y,ft=sh.

Thus a split coequalizer diagram has maps f,g:xy, h:yz, t:yx, and s:zy satisfying hf=hg, hs=1z, gt=1y, and ft=sh. The morphism h is called a split coequalizer of f and g (Equalizers and coequalizers as limits and colimits of a parallel pair).

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Every split coequalizer is a coequalizer and an absolute colimit

Statement

Every split coequalizer diagram (Split coequalizer diagrams) is a coequalizer diagram (Equalizers and coequalizers as limits and colimits of a parallel pair), and its coequalizer is an absolute colimit (Absolute colimits).

Facts & Assumptions

Given: A split coequalizer diagram xf,gyhz with splitting maps t:yx and s:zy.

[L1]

A split coequalizer diagram has maps f,g:xy, h:yz, t:yx, and s:zy satisfying hf=hg, hs=1z, gt=1y, and ft=sh (Split coequalizer diagrams).

[L2]

A colimit is absolute when every functor preserves it (Absolute colimits).

Proof

technique · direct
1.1

Let k:yw satisfy kf=kg. Define u:=ks:zw. Then uh=ksh=kft=kgt=k, using ft=sh, the equality kf=kg, and gt=1y.

L1construct
1.2

Let H be any functor with the given category as domain. Functoriality sends the four equations in [L1] to HhHf=HhHg, HhHs=1Hz, HgHt=1Hy, and HfHt=HsHh, so the image diagram is again split.

L1given
2.1

If v:zw also satisfies vh=k, then v=vhs=ks=u because hs=1z. Thus h has the coequalizer universal property, including when f=g or h is an identity.

step 1.1L1algebra
3.1

Repeating steps 1.1 and 2.1 in the target of H shows that Hh is a coequalizer of Hf and Hg. Since H was arbitrary, every functor preserves this coequalizer, so it is absolute by [L2].

step 1.1step 2.1step 1.2L2
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Reflexive parallel pairs and reflexive coequalizers

Definition

A parallel pair f,g:AB is reflexive when it has a common section: there is a morphism r:BA such that

fr=gr=1B.

A reflexive coequalizer is a coequalizer (Equalizers and coequalizers as limits and colimits of a parallel pair) of a reflexive parallel pair.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

U-split pairs and ordinary or strict creation of their coequalizers

Definition

Let U:DC be a functor. A parallel pair f,g:dd in D is U-split when its image under U extends to a split coequalizer diagram in C (Split coequalizer diagrams).

The functor U creates coequalizers of U-split pairs when each chosen split coequalizer of Uf and Ug is isomorphic, as a coequalizer diagram, to the image under U of a coequalizer of f and g, and every lifted fork whose image is a coequalizer is itself a coequalizer. This is ordinary isomorphism-invariant creation in the sense of Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors.

The functor U strictly creates coequalizers of U-split pairs when every supplied splitting has a unique lift on the same apex and legs, and the lifted fork is a coequalizer. Strict creation therefore specifies the lifted object and structure on the nose, rather than only up to isomorphism.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Every algebra is the coequalizer of its canonical pair of free algebras

Statement

Let (T,η,μ) be a monad on C and let (A,a) be a T-algebra. In the Eilenberg–Moore category CT, the diagram

(T2A,μTA)T(a)μA(TA,μA)a(A,a)

is a coequalizer. Thus every T-algebra is the coequalizer in CT of the canonical pair of free algebras.

Facts & Assumptions

Given: A monad (T,η,μ) and a T-algebra (A,a) in the Eilenberg–Moore category (Monad on a category, Eilenberg–Moore category of a monad).

[L1]

A T-algebra is an object A with a morphism a:TAA satisfying aηA=1A and aT(a)=aμA; a morphism r:(A,a)(B,b) satisfies ra=bT(r) (Algebra and algebra homomorphism for a monad).

[L2]

The free T-algebra on A is (TA,μA), and T(f) is an algebra homomorphism between free algebras for every f (Free algebra for a monad).

[L3]

A coequalizer of f,g is a morphism coequalizing them through which every other coequalizing morphism factors uniquely (Equalizers and coequalizers as limits and colimits of a parallel pair).

Proof

technique · direct
1.1

By [L2], T(a):(T2A,μTA)(TA,μA) is an algebra homomorphism. The monad associativity equation says that μA:(T2A,μTA)(TA,μA) is also an algebra homomorphism.

L1L2algebra
2.1

The structure map a:(TA,μA)(A,a) is an algebra homomorphism by the algebra associativity law, and that same law gives aT(a)=aμA, so a coequalizes the canonical pair.

step 1.1L1
3.1

Let r:(TA,μA)(B,b) be an algebra homomorphism with rT(a)=rμA. Define rˉ:=rηA:AB. Naturality of η and the monad unit law give rˉa=rηAa=rT(a)ηTA=rμAηTA=r.

step 2.1L1construct
4.1

Since r is an algebra homomorphism, rμA=bT(r). Hence bT(rˉ)=bT(r)T(ηA)=rμAT(ηA)=r=rˉa, so rˉ is an algebra homomorphism.

step 3.1L1algebra
5.1

If c:(A,a)(B,b) satisfies ca=r, then c=caηA=rηA=rˉ by the algebra unit law. Therefore a has the universal property in [L3], including for initial or degenerate algebra objects, and is the claimed coequalizer.

step 3.1step 4.1L1L3
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The canonical algebra presentation is split in the base, but its canonical splittings need not be algebra homomorphisms

Statement

For every T-algebra (A,a), the underlying canonical presentation

T2AT(a)μATAaA

is a split coequalizer in C, with t=ηTA:TAT2A and s=ηA:ATA. These canonical splitting maps need not be algebra homomorphisms, so the presentation need not be split in CT.

Facts & Assumptions

Given: A monad (T,η,μ) and a T-algebra (A,a).

[L1]

Every T-algebra (A,a) is the coequalizer in CT of the canonical pair of free algebras T(a),μA:T2ATA (Every algebra is the coequalizer of its canonical pair of free algebras).

[L2]

A split coequalizer diagram has maps f,g:xy, h:yz, t:yx, and s:zy satisfying hf=hg, hs=1z, gt=1y, and ft=sh (Split coequalizer diagrams).

[L3]

The free-monoid monad inserts letters as one-letter words and flattens words of words by concatenation; its Eilenberg–Moore category is isomorphic over Set to the category of monoids (The free-monoid monad has monoids as its Eilenberg–Moore algebras).

Proof

technique · direct
1.1

The algebra law gives aT(a)=aμA and aηA=1A. The monad unit law gives μAηTA=1TA, while naturality of η gives T(a)ηTA=ηAa. These are exactly the four equations of [L2] for t=ηTA and s=ηA.

L1L2algebra
1.2

For the free-monoid monad, take the monoid M={1,e} with e2=e. On the two-letter word [e,e], the composite ηMa first multiplies and gives the one-letter word [e], whereas μMT(ηM) gives the two-letter word [e,e].

L3construct
2.1

Therefore the underlying canonical presentation is split in C.

step 1.1L2
2.2

The equality ηMa=μMT(ηM) is precisely the algebra-homomorphism equation for ηM:(M,a)(TM,μM), and step 1.2 shows it fails.

step 1.2L3algebra
2.3

For that same algebra no algebra section exists at all. Under the isomorphism over Set of [L3], an algebra map s:(M,a)(TM,μM) with as=1M is a monoid homomorphism σ from M to the free monoid on the set M whose composite with word evaluation is the identity. Concatenation adds word lengths, so w2=w forces w=0 and the empty word is the only idempotent of that free monoid; since e2=e in M, σ(e) is the empty word and evaluates to 1e. Hence the presentation of (M,a) is not split in CT.

step 1.2L3algebra
3.1

Thus the canonical splittings always exist in the base by step 2.1, the canonical ones need not lift to algebra homomorphisms by step 2.2, and by step 2.3 the presentation itself need not be split in CT. No failure is asserted for every monad or every algebra.

step 2.1step 2.2step 2.3
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The Eilenberg–Moore forgetful functor strictly creates coequalizers of UT-split pairs

Statement

For every monad T on C, the Eilenberg–Moore forgetful functor UT:CTC strictly creates coequalizers of UT-split pairs.

Facts & Assumptions

Given: Algebra homomorphisms f,g:(A,a)(B,b) and a supplied split coequalizer q:BC of their underlying pair in C.

[L1]

The functor U strictly creates coequalizers of U-split pairs when every supplied splitting has a unique lift on the same apex and legs, and the lifted fork is a coequalizer (U-split pairs and ordinary or strict creation of their coequalizers).

[L2]

Every split coequalizer is a coequalizer and an absolute colimit (Every split coequalizer is a coequalizer and an absolute colimit).

Proof

technique · direct
1.1

By [L2], q, Tq, and T2q are coequalizers of the corresponding images of f,g. In particular each is an epimorphism, since every coequalizer is epic by its uniqueness clause.

L2given
2.1

Because f and g are algebra homomorphisms, qb:TBC coequalizes Tf and Tg. The universal property of Tq gives a unique c:TCC satisfying cTq=qb.

step 1.1construct
3.1

After precomposition with the epimorphism q, the unit equation cηC=1C is the unit law for b. After precomposition with the epimorphism T2q, the associativity equation cT(c)=cμC is the associativity law for b. Hence (C,c) is a T-algebra.

step 1.1step 2.1algebra
4.1

The defining equation cTq=qb says exactly that q:(B,b)(C,c) is an algebra homomorphism.

step 2.1step 3.1algebra
5.1

If r:(B,b)(D,d) is an algebra homomorphism with rf=rg, [L2] gives a unique underlying u:CD with uq=r. Precomposing uc and dT(u) with the epimorphism Tq gives the same map, so u is an algebra homomorphism and is the unique algebraic factorization.

step 4.1L2
6.1

Any algebra structure c on the supplied apex for which q is an algebra homomorphism satisfies cTq=qb=cTq, so c=c because Tq is epic. Together with step 5.1 this is the unique on-the-nose lift required by [L1].

step 2.1step 5.1L1
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Supplied created canonical presentations give a quasi-inverse to the comparison functor

Statement

Let F:CD:U be an adjunction inducing the monad T=UF, and let K:DCT be its comparison functor. Suppose U creates coequalizers of U-split pairs and, for every T-algebra (A,a), a specific created coequalizer of its lifted canonical pair is supplied. Then these supplied coequalizers define a functor H:CTD and natural isomorphisms

KH1CT,HK1D.

Thus H is a quasi-inverse to K.

Facts & Assumptions

Given: An adjunction FU inducing T on the nose, with U creating coequalizers of U-split pairs.

[L1]

The comparison functor is K(d)=(Ud,Uεd) and K(h)=U(h) (The comparison functor to the Eilenberg–Moore category exists and is unique).

[L2]
[L3]

A parallel pair is U-split when its image under U extends to a split coequalizer diagram, and ordinary creation supplies and reflects the corresponding lifted coequalizer up to isomorphism (U-split pairs and ordinary or strict creation of their coequalizers).

[L4]

The Eilenberg–Moore forgetful functor strictly creates coequalizers of its split pairs (The Eilenberg–Moore forgetful functor strictly creates coequalizers of UT-split pairs).

[L5]

Every T-algebra is the coequalizer in CT of its canonical pair of free algebras (Every algebra is the coequalizer of its canonical pair of free algebras).

Proof

technique · direct
1.1

For a T-algebra (A,a), the pair F(TA)F(A) with arrows F(a) and εFA has under U the canonical pair T(a),μA:T2ATA. By [L2] and [L3] it is U-split.

L2L3
2.1

Let qA:F(A)H(A,a) be the created coequalizer supplied for (A,a). Its image is isomorphic to the canonical base coequalizer from step 1.1, and the universal property fixes the resulting comparisons.

step 1.1L3given
3.1

An algebra homomorphism r:(A,a)(B,b) carries the canonical pair for A to that for B. The two coequalizer universal properties therefore define a unique morphism H(r):H(A,a)H(B,b), and uniqueness proves preservation of identities and composition.

step 2.1construct
3.2

For dD, the counit fork F(TUd)F(Ud)εdd maps under U to the canonical split presentation of K(d). Creation reflects the lifted coequalizer, so comparison with qK(d) yields an isomorphism HK(d)d.

step 2.1L1L2
3.3

The underlying fork of K(qA) is a split coequalizer, transported from the canonical split fork along the isomorphism supplied by ordinary creation. Since K(qA) is a lift of that fork, [L4] makes it a coequalizer in CT. The map a:TAA is the other canonical algebra coequalizer by [L5], so their universal properties produce a unique isomorphism KH(A,a)(A,a).

step 2.1L1L2L4L5
4.1

The defining equations for the comparisons in steps 3.3 and 3.2 commute with every algebra homomorphism and every morphism of D. Uniqueness of maps out of the coequalizers therefore makes both families natural, proving the two displayed natural isomorphisms.

step 3.3step 3.2algebra
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Beck's monadicity theorem in data-supplied form

Statement

Let U:DC be a right adjoint.

  1. If U is monadic, then it creates coequalizers of U-split pairs.
  2. Conversely, suppose U creates coequalizers of U-split pairs and, for every algebra of the induced monad, a specific created coequalizer of its lifted canonical pair is supplied. Then U is monadic.

Here monadic means that the comparison functor is an equivalence, and creation is ordinary isomorphism-invariant creation, not strict creation. The supplied family in the converse is data; it is not manufactured by global choice.

Facts & Assumptions

Given: A right adjoint U:DC, a left adjoint F, the induced monad T=UF, and comparison functor K:DCT.

[L1]

The functor U is monadic when its comparison functor K is an equivalence of categories (Monadic and strictly monadic functors).

[L2]

The Eilenberg–Moore forgetful functor strictly creates coequalizers of UT-split pairs (The Eilenberg–Moore forgetful functor strictly creates coequalizers of UT-split pairs).

[L3]

If U creates coequalizers of U-split pairs and a created coequalizer is supplied for every lifted canonical algebra pair, those supplied presentations give a quasi-inverse to the comparison functor (Supplied created canonical presentations give a quasi-inverse to the comparison functor).

[L4]

An equivalence of categories preserves, reflects, and creates existing colimits in the ordinary isomorphism-invariant sense (Equivalences preserve, reflect, and create limits and colimits in the isomorphism-invariant sense).

Proof

technique · direct
1.1

For the forward direction, suppose U is monadic. Then K is an equivalence by [L1] and U=UTK. Transporting the strict-creation result [L2] across K by [L4] shows that U creates coequalizers of U-split pairs in the ordinary sense.

L1L2L4
1.2

For the converse, suppose U creates coequalizers of U-split pairs and the stated family of created canonical coequalizers is supplied. By [L3], those data define a quasi-inverse to K.

L3given
2.1

A functor with a quasi-inverse and the two natural isomorphisms is an equivalence, so K is an equivalence and U is monadic by [L1].

step 1.2L1
3.1

Step 1.1 proves the monadic-to-creation implication, while steps 1.2 and 2.1 prove the data-supplied converse.

step 1.1step 2.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Strict Beck monadicity theorem

Statement

Let U:DC be a right adjoint. Then U is strictly monadic if and only if it strictly creates coequalizers of U-split pairs.

Both clauses are on-the-nose: the comparison is an isomorphism of categories, and each supplied split coequalizer has a unique lift with the same apex and legs.

Facts & Assumptions

Given: A right adjoint U:DC, a left adjoint F, induced monad T, and comparison functor K.

[L1]

The functor U is strictly monadic when K is an isomorphism of categories (Monadic and strictly monadic functors).

[L2]

The Eilenberg–Moore forgetful functor strictly creates coequalizers of UT-split pairs (The Eilenberg–Moore forgetful functor strictly creates coequalizers of UT-split pairs).

[L3]

The functor U strictly creates coequalizers of U-split pairs when every supplied splitting has a unique lift on the same apex and legs, and the lifted fork is a coequalizer (U-split pairs and ordinary or strict creation of their coequalizers).

[L4]

The underlying canonical presentation of every algebra is split in the base category (The canonical algebra presentation is split in the base, but its canonical splittings need not be algebra homomorphisms).

[L5]

Every T-algebra is the coequalizer in CT of its canonical pair of free algebras (Every algebra is the coequalizer of its canonical pair of free algebras).

Proof

technique · direct
1.1

For the forward direction, if K is an isomorphism then U=UTK on the nose. Transport through the inverse functor of K preserves the exact apex, legs, and uniqueness in [L2], so U has the strict-creation property in [L3].

L1L2L3
1.2

For the reverse direction, [L4] makes each lifted canonical pair U-split. Strict creation [L3] gives a unique object H(A,a) of D on the prescribed underlying apex A and a coequalizer whose underlying map is a:TAA. Uniqueness and the coequalizer universal property define H on algebra homomorphisms.

L3L4construct
2.1

The functor K(H(A,a)) and the given algebra (A,a) are lifts of the same split base fork; [L2] and the canonical coequalizer [L5] make the lift unique, so KH=1CT on objects and morphisms. For dD, its counit fork is the existing lift of the canonical split fork of K(d), so strict uniqueness gives HK(d)=d and the same equality on morphisms. Hence H is a two-sided inverse of K, and U is strictly monadic by [L1].

step 1.2L1L2L5algebra
3.1

Step 1.1 proves the forward implication and steps 1.2 and 2.1 prove the reverse implication, establishing the biconditional.

step 1.1step 2.1
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Data-supplied crude monadicity theorem for reflexive coequalizers

Statement

Let U:DC have a left adjoint. Suppose that a specific coequalizer is supplied for every reflexive pair in D, that U preserves these coequalizers, and that U reflects isomorphisms. Then U is monadic.

Facts & Assumptions

Given: An adjunction FU satisfying the three hypotheses in the Statement, with induced monad T and comparison functor K.

[L1]

A parallel pair f,g:AB is reflexive when it has a common section r:BA with fr=gr=1B (Reflexive parallel pairs and reflexive coequalizers).

[L2]

A conservative functor reflects isomorphisms (Conservative functor).

[L3]
[L4]

Every T-algebra is the coequalizer in CT of its canonical pair of free algebras (Every algebra is the coequalizer of its canonical pair of free algebras).

[L5]

The Eilenberg–Moore forgetful functor strictly creates coequalizers of its split pairs (The Eilenberg–Moore forgetful functor strictly creates coequalizers of UT-split pairs).

Proof

technique · direct
1.1

For a T-algebra (A,a), the pair F(TA)F(A) used in canonical reconstruction has common section F(ηA): one composite is the algebra unit law and the other is the adjunction triangle identity. Hence it is reflexive by [L1].

L1L3
2.1

Use the supplied coequalizer qA:F(A)H(A,a) of this reflexive pair. By hypothesis, applying U preserves it.

step 1.1given
3.1

The preserved coequalizer UqA and the split canonical base coequalizer in [L3] coequalize the same pair, so transport of the splitting makes the underlying fork of K(qA) split. By [L5], K(qA) is a coequalizer in CT; by [L4], so is the canonical fork ending at (A,a). Their universal properties therefore give an isomorphism KH(A,a)(A,a).

step 2.1L3L4L5
4.1

For dD, compare the coequalizer of the reflexive counit pair with the counit fork ending at d. Their images under U are isomorphic canonical coequalizers, so the comparison morphism becomes an isomorphism under U and is itself an isomorphism by [L2].

step 3.1L2
5.1

The supplied object assignment and coequalizer universality define H on algebra homomorphisms, and uniqueness makes the comparisons in steps 3.1 and 4.1 natural. Thus H is a quasi-inverse to K, so K is an equivalence and U is monadic.

step 4.1givenconstruct
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Groups are strictly monadic over sets

Statement

The underlying-set functor U:GrpSet is strictly monadic, and hence monadic.

Facts & Assumptions

Given: The free-group adjunction and its comparison functor.

[L1]

The Eilenberg–Moore category of the free-group monad is isomorphic over Set to the category of groups (The free-group monad has groups as its Eilenberg–Moore algebras).

[L2]

A functor is strictly monadic when its comparison functor is an isomorphism of categories (Monadic and strictly monadic functors).

[L3]

The comparison functor is K(d)=(Ud,Uεd) and acts on morphisms by K(h)=U(h) (The comparison functor to the Eilenberg–Moore category exists and is unique).

[L4]

Choosing a free group (F(X),iX) on every set X makes F left adjoint to the underlying-set functor U, the adjunction bijection sending φ:F(X)G to U(φ)iX (The free-group functor is left adjoint to the underlying-set functor).

[L5]

An algebra (A,a) for a monad (T,η,μ) satisfies aηA=1A and aT(a)=aμA, and an algebra homomorphism is a map commuting with the two structure maps (Algebra and algebra homomorphism for a monad).

Proof

technique · direct
1.1

By [L3], K(G)=(UG,UεG) and K(h)=U(h). Under [L4] the counit εG corresponds to the identity of UG, so it is the unique group homomorphism F(UG)G carrying each basis element g to g; a homomorphism out of a free group is determined by its values on the basis, so εG evaluates a reduced word in the elements of G to its product in G. Hence K(G) is the underlying set of G with word evaluation.

L3L4construct
2.1

A function f:UGUH commutes with word evaluation exactly when it is a group homomorphism: evaluating the words [x,y], the empty word and [x1] turns commutation into preservation of product, identity and inverse, and conversely a homomorphism preserves the value of every word. With [L5] and K(h)=U(h) this makes K bijective on the morphisms between any two groups.

step 1.1L5algebra
2.2

K is injective on objects, since step 1.1 recovers the product of G from UεG as its value on two-letter words.

step 1.1
2.3

K is surjective on objects. Let (A,a) be an algebra for the free-group monad. Put xy:=a([x,y]), 1:=a([]) and x1:=a([x1]). Writing a word as the concatenation of its first letter with its tail and applying the multiplication law aT(a)=aμA of [L5] to the corresponding word of words gives a(w)=a([x1])a(tail), while the unit law aηA=1A gives a([x])=x; induction on length therefore identifies a with evaluation of words in the operations just defined. Substituting the group-word identities into the same multiplication law turns them into associativity, the unit laws and the inverse laws, so those operations make A a group GA with a=UεGA, that is (A,a)=K(GA).

step 1.1L5construct
3.1

By steps 2.1, 2.2 and 2.3 the comparison is bijective on objects and on morphisms, hence an isomorphism of categories over Set; the isomorphism over Set asserted by [L1] may therefore be taken to be K. So U is strictly monadic by [L2], and strict monadicity implies monadicity.

step 2.1step 2.2step 2.3L1L2
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Modules over a fixed unital ring are strictly monadic over sets

Statement

For every fixed unital ring R, the underlying-set functor U:R-ModSet is strictly monadic, and hence monadic.

Facts & Assumptions

Given: A fixed unital ring R and the free-left-R-module adjunction.

[L1]

The Eilenberg–Moore category of the free-left-R-module monad is isomorphic over Set to the category of left R-modules (For a unital ring R, the free-R-module monad on sets has left R-modules as its Eilenberg–Moore algebras).

[L2]

A functor is strictly monadic when its comparison functor is an isomorphism of categories (Monadic and strictly monadic functors).

[L3]

The comparison functor is K(d)=(Ud,Uεd) and acts on morphisms by K(h)=U(h) (The comparison functor to the Eilenberg–Moore category exists and is unique).

Proof

technique · direct
1.1

The isomorphism in [L1] sends a module to its underlying set with its finite-linear-combination algebra structure and acts identically on underlying functions. By the comparison formula in [L3], it is the comparison for the free-module adjunction, including for the zero ring and zero module.

L1L3construct
2.1

The comparison is therefore an isomorphism over Set, so the underlying-set functor is strictly monadic by [L2].

step 1.1L2
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-24Open item page →

Integer-valued finite formal sums of words form unital convolution rings

Statement

For a set X, let X be its finite-word monoid and let

Z(X)={α:XZ:α has finite support}.

With pointwise addition and convolution

(αβ)(w)=uv=wα(u)β(v),

this is a unital ring. Its multiplicative identity is the basis vector supported at the empty word. When X=, the construction is canonically Z.

Facts & Assumptions

Given: A set X, its finite-word monoid X, and the displayed convolution formula.

[L1]

The assignment XX is the finite-word monoid functor (The free-monoid functor is left adjoint to the underlying-set functor).

[L2]

Every element of a free module has a unique finite expression in its standard basis, including the empty-basis case (The free module on a set and its standard basis).

[L3]

Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini formula (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

Proof

technique · direct
1.1

Regard Z(X) as the free abelian group on the words. Define the product by bilinearly extending concatenation of basis words, equivalently by the displayed coefficient formula.

L1L2construct
2.1

A finite word w has only finitely many cuts w=uv, and finite supports leave only finitely many nonzero summands. Hence every coefficient sum is finite, and the product has finite support contained in the finite set of concatenations of support words.

step 1.1L2L3
3.1

For α,β,γ, both coefficients of (αβ)γ and α(βγ) are the sum of α(u)β(v)γ(r) over triples with uvr=w. The two bracketings are bijective reindexings of the same finite set, so [L3] proves associativity.

step 2.1L1L3algebra
3.2

Splitting finite sums termwise proves (α+β)γ=αγ+βγ and α(β+γ)=αβ+αγ. Together with the pointwise abelian-group structure over Z, these are both distributive laws.

step 2.1L3algebra
4.1

Let δ[] be 1 on the empty word and 0 elsewhere. The only contributing cut with a nonzero δ[] factor is w=[]w or w=w[], so δ[]α=α=αδ[]. This verifies the multiplicative identity and all ring laws. If X=, then X={[]} and the coefficient at [] identifies the ring with Z.

step 3.1step 3.2L1algebra
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The free unital ring functor is left adjoint to the underlying-set functor

Statement

The free-word-ring construction XZ(X) extends to a functor FreeRing:SetRing left adjoint to the underlying-set functor. Its unit sends xX to the basis element of the one-letter word [x].

Facts & Assumptions

Given: A set X, its free word ring, a unital ring R, and a function u:XR.

[L1]

For every set X, integer-valued finite formal sums of words in X form a unital ring (Integer-valued finite formal sums of words form unital convolution rings).

[L2]

Every map from a basis set to a module extends uniquely to a linear map from the corresponding free module (Universal property of the free module on a set).

[L3]

Supplied objectwise universal arrows assemble uniquely into a left adjoint (Chosen objectwise universal arrows assemble uniquely into a left adjoint).

Proof

technique · direct
1.1

Send a word [x1,,xn] to u(x1)u(xn) in R, and send the empty word to 1R. The generator x is represented by the basis word [x].

L1construct
2.1

Apply [L2] over Z to extend this word-evaluation function uniquely to a Z-linear map uˉ:Z(X)R.

step 1.1L2
3.1

Expanding convolution as a finite sum shows uˉ(αβ)=uˉ(α)uˉ(β), and the empty-word basis vector maps to 1R. Thus uˉ is a unit-preserving ring homomorphism, including when R is the zero ring.

step 2.1L1algebra
4.1

Any ring homomorphism extending u must send every word basis vector to the corresponding product and is additive, so it equals uˉ by uniqueness in [L2].

step 3.1L2
5.1

Hence the generator inclusion is a universal arrow from every set X to the underlying-set functor on rings. By [L3] these universal arrows assemble into the free-ring functor and the asserted adjunction; for X= the free ring is Z.

step 4.1L3
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The underlying-set functor on unital rings strictly creates split coequalizers

Statement

The underlying-set functor U:RingSet strictly creates coequalizers of U-split pairs of unital ring homomorphisms.

Facts & Assumptions

Given: Ring homomorphisms f,g:AB and a supplied split coequalizer q:UBQ of their underlying functions.

[L1]

A split coequalizer has splitting maps satisfying qf=qg, qs=1Q, gt=1B, and ft=sq (Split coequalizer diagrams).

[L2]

A ring has associative and commutative addition, associative multiplication, two-sided additive and multiplicative identities, additive inverses, and multiplication distributing over addition on both sides (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides).

[L3]

A ring homomorphism preserves addition, multiplication, and the multiplicative identity (Ring homomorphism: additive, multiplicative, and required to send 1 to 1).

[L4]

Every split coequalizer is a coequalizer and is preserved by every functor (Every split coequalizer is a coequalizer and an absolute colimit).

Proof

technique · direct
1.1

By [L4], each finite Cartesian power qn is the coequalizer of fn,gn.

L1L4given
2.1

Each basic ring operation on B, followed by q, coequalizes the appropriate finite powers of f and g. It therefore descends uniquely to Q; explicitly 0Q=q(0B), 1Q=q(1B), and negation, addition, and multiplication are the unique operations making q preserve them.

step 1.1construct
3.1

Each ring axiom in [L2] becomes true after precomposition with the relevant surjection qn, because it then becomes the corresponding axiom in B. Hence the descended operations make Q a unital ring, including the zero-ring case.

step 2.1L2algebra
4.1

By construction q preserves addition, multiplication, and one, so it is a ring homomorphism by [L3].

step 2.1step 3.1L3
5.1

If a ring homomorphism r:BC coequalizes f,g, the set coequalizer gives a unique u:QUC with uq=r. Precomposing the preservation equations for u with the appropriate qn reduces them to those for r, so u is a ring homomorphism and is the unique algebraic factor.

step 4.1L3
6.1

The descended operations are uniquely forced by the requirement that the supplied q be a ring homomorphism. Thus the lift has exactly the same apex and legs and is unique, which is strict creation.

step 2.1step 5.1
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Monoids and unital rings are strictly monadic over sets

Statement

The underlying-set functors from monoids and from unital rings to Set are strictly monadic, and hence monadic.

Facts & Assumptions

Given: The free-monoid and free-ring adjunctions.

[L1]

The Eilenberg–Moore category of the free-monoid monad is isomorphic over Set to the category of monoids (The free-monoid monad has monoids as its Eilenberg–Moore algebras).

[L2]

The free unital ring functor is left adjoint to the underlying-set functor (The free unital ring functor is left adjoint to the underlying-set functor).

[L3]

The underlying-set functor on unital rings strictly creates split coequalizers (The underlying-set functor on unital rings strictly creates split coequalizers).

[L4]

A right adjoint is strictly monadic if and only if it strictly creates coequalizers of its split pairs (Strict Beck monadicity theorem).

[L5]

Choosing a free monoid (X,iX) on every set X makes the finite-word functor left adjoint to the underlying-set functor, the adjunction bijection sending φ:XM to U(φ)iX (The free-monoid functor is left adjoint to the underlying-set functor).

[L6]

The comparison functor is K(d)=(Ud,Uεd) and K(h)=U(h) (The comparison functor to the Eilenberg–Moore category exists and is unique).

[L7]

An algebra (A,a) for a monad (T,η,μ) satisfies aηA=1A and aT(a)=aμA, and an algebra homomorphism is a map commuting with the two structure maps (Algebra and algebra homomorphism for a monad).

Proof

technique · direct
1.1

By [L6], the comparison for the free-monoid adjunction is K(M)=(UM,UεM) with K(h)=U(h). Under [L5] the counit εM corresponds to the identity of UM, so it is the unique monoid homomorphism (UM)M carrying each one-letter word [m] to m; a homomorphism out of a free monoid is determined on the letters, so εM evaluates a word in the elements of M to its product.

L5L6construct
1.2

For rings, [L2] supplies the left adjoint and [L3] supplies strict creation of the required split coequalizers.

L2L3
2.1

Applying strict Beck [L4] to step 1.2 makes the ring underlying-set functor strictly monadic. The construction includes the empty generating set and the zero ring.

step 1.2L4
2.2

A function f:UMUN commutes with word evaluation exactly when it is a monoid homomorphism, by evaluating the two-letter words and the empty word in one direction and every word in the other; with [L7] and K(h)=U(h) this makes K bijective on morphisms. It is injective on objects because step 1.1 recovers the product of M from UεM on two-letter words.

step 1.1L7algebra
2.3

K is surjective on objects: for an algebra (A,a) of the free-monoid monad put xy:=a([x,y]) and 1:=a([]). Splitting a word into its first letter and its tail and applying the multiplication law aT(a)=aμA of [L7] gives a(w)=a([x1])a(tail), while the unit law gives a([x])=x; induction on length identifies a with evaluation of words in these operations, and substituting the monoid-word identities into the same law gives associativity and the unit laws. Hence A is a monoid MA with a=UεMA, that is (A,a)=K(MA).

step 1.1L7construct
3.1

By steps 2.2 and 2.3 the monoid comparison is bijective on objects and morphisms, hence an isomorphism of categories over Set — the isomorphism [L1] asserts may be taken to be it — so the monoid underlying-set functor is strictly monadic. With step 2.1 this proves the assertion for both concrete categories, and strict monadicity implies monadicity.

step 2.1step 2.2step 2.3L1
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

G-sets are strictly monadic over sets

Statement

For a fixed group G, the underlying-set functor from the category of left G-sets and equivariant maps to Set is strictly monadic.

Facts & Assumptions

Given: A fixed group G with identity e.

[L1]

A left G-action satisfies ex=x and (gh)x=g(hx) (Left group actions, transitive actions, and faithful actions).

[L2]

A map of G-sets is equivariant when f(gx)=gf(x) for every g,x (Equivariant maps and isomorphisms of group actions).

[L3]

A T-algebra structure a:TXX satisfies aηX=1X and aT(a)=aμX, and an algebra homomorphism satisfies the corresponding square (Algebra and algebra homomorphism for a monad).

[L4]

A functor is strictly monadic when its comparison with the Eilenberg–Moore category is an isomorphism (Monadic and strictly monadic functors).

Proof

technique · direct
1.1

Define F(X)=G×X with action h(g,x)=(hg,x). A function u:XUY into a G-set extends uniquely to the equivariant map uˉ(g,x)=gu(x), whose inverse correspondence evaluates at (e,x). This natural bijection gives the free-action adjunction FU.

L1construct
2.1

Its induced monad is T(X)=G×X, with T(f)=1G×f, ηX(x)=(e,x), and μX(g,(h,x))=(gh,x). The group identity and associativity laws verify the monad equations.

step 1.1L1algebra
3.1

A map a:G×XX satisfies the two algebra laws in [L3] exactly when a(e,x)=x and a(g,a(h,x))=a(gh,x), which are the action laws in [L1]. This includes the empty set, the trivial group, and trivial actions.

step 2.1L1L3
4.1

The algebra-homomorphism equation is f(a(g,x))=b(g,f(x)), exactly the equivariance condition in [L2].

step 3.1L2L3
5.1

By steps 3.1 and 4.1, the comparison for the adjunction constructed in step 1.1 is bijective on objects and morphisms, with inverse given by the same action structure and underlying functions. It is therefore an isomorphism over Set, so the underlying-set functor is strictly monadic by [L4].

step 1.1step 3.1step 4.1L4
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Direct and inverse image satisfy Beck–Chevalley for pullback squares of sets

Statement

Let

PqYpgXfZ

be a pullback square of sets. For every AX,

q[p1[A]]=g1[f[A]].

Equivalently, direct image and inverse image satisfy q!p=gf! on power sets. The formula remains valid for empty fibres and identity pullbacks.

Facts & Assumptions

Given: The displayed pullback square and a subset AX.

[L1]

A pullback of XfZgY has projections satisfying fp=gq and the universal property for every compatible pair (Pullbacks and pushouts as limits and colimits of cospans and spans).

[L2]

Membership in a direct image or inverse image is witnessed by the corresponding relation equation (The image R[A] and the preimage R1[B] of a set under a relation).

Proof

technique · direct
1.1

If yq[p1[A]], then some wP satisfies q(w)=y and p(w)A. The pullback equation gives g(y)=gq(w)=fp(w), so g(y)f[A] and yg1[f[A]].

L1L2
1.2

Conversely, if yg1[f[A]], choose xA with f(x)=g(y). The pullback universal property supplies the unique wP with p(w)=x and q(w)=y, so yq[p1[A]]. If the fibre is empty, both existential conditions fail.

L1L2construct
2.1

Steps 1.1 and 1.2 prove equality. Identity squares give the identity direct and inverse images; if one map is a section of the other, the same equality specializes to the usual section–retraction image formulas.

step 1.1step 1.2
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24 rests on unproved material (inherited)Open item page →
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.

The contravariant power-set functor is monadic

Statement

The contravariant power-set functor

P:SetopSet,XP(X),fopf1,

is monadic.

Facts & Assumptions

Given: The contravariant power-set functor between Setop and Set.

[L1]

An adjunction may be specified by a natural family of hom-set bijections (The unit-counit, hom-set, unit-universal, and counit-universal encodings of an adjunction are equivalent).

[L2]

A conservative functor reflects isomorphisms (Conservative functor).

[L3]

Direct and inverse image satisfy Beck–Chevalley for pullback squares of sets (Direct and inverse image satisfy Beck–Chevalley for pullback squares of sets).

[L4]

A right adjoint equipped with a specified coequalizer for every reflexive pair is monadic when it preserves those coequalizers and reflects isomorphisms (Data-supplied crude monadicity theorem for reflexive coequalizers).

Proof

technique · direct
1.1

A function XP(Y) is the same as a relation RX×Y. Transposing R gives a function YP(X), and transposition is natural and involutive. By [L1] this makes the power-set functor on the opposite side its own left adjoint.

L1construct
1.2

If f1:P(Y)P(X) is bijective, then f is surjective because otherwise and a singleton outside f[X] have the same preimage. It is injective because surjectivity of f1 realizes each singleton of X as a preimage, which separates points with different singleton membership. Thus f is bijective and the functor is conservative by [L2], including when X is empty.

L2algebra
1.3

A reflexive pair in Setop corresponds to maps f,g:AB in Set with a common retraction r:BA, so rf=rg=1A. Define E={aA:f(a)=g(a)} and let e:EA be inclusion. This formula supplies an equalizer for every such pair uniformly, so the opposite maps form the required specified family of reflexive coequalizers in Setop.

L5construct
2.1

The square with both left and top maps e:EA, and with bottom and right maps f,g:AB, is a pullback: if f(a)=g(a), applying r gives a=aE. Hence [L3] gives e[e1[S]]=g1[f[S]]=Se[E] for every SA; the last equality also follows directly, while f1[f[S]]=S because rf=1A.

step 1.3L3algebra
3.1

Let H:P(A)Z satisfy Hf1=Hg1. Applying this equality to f[S] and using step 2.1 gives H(S)=H(Se[E]). Define Hˉ:P(E)Z by Hˉ(R)=H(e[R]). Then Hˉe1=H, and this factorization is unique because e1:P(A)P(E) is surjective. Thus e1 is the coequalizer of f1,g1, so the power-set functor preserves every reflexive coequalizer in Setop.

step 2.1construct
4.1

Step 1.3 supplies the required coequalizer family, while steps 1.1, 1.2, and 3.1 give the left adjoint, conservativity, and preservation hypotheses of [L4]. The crude monadicity theorem therefore proves that P:SetopSet is monadic.

step 1.1step 1.2step 1.3step 3.1L4
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24 rests on unproved material (inherited)Open item page →
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.

Finitary functors and finitary monads

Definition

A functor is finitary when it preserves every small filtered colimit (Filtered categories and filtered colimits, Preservation, reflection, and creation of limits and colimits; continuous and cocontinuous functors).

A monad (T,η,μ) is finitary when its underlying endofunctor T is finitary (Monad on a category). No preservation claim is imposed on the unit or multiplication separately.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24 rests on unproved material (inherited)Open item page →
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.

Categories of models for algebraic theories

Definition

A category of models for an algebraic theory is a category A equipped with a monadic functor U:ASet whose induced monad on Set is finitary (Monadic and strictly monadic functors, Finitary functors and finitary monads).

Equivalently, up to the comparison equivalence over Set, it is the Eilenberg–Moore category of a finitary monad on sets. The phrase records the finitary monadic presentation as part of the data; it does not choose such a presentation for an arbitrary category.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24 rests on unproved material (inherited)Open item page →
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.

Over a cocomplete base, a monadic category is cocomplete exactly when it has coequalizers

Statement

Let U:AC be monadic and suppose C is cocomplete. Then A is cocomplete if and only if A has coequalizers.

Facts & Assumptions

Given: A monadic functor U:AC with cocomplete base C and induced monad T.

[L1]

A category is cocomplete when every small diagram in it has a colimit (Finite, small, and large limits and colimits; complete and cocomplete categories).

[L2]

Once the required coproducts and a coequalizer between them exist, every small colimit is constructed by the standard coproduct-coequalizer formula (Every small colimit can be constructed as a coequalizer between coproducts over the arrows and objects of the index category).

[L3]

An equivalence of categories preserves and reflects every existing colimit (Equivalences preserve, reflect, and create limits and colimits in the isomorphism-invariant sense).

[L4]

Every T-algebra (A,a) is the coequalizer in CT of the canonical pair T(a),μA:T2ATA (Every algebra is the coequalizer of its canonical pair of free algebras).

[L5]

The free T-algebra functor FT is left adjoint to the Eilenberg–Moore forgetful functor (The free–forgetful Eilenberg–Moore adjunction induces the given monad).

[L6]

Left adjoints preserve every colimit that exists (Left adjoints preserve every colimit that exists).

Proof

technique · direct
1.1

For the forward direction, if A is cocomplete then it has the colimit of every parallel pair, hence every coequalizer.

L1
1.2

For the reverse direction, replace A across its monadic comparison equivalence by CT. Given a small family (Ai,ai), [L5] and [L6] identify the coproducts of free algebras P:=iFT(TAi),Q:=iFT(Ai) with free algebras on the corresponding base coproducts. If ji and ki are their coproduct injections, define α,β:PQ by αji=kiT(ai),βji=kiμAi. By hypothesis this pair has a coequalizer q:QR in CT. The construction also applies to the empty family.

L5L6construct
2.1

For every i, the map qki coequalizes the canonical pair for (Ai,ai). Its universal property [L4] gives a unique algebra map ιi:(Ai,ai)R satisfying ιiai=qki.

step 1.2L4
3.1

Given algebra maps ri:(Ai,ai)(D,d), the maps riai:FT(Ai)(D,d) assemble to a map r:Q(D,d). Each coequalizes its canonical pair by [L4], so rα=rβ and there is a unique rˉ:R(D,d) with rˉq=r. Then rˉιi=ri because the two maps agree after the epimorphism ai, and uniqueness follows because the qki=ιiai are jointly epimorphic. Thus (R,(ιi)) is the coproduct of the family.

step 1.2step 2.1L4construct
4.1

For the reverse direction, CT now has all small coproducts by step 3.1 and all coequalizers by hypothesis, so [L2] constructs every small colimit.

step 3.1L2
5.1

For the reverse direction, transport these colimits back across the comparison equivalence by [L3]. Thus A is cocomplete.

step 4.1L3
6.1

Step 1.1 proves the forward implication, while steps 1.2 to 5.1 prove the reverse implication, establishing the biconditional.

step 1.1step 5.1
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24 rests on unproved material (inherited)Open item page →
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.

Under dependent choice, algebras for a finitary monad on a complete cocomplete locally small category have coequalizers

Statement

Assume dependent choice. If T is a finitary monad on a complete, cocomplete, locally small category C, then the Eilenberg–Moore category CT has coequalizers.

Facts & Assumptions

Given: Dependent choice, a complete cocomplete locally small category C, a finitary monad T, and algebra homomorphisms f,g:(A,a)(B,b).

[L1]

A functor is finitary when it preserves every small filtered colimit (Finitary functors and finitary monads).

[L2]

Dependent choice produces a sequence from a nonempty set with an entire successor relation and a specified starting point (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain).

[L3]

Let V:AB have complete locally small domain and be continuous. If V satisfies the solution-set condition at BB, then (BV) has an initial object, equivalently a universal arrow from B to V (General adjoint functor theorem, objectwise initial-object form).

[L4]

The Eilenberg–Moore forgetful functor strictly creates every limit existing in the base (The Eilenberg–Moore forgetful functor strictly creates every limit that exists in the base).

[L5]

If A and the indexing category J are small and chosen limits of the pointwise diagrams exist, those choices form a limit in [A,C] (For small source and index categories, chosen target limits and colimits compute the corresponding functor-category limits and colimits pointwise).

Proof

technique · direct
1.1

In C, form q0:BQ0, the coequalizer of f,g, and p0:TBP0, the coequalizer of Tf,Tg. Their universal properties induce maps u0:P0Q0 and v0:P0TQ0 characterized by u0p0=q0b and v0p0=Tq0. Both p0 and q0 are epimorphisms.

givenconstruct
1.2

The category CT is complete by [L4] and locally small because its hom-sets are subsets of those of C. The walking parallel-pair category is finite and hence small. For any small limit diagram, the finitely many pointwise limits can be chosen without a choice axiom, so [L5] makes the parallel-pair functor category complete. The constant-diagram functor is continuous because these limits are pointwise.

L4L5construct
2.1

Suppose (Pn,Qn,un,vn,pn,qn) has been constructed with unpn=qnb and vnpn=Tqn. Put Pn+1=TQn, and choose un+1:TQnQn+1 as a coequalizer of T(un),μQnT(vn):TPnTQn. Define qn,n+1=un+1ηQn, vn+1=Tqn,n+1, pn+1=vnpn, and qn+1=qn,n+1qn. Naturality of η and the monad unit law give qn,n+1un=un+1ηQnun=un+1vn. Consequently un+1pn+1=qn+1b and vn+1pn+1=Tqn+1.

step 1.1algebraconstruct
2.2

Let h:(B,b)(C,c) be any algebra homomorphism with hf=hg. Factor it uniquely as h=k0q0. Precomposing with the epimorphism p0 and using step 1.1 gives cT(k0)v0=k0u0.

step 1.1constructalgebra
3.1

To justify the countable sequence of choices in step 2.1, encode each finite stage by a set. For a state x, let S(x) be all valid successor codes of least possible von Neumann rank; it is a nonempty subset of some Vα, hence a set. Starting with the code from step 1.1, recursively close under xS(x) for finitely many steps and take the union over N. Replacement and union make this closure a set on which the successor relation is entire. Applying [L2] to that set gives one compatible sequence of stages.

step 1.1step 2.1L2choose
3.2

Suppose kn:QnC satisfies cT(kn)vn=knun. The algebra law for c shows that cT(kn) coequalizes T(un) and μQnT(vn), so it factors uniquely through un+1 as a map kn+1:Qn+1C with kn+1un+1=cT(kn). The definitions in step 2.1 then give kn+1qn,n+1=kn and cT(kn+1)vn+1=kn+1un+1, closing the induction.

step 2.1step 2.2algebraconstruct
4.1

Form the sequential colimits Qω=colimnQn and Pω=colimnPn, with injections qn,ω and pn,ω. The identities qn,n+1un=un+1vn make the un a map of the two sequential diagrams, hence induce uω:PωQω. The compatible qn induce qω:BQω. The shifted identities Pn+1=TQn and vn+1=Tqn,n+1 identify Pω with colimnTQn.

step 2.1step 3.1construct
5.1

The natural-number indexing category is filtered, so finitarity [L1] identifies the colimit in step 4.1 with TQω. Make this identification, so Pω=TQω and the induced comparison vω:PωTQω is the identity. Thus uω:TQωQω.

step 4.1L1
6.1

For every n, naturality of η and the definition of qn,n+1 give uωηQωqn,ω=qn,ω. The colimit injections are jointly epimorphic, so uωηQω=1Qω.

step 2.1step 5.1algebra
6.2

The compatible kn induce k:QωC. Passing the equations kn+1un+1=cT(kn) to the colimit gives kuω=cT(k), and compatibility at stage zero gives kqω=h.

step 5.1step 3.2
7.1

The successor coequalizer equations are un+1T(un)=un+1μQnT(vn). Passing these compatible equations to the filtered colimit gives uωT(uω)=uωμQωT(vω)=uωμQω because vω=1 in step 5.1. Together with step 6.1, this makes (Qω,uω) a T-algebra.

step 2.1step 5.1step 6.1algebra
8.1

Passing unpn=qnb and vnpn=Tqn to the colimit gives uωTqω=qωb, so qω is an algebra homomorphism; it coequalizes f,g because q0 does.

step 2.1step 5.1step 7.1
9.1

By steps 6.2 and 7.1, k is an algebra homomorphism, and step 6.2 gives kqω=h. Therefore the single algebra fork qω is a solution set for the constant-diagram functor Δ:CT(CT) at the given parallel pair: every algebra fork factors through it, without a uniqueness assertion.

step 8.1step 6.2step 7.1construct
10.1

Apply [L3] to Δ using the singleton solution set from step 9.1 and the complete, locally small, and continuity properties proved in step 1.2. The resulting universal arrow is a left adjoint value for Δ, hence a coequalizer of f,g in CT. Since the pair was arbitrary, all coequalizers exist.

step 9.1step 1.2L3
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24 rests on unproved material (inherited)Open item page →
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.

Under dependent choice, a finitary monad on a complete cocomplete locally small category has complete and cocomplete algebras

Statement

Assume dependent choice. If T is a finitary monad on a complete, cocomplete, locally small category C, then its Eilenberg–Moore category CT is complete and cocomplete.

The completeness conclusion itself uses no choice; dependent choice enters only in the construction of coequalizers used for cocompleteness.

Facts & Assumptions

Given: Dependent choice and a finitary monad T on a complete cocomplete locally small category C.

[L1]

The Eilenberg–Moore forgetful functor strictly creates every limit that exists in the base (The Eilenberg–Moore forgetful functor strictly creates every limit that exists in the base).

[L2]

Under dependent choice, algebras for such a finitary monad have coequalizers (Under dependent choice, algebras for a finitary monad on a complete cocomplete locally small category have coequalizers).

[L3]

Over a cocomplete base, a monadic category is cocomplete exactly when it has coequalizers (Over a cocomplete base, a monadic category is cocomplete exactly when it has coequalizers).

[L4]

The Eilenberg–Moore adjunction induces the given monad on the nose (The free–forgetful Eilenberg–Moore adjunction induces the given monad).

Proof

technique · direct
1.1

Since C has every small limit, [L1] creates every such limit in CT, including the empty limit. Thus CT is complete without using dependent choice.

L1
1.2

Under the stated dependent-choice hypothesis, [L2] gives every coequalizer in CT, including equal parallel maps and the zero-stage case of its construction.

L2
2.1

By [L4], the Eilenberg–Moore adjunction induces T on the nose, so its forgetful functor is monadic. Applying [L3] to the cocomplete base and step 1.2 makes CT cocomplete, including the empty colimit.

step 1.2L3L4
3.1

Combining step 1.1 with step 2.1 proves that CT is complete and cocomplete.

step 1.1step 2.1
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24 rests on unproved material (inherited)Open item page →
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.

Under dependent choice, categories of models for algebraic theories are complete and cocomplete

Statement

Assume dependent choice. Every category of models for an algebraic theory is complete and cocomplete.

Facts & Assumptions

Given: Dependent choice and a category A of models for an algebraic theory.

[L1]

A category of models for an algebraic theory is equipped with a finitary monadic functor to Set (Categories of models for algebraic theories).

[L4]

Equivalences preserve and reflect existing limits and colimits (Equivalences preserve, reflect, and create limits and colimits in the isomorphism-invariant sense).

[L5]

Under dependent choice, a finitary monad on a complete cocomplete locally small category has a complete and cocomplete Eilenberg–Moore category (Under dependent choice, a finitary monad on a complete cocomplete locally small category has complete and cocomplete algebras).

Proof

technique · direct
1.1

By [L2] and [L3], Set is complete and cocomplete; it is locally small because each function collection between two sets is a set. This includes empty diagrams.

L2L3given
2.1

The finitary monad induced by [L1] satisfies the hypotheses of [L5], so under dependent choice its Eilenberg–Moore category is complete and cocomplete.

step 1.1L1L5
3.1

The comparison supplied by [L1] is an equivalence over Set. Transporting the limits and colimits of step 2.1 across it by [L4] proves that A is complete and cocomplete.

step 2.1L1L4
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The ultrafilter extension principle (UL/BPI)

Definition

The ultrafilter extension principle says that every filter on a set is contained in an ultrafilter on that set (Ultrafilter).

It is also called the ultrafilter lemma and is equivalent over ZF to the Boolean prime ideal theorem, abbreviated BPI. Items below write assume UL/BPI precisely when they use this extension principle; they do not thereby assume the full axiom of choice.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

A given ultrafilter on a compact Hausdorff space has a unique limit

Statement

Every ultrafilter on a compact Hausdorff space converges to exactly one point. This statement concerns a given ultrafilter and uses no ultrafilter-extension or other choice principle.

Facts & Assumptions

Given: A compact Hausdorff space X and an ultrafilter U on X.

[L1]

Compactness is equivalent to the assertion that every family of closed subsets with the finite-intersection property has nonempty intersection (A space is compact exactly when every family of closed subsets with the finite intersection property has nonempty intersection).

[L2]

Every cluster point of an ultrafilter is a limit of that ultrafilter (Every cluster point of an ultrafilter is a limit of that ultrafilter).

Proof

technique · direct
1.1

The closed members of U have the finite-intersection property: a finite intersection remains in the filter and cannot be empty.

givenalgebra
2.1

By compactness and [L1], choose a point x in the intersection of all closed members of U. If X=, no ultrafilter exists, so the universal assertion is vacuous.

step 1.1L1choose
3.1

For every AU, its closure also belongs to U and contains x; hence every neighbourhood of x meets every member of U. Thus x is a cluster point and therefore a limit by [L2].

step 2.1L2
4.1

If x and y were distinct limits, [L3] would give disjoint open neighbourhoods V of x and W of y. Both would belong to U, forcing VW= into the filter, a contradiction. Hence the limit is unique, including in a singleton space.

step 3.1L3algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The ultrafilter-limit map of a compact Hausdorff space is an algebra for the ultrafilter monad

Statement

Let X be compact Hausdorff, and define ξX:βXX by sending each ultrafilter to its unique limit. Then ξX is an algebra for the ultrafilter monad:

ξXηX=1X,ξXμX=ξXβ(ξX).

Facts & Assumptions

Given: A compact Hausdorff space X and its ultrafilter-limit map ξX.

[L1]

Every ultrafilter on a compact Hausdorff space has exactly one limit (A given ultrafilter on a compact Hausdorff space has a unique limit).

[L2]

The ultrafilter monad has principal unit ηX(x)={AX:xA} and flattening multiplication μX(W)={AX:A^W}, where A^={U:AU} (The ultrafilter endofunctor with principal unit and flattening multiplication).

[L3]

A T-algebra structure a satisfies aη=1 and aT(a)=aμ (Algebra and algebra homomorphism for a monad).

Proof

technique · direct
1.1

By [L1], ξX is defined on every ultrafilter. When X=, both βX and X are empty and the unique empty map satisfies the equations below.

L1construct
2.1

The principal ultrafilter ηX(x) contains every neighbourhood of x, so it converges to x. Uniqueness in [L1] gives ξXηX(x)=x for every x.

step 1.1L2algebra
2.2

Let W be an ultrafilter on βX. If an open neighbourhood O of a point belongs to the pushforward β(ξX)(W), then ξX1[O]W. Every ultrafilter whose limit lies in O contains O, so ξX1[O]O^; upward closure gives O^W, hence OμX(W) by [L2]. Thus every limit of the pushforward is a limit of the flattening.

step 1.1L2algebra
3.1

Both ultrafilters in step 2.2 have unique limits by [L1], so their limits coincide: ξXβ(ξX)(W)=ξXμX(W).

step 2.2L1
4.1

Steps 2.1 and 3.1 are exactly the unit and multiplication equations in [L3], so ξX is an ultrafilter algebra.

step 2.1step 3.1L3
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

A continuous map of compact Hausdorff spaces is an ultrafilter-algebra homomorphism

Statement

Let f:XY be continuous between compact Hausdorff spaces, and let ξX,ξY be their ultrafilter-limit maps. Then

fξX=ξYβ(f),

so f is an ultrafilter-algebra homomorphism.

Facts & Assumptions

Given: A continuous map f:XY of compact Hausdorff spaces and an ultrafilter U on X.

[L1]

The pushforward fU is an ultrafilter on Y, and ultrafilter pushforward is functorial (Pushforward sends ultrafilters to ultrafilters and is functorial).

[L2]

Every ultrafilter on a compact Hausdorff space has exactly one limit (A given ultrafilter on a compact Hausdorff space has a unique limit).

[L3]

A T-algebra homomorphism f:(A,a)(B,b) satisfies fa=bT(f) (Algebra and algebra homomorphism for a monad).

Proof

technique · direct
1.1

Push U forward along f to the ultrafilter fU on Y supplied by [L1].

L1
2.1

If U converges to x, then for each neighbourhood V of f(x), continuity makes f1[V] a neighbourhood of x and hence a member of U. Therefore VfU, so the pushforward converges to f(x).

step 1.1given
3.1

Taking x=ξX(U), uniqueness in the target gives ξY(fU)=f(ξX(U)).

step 2.1L2
4.1

Since fU=β(f)(U), step 3.1 is the equation fξX=ξYβ(f) in [L3]. Thus f is an algebra homomorphism, including for the unique map from an empty compact space.

step 3.1L3
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The open-set family induced by an ultrafilter algebra

Definition

Let ξ:βXX be an algebra (Algebra and algebra homomorphism for a monad) for the ultrafilter monad, that is, for the endofunctor β with its principal unit and flattening multiplication, which form a monad on Set by The ultrafilter endofunctor with principal unit and flattening multiplication is a monad. A subset OX is ξ-open, or induced-open, when

ξ(U)OOU

for every ultrafilter U on X. Write τξ for the family of all ξ-open subsets.

The topology induced by ξ is τξ. The fact that this family satisfies the topology axioms is proved in The open-set family induced by an ultrafilter algebra is a topology .

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The open-set family induced by an ultrafilter algebra is a topology

Statement

For every ultrafilter algebra ξ:βXX, the family τξ of induced-open subsets is a topology on X.

Facts & Assumptions

Given: An ultrafilter algebra ξ:βXX and its induced-open family τξ.

[L1]

A subset OX is induced-open when ξ(U)O implies OU for every ultrafilter U on X (The open-set family induced by an ultrafilter algebra).

[L2]

A topology contains the empty set and whole space, is closed under arbitrary unions, and is closed under finite intersections (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison).

Proof

technique · direct
1.1

The empty set is induced-open because its antecedent never holds, and X is induced-open because every ultrafilter contains X.

L1algebra
1.2

Let (Oi)iI be induced-open and suppose ξ(U)iOi. Some Oi contains ξ(U), hence OiU by [L1], and upward closure gives iOiU. Thus arbitrary unions are induced-open.

L1algebra
2.1

If O and V are induced-open and ξ(U)OV, then O,VU by [L1], so OVU. This also covers the empty and singleton finite intersections using step 1.1.

L1algebra
3.1

Steps 1.1, 1.2, and 2.1 verify the axioms in [L2], so τξ is a topology. No extension of a filter and no choice principle was used.

step 1.1step 1.2step 2.1L2
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Under the ultrafilter lemma, closure in an ultrafilter-algebra topology is the image of ultrafilters containing the set

Statement

Assume UL/BPI. Let ξ:βXX be an ultrafilter algebra, give X its induced topology, and put

A^:={UβX:AU}.

Then for every AX,

A=ξ[A^].

Facts & Assumptions

Given: UL/BPI, an ultrafilter algebra ξ:βXX, its induced topology, and a subset AX.

[L1]

The closure of A is the smallest closed subset containing A (Interior, closure, boundary, exterior, derived set and isolated point in a topological space).

[L2]

The ultrafilter extension principle says that every filter on a set is contained in an ultrafilter on that set (The ultrafilter extension principle (UL/BPI)).

[L3]

Flattening satisfies BμX(W) exactly when B^W (The ultrafilter endofunctor with principal unit and flattening multiplication).

[L4]

An ultrafilter contains exactly one of C and XC for every CX (Characterisation of ultrafilters: every set or its complement).

Proof

technique · direct
1.1

If xA, its principal ultrafilter contains A and the algebra unit law gives ξ(ηX(x))=x. Hence Aξ[A^]; when A=, no ultrafilter contains it and both sides of this inclusion are empty.

givenconstruct
1.2

A set CX is induced-closed exactly when every ultrafilter containing C has its algebra value in C: this is the complement of the defining induced-open implication, using [L4].

L4algebra
2.1

Put C=ξ[A^] and fix an ultrafilter V with CV. On βX, the family consisting of A^ and all ξ1[B] for BV has the finite-intersection property: for a finite intersection B of members of V, choose xBC and then an ultrafilter in A^ mapping to x. By [L2], extend this family to an ultrafilter W on βX.

step 1.2L2choose
3.1

Since A^W, [L3] gives AμX(W). Since every ξ1[B] with BV lies in W, maximality gives β(ξ)(W)=V. The algebra multiplication law yields ξ(V)=ξμX(W)ξ[A^]=C. Thus C is induced-closed by step 1.2.

step 2.1L3algebra
4.1

If D is any induced-closed superset of A, every ultrafilter containing A contains D, so step 1.2 gives ξ[A^]D. By steps 1.1 and 3.1, ξ[A^] is itself a closed superset of A, hence it is the closure by [L1]. This also gives =.

step 1.1step 3.1L1
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Under the ultrafilter lemma, an ultrafilter algebra maps each ultrafilter to its unique limit

Statement

Assume UL/BPI. For an ultrafilter algebra ξ:βXX with its induced topology, every ultrafilter U converges to exactly one point, namely ξ(U).

Facts & Assumptions

Given: UL/BPI, an ultrafilter algebra ξ:βXX, and an ultrafilter U on X.

[L2]

A filter converges to p when every neighbourhood of p belongs to the filter (Convergence and cluster points of a filter on a topological space).

[L3]

The ultrafilter extension principle says that every filter on a set is contained in an ultrafilter on that set (The ultrafilter extension principle (UL/BPI)).

Proof

technique · direct
1.1

If an induced-open neighbourhood O contains ξ(U), the definition of induced-open gives OU. Thus U converges to ξ(U) by [L2].

givenL2
1.2

Let x be any limit of U. For each AU, every neighbourhood of x meets A, so xA=ξ[A^] by [L1].

L1L2
2.1

On βX, the family {A^:AU}{ξ1[{x}]} has the finite-intersection property by step 1.2. Extend it by [L3] to an ultrafilter W on βX.

step 1.2L3choose
3.1

The inclusions forced by step 2.1 and maximality give μX(W)=U and β(ξ)(W)=ηX(x). The algebra laws therefore give ξ(U)=ξμX(W)=ξβ(ξ)(W)=ξηX(x)=x.

step 2.1algebra
4.1

Step 1.1 supplies the limit ξ(U) and step 3.1 identifies every other limit with it, proving existence and uniqueness. If X=, no ultrafilter exists and the assertion is vacuous.

step 1.1step 3.1
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Under the ultrafilter lemma, every ultrafilter algebra determines a compact Hausdorff topology

Statement

Assume UL/BPI. For every ultrafilter algebra ξ:βXX, the topology induced by ξ is compact and Hausdorff.

Facts & Assumptions

Given: UL/BPI and an ultrafilter algebra ξ:βXX.

[L1]

The open-set family induced by an ultrafilter algebra is a topology (The open-set family induced by an ultrafilter algebra is a topology).

[L2]

Under UL/BPI, every ultrafilter has exactly one limit in the induced topology, namely its algebra value (Under the ultrafilter lemma, an ultrafilter algebra maps each ultrafilter to its unique limit).

[L4]

The ultrafilter extension principle says that every filter on a set is contained in an ultrafilter on that set (The ultrafilter extension principle (UL/BPI)).

Proof

technique · direct
1.1

Equip X with the topology supplied by [L1].

L1
1.2

By [L2], every ultrafilter on X converges, and its limit is unique.

L2
2.1

The equivalence in [L3] applied to step 1.2 proves that the induced topology is compact.

step 1.2L3
2.2

If distinct x,y had no disjoint neighbourhoods, the union of their two neighbourhood filters would have the finite-intersection property. By [L4] it extends to an ultrafilter converging to both x and y, contradicting uniqueness in step 1.2. Hence the topology is Hausdorff, with the empty and singleton cases vacuous.

step 1.2L4choose
3.1

Steps 2.1 and 2.2 prove that the induced topology is compact Hausdorff.

step 2.1step 2.2
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Under the ultrafilter lemma, compact Hausdorff spaces and ultrafilter algebras are recovered by the two limit constructions

Statement

Assume UL/BPI. The following constructions are inverse on objects and morphisms:

  1. a compact Hausdorff space X is sent to the ultrafilter algebra whose structure map takes each ultrafilter to its unique limit;
  2. an ultrafilter algebra ξ:βXX is sent to its induced compact Hausdorff topology.

In particular, rebuilding the algebra recovers ξ, rebuilding the topology recovers the original topology, continuous maps are algebra homomorphisms, and algebra homomorphisms are continuous. Thus the two concrete categories are isomorphic over Set.

Facts & Assumptions

Given: UL/BPI, the limit-algebra construction on compact Hausdorff spaces, and the induced-topology construction on ultrafilter algebras.

[L1]

The ultrafilter-limit map of a compact Hausdorff space is an algebra for the ultrafilter monad (The ultrafilter-limit map of a compact Hausdorff space is an algebra for the ultrafilter monad).

[L2]

Under UL/BPI, an ultrafilter algebra maps each ultrafilter to its unique limit in the induced topology (Under the ultrafilter lemma, an ultrafilter algebra maps each ultrafilter to its unique limit).

[L3]

Every continuous map of compact Hausdorff spaces is an ultrafilter-algebra homomorphism (A continuous map of compact Hausdorff spaces is an ultrafilter-algebra homomorphism).

[L4]

Under UL/BPI, the topology induced by an ultrafilter algebra ξ:βXX is compact and Hausdorff (Under the ultrafilter lemma, every ultrafilter algebra determines a compact Hausdorff topology).

Proof

technique · direct
1.1

Starting with an algebra ξ, [L4] makes its induced topology compact Hausdorff, so the limit construction of clause 1 applies to it, and [L2] says that the unique-limit map of that topology is exactly ξ. Thus the algebra is recovered on the nose, including on an empty or singleton carrier.

L2L4
1.2

Starting with a compact Hausdorff topology τ, every τ-open set is open for the limit algebra because a convergent ultrafilter contains each neighbourhood of its limit. Conversely, if O is not a τ-neighbourhood of some xO, the neighbourhood filter at x together with XO has the finite-intersection property; UL/BPI extends it to an ultrafilter converging to x but not containing O, contradicting induced openness. Hence the rebuilt topology is exactly τ.

L1construct
1.3

The forward morphism direction is [L3]: every continuous map preserves unique ultrafilter limits and is an algebra homomorphism.

L3
1.4

Conversely, let f:(X,ξX)(Y,ξY) be an algebra homomorphism. If O is induced-open in Y and ξX(U)f1[O], then ξY(βf(U))=f(ξX(U))O, so Oβf(U) and hence f1[O]U. Thus every preimage of an induced-open set is induced-open, and f is continuous.

L2construct
2.1

Steps 1.1 and 1.2 recover both object structures, while steps 1.3 and 1.4 identify both morphism classes. The assignments therefore define inverse functors over Set.

step 1.1step 1.2step 1.3step 1.4
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Under the ultrafilter lemma, compact Hausdorff spaces are monadic over sets

Statement

Assume UL/BPI. The underlying-set functor U:CompHausSet is monadic. Its induced monad is the ultrafilter monad, and its comparison with the Eilenberg–Moore category of ultrafilter algebras is an equivalence, in fact an isomorphism over Set.

Facts & Assumptions

Given: UL/BPI and the ultrafilter monad β on Set.

[L1]

Compact Hausdorff spaces and ultrafilter algebras are recovered by inverse object and morphism constructions over Set (Under the ultrafilter lemma, compact Hausdorff spaces and ultrafilter algebras are recovered by the two limit constructions).

[L2]

The Eilenberg–Moore adjunction of a monad induces that monad on the nose (The free–forgetful Eilenberg–Moore adjunction induces the given monad).

[L3]

A right adjoint is monadic when its comparison functor is an equivalence of categories (Monadic and strictly monadic functors).

Proof

technique · direct
1.1

By [L1], the category CompHaus with its underlying-set functor is isomorphic over Set to the Eilenberg–Moore category Setβ.

L1
2.1

Transport the Eilenberg–Moore free-forgetful adjunction across this isomorphism. Its right adjoint is the compact-Hausdorff underlying-set functor.

step 1.1L2
3.1

By [L2], the monad induced by this adjunction is the ultrafilter monad on the nose.

step 2.1L2
4.1

The comparison is the isomorphism of [L1], hence an equivalence. Therefore the underlying-set functor is monadic by [L3], with UL/BPI as the only choice assumption used in [L1].

step 1.1step 3.1L3
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

A continuous bijection of compact Hausdorff spaces is a homeomorphism, by conservativity

Statement

Assume UL/BPI. Every continuous bijection between compact Hausdorff spaces is a homeomorphism.

Facts & Assumptions

Given: UL/BPI and a continuous bijection f:XY between compact Hausdorff spaces.

[L1]

Every monadic functor reflects isomorphisms (Every monadic functor is conservative).

[L2]

Under UL/BPI, compact Hausdorff spaces are monadic over sets (Under the ultrafilter lemma, compact Hausdorff spaces are monadic over sets).

[L3]

A homeomorphism is a continuous bijection whose inverse is continuous (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological).

Proof

technique · direct
1.1

By [L1] and [L2], the underlying-set functor from compact Hausdorff spaces reflects isomorphisms.

L1L2
2.1

The underlying function of f is a bijection, hence an isomorphism in Set. Conservativity from step 1.1 makes f an isomorphism in the category of compact Hausdorff spaces.

step 1.1given
3.1

The categorical inverse of f is a continuous map, so f is a continuous bijection with continuous inverse and is a homeomorphism by [L3]. This includes empty and singleton spaces.

step 2.1L3

Remarks

The same conclusion has a direct topological proof: A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism makes the inverse send closed sets to closed sets when the codomain is Hausdorff. The proof above records how the conclusion follows instead from monadic conservativity.

5 · Examples, counterexamples and false statements

CounterexampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Torsion-free abelian groups give a conservative right adjoint that is not monadic

Statement refuted

The assertion that every conservative right adjoint is monadic is false. Torsion-free abelian groups give a conservative right adjoint that is not monadic.

Facts & Assumptions

Given: The category TFAb of torsion-free abelian groups and group homomorphisms, with underlying-set functor U:TFAbSet.

[L1]

The full subcategory of torsion-free abelian groups is reflective in Ab (Torsion-free abelian groups form a reflective full subcategory of abelian groups).

[L2]

For R=Z, the Eilenberg–Moore category of the free-module monad is isomorphic over Set to the category of abelian groups (For a unital ring R, the free-R-module monad on sets has left R-modules as its Eilenberg–Moore algebras).

[L3]

A Z-module is torsion-free when no nonzero integer annihilates a nonzero element (Annihilators, torsion elements and the torsion subset of a module).

[L4]

The quotient group (Z,+)/2Z is (Z/2,+) on the same underlying congruence classes (For every nN, the congruence-class group (Z/n,+) is the quotient group (Z,+)/nZ).

Counterexample

technique · direct
1.1

Free abelian groups are torsion-free, so the usual free-abelian-group functor lands in TFAb and is left adjoint to U. Equivalently, this adjunction is obtained by combining the free-abelian adjunction with the reflective inclusion in [L1].

L1construct
1.2

A bijective homomorphism of torsion-free abelian groups has an inverse that preserves addition, so it is an isomorphism. Hence U reflects isomorphisms and is conservative.

givenalgebra
2.1

The induced monad is the usual free-abelian-group monad: applying the torsion-free reflector to a free abelian group changes nothing. By [L2], its full Eilenberg–Moore category is Ab over Set.

step 1.1L2
3.1

The comparison from TFAb to Ab is the inclusion and misses the group Z/2Z in [L4]. The nonzero class of 1 is killed by the nonzero integer 2, so this group is not torsion-free by [L3].

step 2.1L3L4construct
4.1

Thus the comparison is not essentially surjective and is not an equivalence, so U is not monadic, while step 1.2 shows it is conservative.

step 1.2step 3.1
False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

FALSE: ordinary Beck creation characterizes strict monadicity

Statement

False claim: a right adjoint is strictly monadic if and only if it creates coequalizers of its split pairs in the ordinary isomorphism-invariant sense.

Facts & Assumptions

Given: Ordinary and strict monadicity with their respective Beck conditions.

[L1]

A right adjoint is monadic when its comparison functor is an equivalence of categories and strictly monadic when that functor is an isomorphism of categories; strict monadicity implies monadicity, but the converse is not part of the definition (Monadic and strictly monadic functors).

[L2]

A monadic right adjoint creates coequalizers of its split pairs in the ordinary isomorphism-invariant sense (Beck's monadicity theorem in data-supplied form).

[L3]

An isomorphism of categories is bijective on objects and on morphisms (A functor is an isomorphism of categories exactly when its object and morphism maps are bijective).

[L4]

A functor is an equivalence exactly when it is fully faithful and split essentially surjective, and no choice principle is needed because the splitting is part of the data (A functor is an equivalence exactly when it is fully faithful and split essentially surjective, without Choice).

Refutation

technique · direct
1.1

Let D have objects tagged sets (X,i) with i{0,1} and let every morphism (X,i)(Y,j) be a function XY. The forgetful functor U:DSet has a left adjoint F(X)=(X,0).

construct
2.1

The unit and counit of this adjunction act as identity functions, so the induced monad on Set is the identity monad.

step 1.1algebra
2.2

Its object map is not injective because (X,0) and (X,1) are distinct objects with the same image. Hence the comparison is not an isomorphism by [L3] and U is not strictly monadic.

step 1.1L3
3.1

The comparison is U itself. It is fully faithful because every function XY is a morphism (X,i)(Y,j) and no two morphisms have the same underlying function, and the assignment X(X,0) splits it on objects, since U(X,0)=X on the nose. By [L4] it is therefore an equivalence, so U is monadic in the sense of [L1].

step 2.1L1L4
4.1

By [L2], ordinary Beck creation holds for this monadic right adjoint, while step 2.2 shows strict monadicity fails. Thus the implication from ordinary creation to strict monadicity is false.

step 3.1step 2.2L2
5.1

The other implication is true: strict monadicity implies monadicity by [L1], and monadicity implies ordinary creation by [L2]. Hence step 4.1 refutes exactly the reverse implication in the displayed biconditional; strict creation is the additional condition characterized by strict Beck.

step 4.1L1L2
False statementConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

FALSE: every conservative right adjoint is monadic

Statement

False claim: every conservative right adjoint is monadic.

Facts & Assumptions

Given: The underlying-set functor from torsion-free abelian groups.

[L1]

Torsion-free abelian groups give a conservative right adjoint that is not monadic (Torsion-free abelian groups give a conservative right adjoint that is not monadic).

[L2]

A conservative functor reflects isomorphisms (Conservative functor).

Refutation

technique · direct
1.1

Apply the false implication to the underlying-set functor U:TFAbSet from [L1].

L1
1.2

The functor has a left adjoint and reflects isomorphisms, so it is a conservative right adjoint and satisfies the antecedent by [L1] and [L2].

L1L2
2.1

Its comparison misses abelian groups with nonzero torsion, so [L1] says it is not monadic. The antecedent is true and the conclusion false for this functor, refuting the claim.

L1step 1.2
False statementConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

FALSE: every U-split pair is split in the domain

Statement

False claim: if a parallel pair in D is U-split for a functor U:DC, then that pair is split in D.

Facts & Assumptions

Given: The Eilenberg–Moore forgetful functor for the free-monoid monad.

[L1]

A parallel pair is U-split when its image under U extends to a split coequalizer diagram (U-split pairs and ordinary or strict creation of their coequalizers).

[L2]

The underlying canonical presentation is split in the base, but its canonical splittings need not be algebra homomorphisms (The canonical algebra presentation is split in the base, but its canonical splittings need not be algebra homomorphisms).

Refutation

technique · direct
1.1

Take the canonical presentation of the two-element monoid M={1,e} with e2=e as an algebra for the free-monoid monad. By [L1] and [L2], its underlying pair is UT-split.

L1L2
1.2

If the coequalizer evaluation MM had a monoid-homomorphic section s, then s(e)2=s(e) because e2=e. The only idempotent word in a free monoid is the empty word, since a nonempty word has positive length and its square has twice that length. But evaluation of the empty word is 1, not e, so no such section exists.

L2
2.1

Hence this pair becomes split after applying UT but is not split in the algebra category. The U-split condition therefore does not imply a splitting in the domain.

step 1.1step 1.2
False statementConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

FALSE: the underlying-set functor from topological spaces is monadic

Statement

False claim: the underlying-set functor U:TopSet is monadic.

Facts & Assumptions

Given: The underlying-set functor on topological spaces.

[L1]

Every monadic functor reflects isomorphisms (Every monadic functor is conservative).

[L2]

A continuous bijection need not be a homeomorphism; the published false statement supplies a two-point witness (FALSE: every continuous bijection of topological spaces is a homeomorphism).

[L3]

Topological spaces and continuous maps form the category Top (Topological spaces and continuous maps form the large locally small category Top).

Refutation

technique · direct
1.1

By [L1], conservativity is necessary for the underlying-set functor to be monadic.

L1
1.2

On S={a,b}, let Sd be discrete and let Ss have the Sierpiński topology {,{b},S}. The identity function q:SdSs is a continuous bijection, but its inverse is not continuous because {a} is open in Sd and not in Ss. This is the failure recorded in [L2] inside the category [L3].

L2L3
2.1

The underlying function Uq is an isomorphism in Set, while q is not an isomorphism in Top because it is not a homeomorphism. Thus U does not reflect this isomorphism.

step 1.2algebra
3.1

The functor U is not conservative by step 2.1 and therefore cannot be monadic by step 1.1.

step 1.1step 2.1

Sources