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.
Monadicity and Beck's Theorem
1 · Prerequisites
- Adjunctions Units and Counits
- Binary Operations, Monoids, Groups and Subgroups
- Cardinal Arithmetic, Cofinality and the Alephs
- Categories, Functors and Natural Transformations
- Compactness
- Compactness in Metric Spaces
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Convergence: Nets and Filters
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Free Groups and Presentations
- Free Modules, Exact Sequences, Projective and Injective Modules
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Limits and Colimits
- Metric Spaces
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Monads Comonads and Their Algebras
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Ordinal Arithmetic and the First Uncountable Ordinal
- Ordinals, Cardinals, and Transfinite Recursion
- Reflective Subcategories and the Adjoint Functor Theorems
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Set Theory Beyond Choice: Recorded, Not Proved Here
- Subspaces, Products, and Quotients
- Suprema and Infima
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Universal Properties, Representables and the Yoneda Lemma
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 -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
Absolute colimits
Definition
A colimit of a diagram in a category is absolute when every functor with domain 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.
Split coequalizer diagrams
Definition
A split coequalizer diagram consists of morphisms
such that
Thus a split coequalizer diagram has maps , , , and satisfying , , , and . The morphism is called a split coequalizer of and (Equalizers and coequalizers as limits and colimits of a parallel pair).
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 with splitting maps and .
A split coequalizer diagram has maps , , , and satisfying , , , and (Split coequalizer diagrams).
A colimit is absolute when every functor preserves it (Absolute colimits).
Proof
Let satisfy . Define . Then , using , the equality , and .
Let be any functor with the given category as domain. Functoriality sends the four equations in [L1] to , , , and , so the image diagram is again split.
If also satisfies , then because . Thus has the coequalizer universal property, including when or is an identity.
Repeating steps 1.1 and 2.1 in the target of shows that is a coequalizer of and . Since was arbitrary, every functor preserves this coequalizer, so it is absolute by [L2].
Reflexive parallel pairs and reflexive coequalizers
Definition
A parallel pair is reflexive when it has a common section: there is a morphism such that
A reflexive coequalizer is a coequalizer (Equalizers and coequalizers as limits and colimits of a parallel pair) of a reflexive parallel pair.
-split pairs and ordinary or strict creation of their coequalizers
Definition
Let be a functor. A parallel pair in is -split when its image under extends to a split coequalizer diagram in (Split coequalizer diagrams).
The functor creates coequalizers of -split pairs when each chosen split coequalizer of and is isomorphic, as a coequalizer diagram, to the image under of a coequalizer of and , 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 strictly creates coequalizers of -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.
Every algebra is the coequalizer of its canonical pair of free algebras
Statement
Let be a monad on and let be a -algebra. In the Eilenberg–Moore category , the diagram
is a coequalizer. Thus every -algebra is the coequalizer in of the canonical pair of free algebras.
Facts & Assumptions
Given: A monad and a -algebra in the Eilenberg–Moore category (Monad on a category, Eilenberg–Moore category of a monad).
A -algebra is an object with a morphism satisfying and ; a morphism satisfies (Algebra and algebra homomorphism for a monad).
The free -algebra on is , and is an algebra homomorphism between free algebras for every (Free algebra for a monad).
A coequalizer of 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
By [L2], is an algebra homomorphism. The monad associativity equation says that is also an algebra homomorphism.
The structure map is an algebra homomorphism by the algebra associativity law, and that same law gives , so coequalizes the canonical pair.
Let be an algebra homomorphism with . Define . Naturality of and the monad unit law give .
Since is an algebra homomorphism, . Hence , so is an algebra homomorphism.
If satisfies , then by the algebra unit law. Therefore has the universal property in [L3], including for initial or degenerate algebra objects, and is the claimed coequalizer.
The canonical algebra presentation is split in the base, but its canonical splittings need not be algebra homomorphisms
Statement
For every -algebra , the underlying canonical presentation
is a split coequalizer in , with and . These canonical splitting maps need not be algebra homomorphisms, so the presentation need not be split in .
Facts & Assumptions
Given: A monad and a -algebra .
Every -algebra is the coequalizer in of the canonical pair of free algebras (Every algebra is the coequalizer of its canonical pair of free algebras).
A split coequalizer diagram has maps , , , and satisfying , , , and (Split coequalizer diagrams).
The free-monoid monad inserts letters as one-letter words and flattens words of words by concatenation; its Eilenberg–Moore category is isomorphic over to the category of monoids (The free-monoid monad has monoids as its Eilenberg–Moore algebras).
Proof
The algebra law gives and . The monad unit law gives , while naturality of gives . These are exactly the four equations of [L2] for and .
For the free-monoid monad, take the monoid with . On the two-letter word , the composite first multiplies and gives the one-letter word , whereas gives the two-letter word .
Therefore the underlying canonical presentation is split in .
The equality is precisely the algebra-homomorphism equation for , and step 1.2 shows it fails.
For that same algebra no algebra section exists at all. Under the isomorphism over of [L3], an algebra map with is a monoid homomorphism from to the free monoid on the set whose composite with word evaluation is the identity. Concatenation adds word lengths, so forces and the empty word is the only idempotent of that free monoid; since in , is the empty word and evaluates to . Hence the presentation of is not split in .
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 . No failure is asserted for every monad or every algebra.
The Eilenberg–Moore forgetful functor strictly creates coequalizers of -split pairs
Statement
For every monad on , the Eilenberg–Moore forgetful functor strictly creates coequalizers of -split pairs.
Facts & Assumptions
Given: Algebra homomorphisms and a supplied split coequalizer of their underlying pair in .
The functor strictly creates coequalizers of -split pairs when every supplied splitting has a unique lift on the same apex and legs, and the lifted fork is a coequalizer (-split pairs and ordinary or strict creation of their coequalizers).
Every split coequalizer is a coequalizer and an absolute colimit (Every split coequalizer is a coequalizer and an absolute colimit).
Proof
By [L2], , , and are coequalizers of the corresponding images of . In particular each is an epimorphism, since every coequalizer is epic by its uniqueness clause.
Because and are algebra homomorphisms, coequalizes and . The universal property of gives a unique satisfying .
After precomposition with the epimorphism , the unit equation is the unit law for . After precomposition with the epimorphism , the associativity equation is the associativity law for . Hence is a -algebra.
The defining equation says exactly that is an algebra homomorphism.
If is an algebra homomorphism with , [L2] gives a unique underlying with . Precomposing and with the epimorphism gives the same map, so is an algebra homomorphism and is the unique algebraic factorization.
Any algebra structure on the supplied apex for which is an algebra homomorphism satisfies , so because is epic. Together with step 5.1 this is the unique on-the-nose lift required by [L1].
Supplied created canonical presentations give a quasi-inverse to the comparison functor
Statement
Let be an adjunction inducing the monad , and let be its comparison functor. Suppose creates coequalizers of -split pairs and, for every -algebra , a specific created coequalizer of its lifted canonical pair is supplied. Then these supplied coequalizers define a functor and natural isomorphisms
Thus is a quasi-inverse to .
Facts & Assumptions
Given: An adjunction inducing on the nose, with creating coequalizers of -split pairs.
The comparison functor is and (The comparison functor to the Eilenberg–Moore category exists and is unique).
The 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).
A parallel pair is -split when its image under extends to a split coequalizer diagram, and ordinary creation supplies and reflects the corresponding lifted coequalizer up to isomorphism (-split pairs and ordinary or strict creation of their coequalizers).
The Eilenberg–Moore forgetful functor strictly creates coequalizers of its split pairs (The Eilenberg–Moore forgetful functor strictly creates coequalizers of -split pairs).
Every -algebra is the coequalizer in of its canonical pair of free algebras (Every algebra is the coequalizer of its canonical pair of free algebras).
Proof
For a -algebra , the pair with arrows and has under the canonical pair . By [L2] and [L3] it is -split.
Let be the created coequalizer supplied for . Its image is isomorphic to the canonical base coequalizer from step 1.1, and the universal property fixes the resulting comparisons.
An algebra homomorphism carries the canonical pair for to that for . The two coequalizer universal properties therefore define a unique morphism , and uniqueness proves preservation of identities and composition.
For , the counit fork maps under to the canonical split presentation of . Creation reflects the lifted coequalizer, so comparison with yields an isomorphism .
The underlying fork of is a split coequalizer, transported from the canonical split fork along the isomorphism supplied by ordinary creation. Since is a lift of that fork, [L4] makes it a coequalizer in . The map is the other canonical algebra coequalizer by [L5], so their universal properties produce a unique isomorphism .
The defining equations for the comparisons in steps 3.3 and 3.2 commute with every algebra homomorphism and every morphism of . Uniqueness of maps out of the coequalizers therefore makes both families natural, proving the two displayed natural isomorphisms.
Beck's monadicity theorem in data-supplied form
Statement
Let be a right adjoint.
- If is monadic, then it creates coequalizers of -split pairs.
- Conversely, suppose creates coequalizers of -split pairs and, for every algebra of the induced monad, a specific created coequalizer of its lifted canonical pair is supplied. Then 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 , a left adjoint , the induced monad , and comparison functor .
The functor is monadic when its comparison functor is an equivalence of categories (Monadic and strictly monadic functors).
The Eilenberg–Moore forgetful functor strictly creates coequalizers of -split pairs (The Eilenberg–Moore forgetful functor strictly creates coequalizers of -split pairs).
If creates coequalizers of -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).
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
For the forward direction, suppose is monadic. Then is an equivalence by [L1] and . Transporting the strict-creation result [L2] across by [L4] shows that creates coequalizers of -split pairs in the ordinary sense.
For the converse, suppose creates coequalizers of -split pairs and the stated family of created canonical coequalizers is supplied. By [L3], those data define a quasi-inverse to .
A functor with a quasi-inverse and the two natural isomorphisms is an equivalence, so is an equivalence and is monadic by [L1].
Step 1.1 proves the monadic-to-creation implication, while steps 1.2 and 2.1 prove the data-supplied converse.
Strict Beck monadicity theorem
Statement
Let be a right adjoint. Then is strictly monadic if and only if it strictly creates coequalizers of -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 , a left adjoint , induced monad , and comparison functor .
The functor is strictly monadic when is an isomorphism of categories (Monadic and strictly monadic functors).
The Eilenberg–Moore forgetful functor strictly creates coequalizers of -split pairs (The Eilenberg–Moore forgetful functor strictly creates coequalizers of -split pairs).
The functor strictly creates coequalizers of -split pairs when every supplied splitting has a unique lift on the same apex and legs, and the lifted fork is a coequalizer (-split pairs and ordinary or strict creation of their coequalizers).
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).
Every -algebra is the coequalizer in of its canonical pair of free algebras (Every algebra is the coequalizer of its canonical pair of free algebras).
Proof
For the forward direction, if is an isomorphism then on the nose. Transport through the inverse functor of preserves the exact apex, legs, and uniqueness in [L2], so has the strict-creation property in [L3].
For the reverse direction, [L4] makes each lifted canonical pair -split. Strict creation [L3] gives a unique object of on the prescribed underlying apex and a coequalizer whose underlying map is . Uniqueness and the coequalizer universal property define on algebra homomorphisms.
The functor and the given algebra are lifts of the same split base fork; [L2] and the canonical coequalizer [L5] make the lift unique, so on objects and morphisms. For , its counit fork is the existing lift of the canonical split fork of , so strict uniqueness gives and the same equality on morphisms. Hence is a two-sided inverse of , and is strictly monadic by [L1].
Step 1.1 proves the forward implication and steps 1.2 and 2.1 prove the reverse implication, establishing the biconditional.
Data-supplied crude monadicity theorem for reflexive coequalizers
Statement
Let have a left adjoint. Suppose that a specific coequalizer is supplied for every reflexive pair in , that preserves these coequalizers, and that reflects isomorphisms. Then is monadic.
Facts & Assumptions
Given: An adjunction satisfying the three hypotheses in the Statement, with induced monad and comparison functor .
A parallel pair is reflexive when it has a common section with (Reflexive parallel pairs and reflexive coequalizers).
A conservative functor reflects isomorphisms (Conservative functor).
The 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).
Every -algebra is the coequalizer in of its canonical pair of free algebras (Every algebra is the coequalizer of its canonical pair of free algebras).
The Eilenberg–Moore forgetful functor strictly creates coequalizers of its split pairs (The Eilenberg–Moore forgetful functor strictly creates coequalizers of -split pairs).
Proof
For a -algebra , the pair used in canonical reconstruction has common section : one composite is the algebra unit law and the other is the adjunction triangle identity. Hence it is reflexive by [L1].
Use the supplied coequalizer of this reflexive pair. By hypothesis, applying preserves it.
The preserved coequalizer and the split canonical base coequalizer in [L3] coequalize the same pair, so transport of the splitting makes the underlying fork of split. By [L5], is a coequalizer in ; by [L4], so is the canonical fork ending at . Their universal properties therefore give an isomorphism .
For , compare the coequalizer of the reflexive counit pair with the counit fork ending at . Their images under are isomorphic canonical coequalizers, so the comparison morphism becomes an isomorphism under and is itself an isomorphism by [L2].
The supplied object assignment and coequalizer universality define on algebra homomorphisms, and uniqueness makes the comparisons in steps 3.1 and 4.1 natural. Thus is a quasi-inverse to , so is an equivalence and is monadic.
Groups are strictly monadic over sets
Statement
The underlying-set functor is strictly monadic, and hence monadic.
Facts & Assumptions
Given: The free-group adjunction and its comparison functor.
The Eilenberg–Moore category of the free-group monad is isomorphic over to the category of groups (The free-group monad has groups as its Eilenberg–Moore algebras).
A functor is strictly monadic when its comparison functor is an isomorphism of categories (Monadic and strictly monadic functors).
The comparison functor is and acts on morphisms by (The comparison functor to the Eilenberg–Moore category exists and is unique).
Choosing a free group on every set makes left adjoint to the underlying-set functor , the adjunction bijection sending to (The free-group functor is left adjoint to the underlying-set functor).
An algebra for a monad satisfies and , and an algebra homomorphism is a map commuting with the two structure maps (Algebra and algebra homomorphism for a monad).
Proof
By [L3], and . Under [L4] the counit corresponds to the identity of , so it is the unique group homomorphism carrying each basis element to ; a homomorphism out of a free group is determined by its values on the basis, so evaluates a reduced word in the elements of to its product in . Hence is the underlying set of with word evaluation.
A function commutes with word evaluation exactly when it is a group homomorphism: evaluating the words , the empty word and turns commutation into preservation of product, identity and inverse, and conversely a homomorphism preserves the value of every word. With [L5] and this makes bijective on the morphisms between any two groups.
is injective on objects, since step 1.1 recovers the product of from as its value on two-letter words.
is surjective on objects. Let be an algebra for the free-group monad. Put , and . Writing a word as the concatenation of its first letter with its tail and applying the multiplication law of [L5] to the corresponding word of words gives , while the unit law gives ; induction on length therefore identifies 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 group with , that is .
By steps 2.1, 2.2 and 2.3 the comparison is bijective on objects and on morphisms, hence an isomorphism of categories over ; the isomorphism over asserted by [L1] may therefore be taken to be . So is strictly monadic by [L2], and strict monadicity implies monadicity.
Modules over a fixed unital ring are strictly monadic over sets
Statement
For every fixed unital ring , the underlying-set functor is strictly monadic, and hence monadic.
Facts & Assumptions
Given: A fixed unital ring and the free-left--module adjunction.
The Eilenberg–Moore category of the free-left--module monad is isomorphic over to the category of left -modules (For a unital ring R, the free-R-module monad on sets has left R-modules as its Eilenberg–Moore algebras).
A functor is strictly monadic when its comparison functor is an isomorphism of categories (Monadic and strictly monadic functors).
The comparison functor is and acts on morphisms by (The comparison functor to the Eilenberg–Moore category exists and is unique).
Proof
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.
The comparison is therefore an isomorphism over , so the underlying-set functor is strictly monadic by [L2].
Integer-valued finite formal sums of words form unital convolution rings
Statement
For a set , let be its finite-word monoid and let
With pointwise addition and convolution
this is a unital ring. Its multiplicative identity is the basis vector supported at the empty word. When , the construction is canonically .
Facts & Assumptions
Given: A set , its finite-word monoid , and the displayed convolution formula.
The assignment is the finite-word monoid functor (The free-monoid functor is left adjoint to the underlying-set functor).
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).
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
Regard as the free abelian group on the words. Define the product by bilinearly extending concatenation of basis words, equivalently by the displayed coefficient formula.
A finite word has only finitely many cuts , 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.
For , both coefficients of and are the sum of over triples with . The two bracketings are bijective reindexings of the same finite set, so [L3] proves associativity.
Splitting finite sums termwise proves and . Together with the pointwise abelian-group structure over , these are both distributive laws.
Let be on the empty word and elsewhere. The only contributing cut with a nonzero factor is or , so . This verifies the multiplicative identity and all ring laws. If , then and the coefficient at identifies the ring with .
The free unital ring functor is left adjoint to the underlying-set functor
Statement
The free-word-ring construction extends to a functor left adjoint to the underlying-set functor. Its unit sends to the basis element of the one-letter word .
Facts & Assumptions
Given: A set , its free word ring, a unital ring , and a function .
For every set , integer-valued finite formal sums of words in form a unital ring (Integer-valued finite formal sums of words form unital convolution rings).
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).
Supplied objectwise universal arrows assemble uniquely into a left adjoint (Chosen objectwise universal arrows assemble uniquely into a left adjoint).
Proof
Send a word to in , and send the empty word to . The generator is represented by the basis word .
Apply [L2] over to extend this word-evaluation function uniquely to a -linear map .
Expanding convolution as a finite sum shows , and the empty-word basis vector maps to . Thus is a unit-preserving ring homomorphism, including when is the zero ring.
Any ring homomorphism extending must send every word basis vector to the corresponding product and is additive, so it equals by uniqueness in [L2].
Hence the generator inclusion is a universal arrow from every set to the underlying-set functor on rings. By [L3] these universal arrows assemble into the free-ring functor and the asserted adjunction; for the free ring is .
The underlying-set functor on unital rings strictly creates split coequalizers
Statement
The underlying-set functor strictly creates coequalizers of -split pairs of unital ring homomorphisms.
Facts & Assumptions
Given: Ring homomorphisms and a supplied split coequalizer of their underlying functions.
A split coequalizer has splitting maps satisfying , , , and (Split coequalizer diagrams).
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).
A ring homomorphism preserves addition, multiplication, and the multiplicative identity (Ring homomorphism: additive, multiplicative, and required to send to ).
Every split coequalizer is a coequalizer and is preserved by every functor (Every split coequalizer is a coequalizer and an absolute colimit).
Proof
By [L4], each finite Cartesian power is the coequalizer of .
Each basic ring operation on , followed by , coequalizes the appropriate finite powers of and . It therefore descends uniquely to ; explicitly , , and negation, addition, and multiplication are the unique operations making preserve them.
Each ring axiom in [L2] becomes true after precomposition with the relevant surjection , because it then becomes the corresponding axiom in . Hence the descended operations make a unital ring, including the zero-ring case.
By construction preserves addition, multiplication, and one, so it is a ring homomorphism by [L3].
If a ring homomorphism coequalizes , the set coequalizer gives a unique with . Precomposing the preservation equations for with the appropriate reduces them to those for , so is a ring homomorphism and is the unique algebraic factor.
The descended operations are uniquely forced by the requirement that the supplied be a ring homomorphism. Thus the lift has exactly the same apex and legs and is unique, which is strict creation.
Monoids and unital rings are strictly monadic over sets
Statement
The underlying-set functors from monoids and from unital rings to are strictly monadic, and hence monadic.
Facts & Assumptions
Given: The free-monoid and free-ring adjunctions.
The Eilenberg–Moore category of the free-monoid monad is isomorphic over to the category of monoids (The free-monoid monad has monoids as its Eilenberg–Moore algebras).
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).
The underlying-set functor on unital rings strictly creates split coequalizers (The underlying-set functor on unital rings strictly creates split coequalizers).
A right adjoint is strictly monadic if and only if it strictly creates coequalizers of its split pairs (Strict Beck monadicity theorem).
Choosing a free monoid on every set makes the finite-word functor left adjoint to the underlying-set functor, the adjunction bijection sending to (The free-monoid functor is left adjoint to the underlying-set functor).
The comparison functor is and (The comparison functor to the Eilenberg–Moore category exists and is unique).
An algebra for a monad satisfies and , and an algebra homomorphism is a map commuting with the two structure maps (Algebra and algebra homomorphism for a monad).
Proof
By [L6], the comparison for the free-monoid adjunction is with . Under [L5] the counit corresponds to the identity of , so it is the unique monoid homomorphism carrying each one-letter word to ; a homomorphism out of a free monoid is determined on the letters, so evaluates a word in the elements of to its product.
For rings, [L2] supplies the left adjoint and [L3] supplies strict creation of the required split coequalizers.
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.
A function 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 this makes bijective on morphisms. It is injective on objects because step 1.1 recovers the product of from on two-letter words.
is surjective on objects: for an algebra of the free-monoid monad put and . Splitting a word into its first letter and its tail and applying the multiplication law of [L7] gives , while the unit law gives ; induction on length identifies with evaluation of words in these operations, and substituting the monoid-word identities into the same law gives associativity and the unit laws. Hence is a monoid with , that is .
By steps 2.2 and 2.3 the monoid comparison is bijective on objects and morphisms, hence an isomorphism of categories over — 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.
-sets are strictly monadic over sets
Statement
For a fixed group , the underlying-set functor from the category of left -sets and equivariant maps to is strictly monadic.
Facts & Assumptions
Given: A fixed group with identity .
A left -action satisfies and (Left group actions, transitive actions, and faithful actions).
A map of -sets is equivariant when for every (Equivariant maps and isomorphisms of group actions).
A -algebra structure satisfies and , and an algebra homomorphism satisfies the corresponding square (Algebra and algebra homomorphism for a monad).
A functor is strictly monadic when its comparison with the Eilenberg–Moore category is an isomorphism (Monadic and strictly monadic functors).
Proof
Define with action . A function into a -set extends uniquely to the equivariant map , whose inverse correspondence evaluates at . This natural bijection gives the free-action adjunction .
Its induced monad is , with , , and . The group identity and associativity laws verify the monad equations.
A map satisfies the two algebra laws in [L3] exactly when and , which are the action laws in [L1]. This includes the empty set, the trivial group, and trivial actions.
The algebra-homomorphism equation is , exactly the equivariance condition in [L2].
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 , so the underlying-set functor is strictly monadic by [L4].
Direct and inverse image satisfy Beck–Chevalley for pullback squares of sets
Statement
Let
be a pullback square of sets. For every ,
Equivalently, direct image and inverse image satisfy on power sets. The formula remains valid for empty fibres and identity pullbacks.
Facts & Assumptions
Given: The displayed pullback square and a subset .
A pullback of has projections satisfying and the universal property for every compatible pair (Pullbacks and pushouts as limits and colimits of cospans and spans).
Membership in a direct image or inverse image is witnessed by the corresponding relation equation (The image and the preimage of a set under a relation).
Proof
If , then some satisfies and . The pullback equation gives , so and .
Conversely, if , choose with . The pullback universal property supplies the unique with and , so . If the fibre is empty, both existential conditions fail.
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.
The contravariant power-set functor is monadic
Statement
The contravariant power-set functor
is monadic.
Facts & Assumptions
Given: The contravariant power-set functor between and .
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).
A conservative functor reflects isomorphisms (Conservative functor).
Direct and inverse image satisfy Beck–Chevalley for pullback squares of sets (Direct and inverse image satisfy Beck–Chevalley for pullback squares of sets).
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).
Every small diagram in has a limit (Set has all small limits, realized as compatible tuples in a set-indexed product).
Proof
A function is the same as a relation . Transposing gives a function , and transposition is natural and involutive. By [L1] this makes the power-set functor on the opposite side its own left adjoint.
If is bijective, then is surjective because otherwise and a singleton outside have the same preimage. It is injective because surjectivity of realizes each singleton of as a preimage, which separates points with different singleton membership. Thus is bijective and the functor is conservative by [L2], including when is empty.
A reflexive pair in corresponds to maps in with a common retraction , so . Define and let 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 .
The square with both left and top maps , and with bottom and right maps , is a pullback: if , applying gives . Hence [L3] gives for every ; the last equality also follows directly, while because .
Let satisfy . Applying this equality to and using step 2.1 gives . Define by . Then , and this factorization is unique because is surjective. Thus is the coequalizer of , so the power-set functor preserves every reflexive coequalizer in .
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 is monadic.
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 is finitary when its underlying endofunctor is finitary (Monad on a category). No preservation claim is imposed on the unit or multiplication separately.
Categories of models for algebraic theories
Definition
A category of models for an algebraic theory is a category equipped with a monadic functor whose induced monad on is finitary (Monadic and strictly monadic functors, Finitary functors and finitary monads).
Equivalently, up to the comparison equivalence over , 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.
Over a cocomplete base, a monadic category is cocomplete exactly when it has coequalizers
Statement
Let be monadic and suppose is cocomplete. Then is cocomplete if and only if has coequalizers.
Facts & Assumptions
Given: A monadic functor with cocomplete base and induced monad .
A category is cocomplete when every small diagram in it has a colimit (Finite, small, and large limits and colimits; complete and cocomplete categories).
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).
An equivalence of categories preserves and reflects every existing colimit (Equivalences preserve, reflect, and create limits and colimits in the isomorphism-invariant sense).
Every -algebra is the coequalizer in of the canonical pair (Every algebra is the coequalizer of its canonical pair of free algebras).
The free -algebra functor is left adjoint to the Eilenberg–Moore forgetful functor (The free–forgetful Eilenberg–Moore adjunction induces the given monad).
Left adjoints preserve every colimit that exists (Left adjoints preserve every colimit that exists).
Proof
For the forward direction, if is cocomplete then it has the colimit of every parallel pair, hence every coequalizer.
For the reverse direction, replace across its monadic comparison equivalence by . Given a small family , [L5] and [L6] identify the coproducts of free algebras with free algebras on the corresponding base coproducts. If and are their coproduct injections, define by By hypothesis this pair has a coequalizer in . The construction also applies to the empty family.
For every , the map coequalizes the canonical pair for . Its universal property [L4] gives a unique algebra map satisfying .
Given algebra maps , the maps assemble to a map . Each coequalizes its canonical pair by [L4], so and there is a unique with . Then because the two maps agree after the epimorphism , and uniqueness follows because the are jointly epimorphic. Thus is the coproduct of the family.
For the reverse direction, now has all small coproducts by step 3.1 and all coequalizers by hypothesis, so [L2] constructs every small colimit.
For the reverse direction, transport these colimits back across the comparison equivalence by [L3]. Thus is cocomplete.
Step 1.1 proves the forward implication, while steps 1.2 to 5.1 prove the reverse implication, establishing the biconditional.
Under dependent choice, algebras for a finitary monad on a complete cocomplete locally small category have coequalizers
Statement
Assume dependent choice. If is a finitary monad on a complete, cocomplete, locally small category , then the Eilenberg–Moore category has coequalizers.
Facts & Assumptions
Given: Dependent choice, a complete cocomplete locally small category , a finitary monad , and algebra homomorphisms .
A functor is finitary when it preserves every small filtered colimit (Finitary functors and finitary monads).
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 -indexed chain).
Let have complete locally small domain and be continuous. If satisfies the solution-set condition at , then has an initial object, equivalently a universal arrow from to (General adjoint functor theorem, objectwise initial-object form).
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).
If and the indexing category are small and chosen limits of the pointwise diagrams exist, those choices form a limit in (For small source and index categories, chosen target limits and colimits compute the corresponding functor-category limits and colimits pointwise).
Proof
In , form , the coequalizer of , and , the coequalizer of . Their universal properties induce maps and characterized by and . Both and are epimorphisms.
The category is complete by [L4] and locally small because its hom-sets are subsets of those of . 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.
Suppose has been constructed with and . Put , and choose as a coequalizer of . Define , , , and . Naturality of and the monad unit law give . Consequently and .
Let be any algebra homomorphism with . Factor it uniquely as . Precomposing with the epimorphism and using step 1.1 gives .
To justify the countable sequence of choices in step 2.1, encode each finite stage by a set. For a state , let be all valid successor codes of least possible von Neumann rank; it is a nonempty subset of some , hence a set. Starting with the code from step 1.1, recursively close under for finitely many steps and take the union over . 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.
Suppose satisfies . The algebra law for shows that coequalizes and , so it factors uniquely through as a map with . The definitions in step 2.1 then give and , closing the induction.
Form the sequential colimits and , with injections and . The identities make the a map of the two sequential diagrams, hence induce . The compatible induce . The shifted identities and identify with .
The natural-number indexing category is filtered, so finitarity [L1] identifies the colimit in step 4.1 with . Make this identification, so and the induced comparison is the identity. Thus .
For every , naturality of and the definition of give . The colimit injections are jointly epimorphic, so .
The compatible induce . Passing the equations to the colimit gives , and compatibility at stage zero gives .
The successor coequalizer equations are . Passing these compatible equations to the filtered colimit gives because in step 5.1. Together with step 6.1, this makes a -algebra.
Passing and to the colimit gives , so is an algebra homomorphism; it coequalizes because does.
By steps 6.2 and 7.1, is an algebra homomorphism, and step 6.2 gives . Therefore the single algebra fork is a solution set for the constant-diagram functor at the given parallel pair: every algebra fork factors through it, without a uniqueness assertion.
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 in . Since the pair was arbitrary, all coequalizers exist.
Under dependent choice, a finitary monad on a complete cocomplete locally small category has complete and cocomplete algebras
Statement
Assume dependent choice. If is a finitary monad on a complete, cocomplete, locally small category , then its Eilenberg–Moore category 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 on a complete cocomplete locally small category .
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).
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).
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).
The Eilenberg–Moore adjunction induces the given monad on the nose (The free–forgetful Eilenberg–Moore adjunction induces the given monad).
Proof
Since has every small limit, [L1] creates every such limit in , including the empty limit. Thus is complete without using dependent choice.
Under the stated dependent-choice hypothesis, [L2] gives every coequalizer in , including equal parallel maps and the zero-stage case of its construction.
By [L4], the Eilenberg–Moore adjunction induces on the nose, so its forgetful functor is monadic. Applying [L3] to the cocomplete base and step 1.2 makes cocomplete, including the empty colimit.
Combining step 1.1 with step 2.1 proves that is complete and cocomplete.
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 of models for an algebraic theory.
A category of models for an algebraic theory is equipped with a finitary monadic functor to (Categories of models for algebraic theories).
Every small diagram in has a limit (Set has all small limits, realized as compatible tuples in a set-indexed product).
Every small diagram in has a colimit (Set has all small colimits, realized as a quotient of a set-indexed disjoint union).
Equivalences preserve and reflect existing limits and colimits (Equivalences preserve, reflect, and create limits and colimits in the isomorphism-invariant sense).
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
By [L2] and [L3], is complete and cocomplete; it is locally small because each function collection between two sets is a set. This includes empty diagrams.
The finitary monad induced by [L1] satisfies the hypotheses of [L5], so under dependent choice its Eilenberg–Moore category is complete and cocomplete.
The comparison supplied by [L1] is an equivalence over . Transporting the limits and colimits of step 2.1 across it by [L4] proves that is complete and cocomplete.
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.
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 and an ultrafilter on .
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).
Every cluster point of an ultrafilter is a limit of that ultrafilter (Every cluster point of an ultrafilter is a limit of that ultrafilter).
Distinct points in a Hausdorff space have disjoint open neighbourhoods (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not).
Proof
The closed members of have the finite-intersection property: a finite intersection remains in the filter and cannot be empty.
By compactness and [L1], choose a point in the intersection of all closed members of . If , no ultrafilter exists, so the universal assertion is vacuous.
For every , its closure also belongs to and contains ; hence every neighbourhood of meets every member of . Thus is a cluster point and therefore a limit by [L2].
If and were distinct limits, [L3] would give disjoint open neighbourhoods of and of . Both would belong to , forcing into the filter, a contradiction. Hence the limit is unique, including in a singleton space.
The ultrafilter-limit map of a compact Hausdorff space is an algebra for the ultrafilter monad
Statement
Let be compact Hausdorff, and define by sending each ultrafilter to its unique limit. Then is an algebra for the ultrafilter monad:
Facts & Assumptions
Given: A compact Hausdorff space and its ultrafilter-limit map .
Every ultrafilter on a compact Hausdorff space has exactly one limit (A given ultrafilter on a compact Hausdorff space has a unique limit).
The ultrafilter monad has principal unit and flattening multiplication , where (The ultrafilter endofunctor with principal unit and flattening multiplication).
A -algebra structure satisfies and (Algebra and algebra homomorphism for a monad).
Proof
By [L1], is defined on every ultrafilter. When , both and are empty and the unique empty map satisfies the equations below.
The principal ultrafilter contains every neighbourhood of , so it converges to . Uniqueness in [L1] gives for every .
Let be an ultrafilter on . If an open neighbourhood of a point belongs to the pushforward , then . Every ultrafilter whose limit lies in contains , so ; upward closure gives , hence by [L2]. Thus every limit of the pushforward is a limit of the flattening.
Both ultrafilters in step 2.2 have unique limits by [L1], so their limits coincide: .
Steps 2.1 and 3.1 are exactly the unit and multiplication equations in [L3], so is an ultrafilter algebra.
A continuous map of compact Hausdorff spaces is an ultrafilter-algebra homomorphism
Statement
Let be continuous between compact Hausdorff spaces, and let be their ultrafilter-limit maps. Then
so is an ultrafilter-algebra homomorphism.
Facts & Assumptions
Given: A continuous map of compact Hausdorff spaces and an ultrafilter on .
The pushforward is an ultrafilter on , and ultrafilter pushforward is functorial (Pushforward sends ultrafilters to ultrafilters and is functorial).
Every ultrafilter on a compact Hausdorff space has exactly one limit (A given ultrafilter on a compact Hausdorff space has a unique limit).
A -algebra homomorphism satisfies (Algebra and algebra homomorphism for a monad).
Proof
Push forward along to the ultrafilter on supplied by [L1].
If converges to , then for each neighbourhood of , continuity makes a neighbourhood of and hence a member of . Therefore , so the pushforward converges to .
Taking , uniqueness in the target gives .
Since , step 3.1 is the equation in [L3]. Thus is an algebra homomorphism, including for the unique map from an empty compact space.
The open-set family induced by an ultrafilter algebra
Definition
Let 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 by The ultrafilter endofunctor with principal unit and flattening multiplication is a monad. A subset is -open, or induced-open, when
for every ultrafilter on . 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 ↗.
The open-set family induced by an ultrafilter algebra is a topology
Statement
For every ultrafilter algebra , the family of induced-open subsets is a topology on .
Facts & Assumptions
Given: An ultrafilter algebra and its induced-open family .
A subset is induced-open when implies for every ultrafilter on (The open-set family induced by an ultrafilter algebra).
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
The empty set is induced-open because its antecedent never holds, and is induced-open because every ultrafilter contains .
Let be induced-open and suppose . Some contains , hence by [L1], and upward closure gives . Thus arbitrary unions are induced-open.
If and are induced-open and , then by [L1], so . This also covers the empty and singleton finite intersections using step 1.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.
Under the ultrafilter lemma, closure in an ultrafilter-algebra topology is the image of ultrafilters containing the set
Statement
Assume UL/BPI. Let be an ultrafilter algebra, give its induced topology, and put
Then for every ,
Facts & Assumptions
Given: UL/BPI, an ultrafilter algebra , its induced topology, and a subset .
The closure of is the smallest closed subset containing (Interior, closure, boundary, exterior, derived set and isolated point in a topological space).
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)).
Flattening satisfies exactly when (The ultrafilter endofunctor with principal unit and flattening multiplication).
An ultrafilter contains exactly one of and for every (Characterisation of ultrafilters: every set or its complement).
Proof
If , its principal ultrafilter contains and the algebra unit law gives . Hence ; when , no ultrafilter contains it and both sides of this inclusion are empty.
A set is induced-closed exactly when every ultrafilter containing has its algebra value in : this is the complement of the defining induced-open implication, using [L4].
Put and fix an ultrafilter with . On , the family consisting of and all for has the finite-intersection property: for a finite intersection of members of , choose and then an ultrafilter in mapping to . By [L2], extend this family to an ultrafilter on .
Since , [L3] gives . Since every with lies in , maximality gives . The algebra multiplication law yields . Thus is induced-closed by step 1.2.
If is any induced-closed superset of , every ultrafilter containing contains , so step 1.2 gives . By steps 1.1 and 3.1, is itself a closed superset of , hence it is the closure by [L1]. This also gives .
Under the ultrafilter lemma, an ultrafilter algebra maps each ultrafilter to its unique limit
Statement
Assume UL/BPI. For an ultrafilter algebra with its induced topology, every ultrafilter converges to exactly one point, namely .
Facts & Assumptions
Given: UL/BPI, an ultrafilter algebra , and an ultrafilter on .
In the induced topology, the closure of is (Under the ultrafilter lemma, closure in an ultrafilter-algebra topology is the image of ultrafilters containing the set).
A filter converges to when every neighbourhood of belongs to the filter (Convergence and cluster points of a filter on a topological space).
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
If an induced-open neighbourhood contains , the definition of induced-open gives . Thus converges to by [L2].
Let be any limit of . For each , every neighbourhood of meets , so by [L1].
On , the family has the finite-intersection property by step 1.2. Extend it by [L3] to an ultrafilter on .
The inclusions forced by step 2.1 and maximality give and . The algebra laws therefore give .
Step 1.1 supplies the limit and step 3.1 identifies every other limit with it, proving existence and uniqueness. If , no ultrafilter exists and the assertion is vacuous.
Under the ultrafilter lemma, every ultrafilter algebra determines a compact Hausdorff topology
Statement
Assume UL/BPI. For every ultrafilter algebra , the topology induced by is compact and Hausdorff.
Facts & Assumptions
Given: UL/BPI and an ultrafilter algebra .
The open-set family induced by an ultrafilter algebra is a topology (The open-set family induced by an ultrafilter algebra is a topology).
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).
Under the ultrafilter lemma, a space is compact if and only if every ultrafilter on it converges (Assuming the ultrafilter lemma, compactness is equivalent to every net having a cluster point, every net having a convergent subnet, every filter having a cluster point, and every ultrafilter converging).
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
Equip with the topology supplied by [L1].
By [L2], every ultrafilter on converges, and its limit is unique.
The equivalence in [L3] applied to step 1.2 proves that the induced topology is compact.
If distinct 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 and , contradicting uniqueness in step 1.2. Hence the topology is Hausdorff, with the empty and singleton cases vacuous.
Steps 2.1 and 2.2 prove that the induced topology is compact Hausdorff.
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:
- a compact Hausdorff space is sent to the ultrafilter algebra whose structure map takes each ultrafilter to its unique limit;
- an ultrafilter algebra 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 .
Facts & Assumptions
Given: UL/BPI, the limit-algebra construction on compact Hausdorff spaces, and the induced-topology construction on ultrafilter algebras.
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).
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).
Every continuous map of compact Hausdorff spaces is an ultrafilter-algebra homomorphism (A continuous map of compact Hausdorff spaces is an ultrafilter-algebra homomorphism).
Under UL/BPI, the topology induced by an ultrafilter algebra is compact and Hausdorff (Under the ultrafilter lemma, every ultrafilter algebra determines a compact Hausdorff topology).
Proof
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.
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 is not a -neighbourhood of some , the neighbourhood filter at together with has the finite-intersection property; UL/BPI extends it to an ultrafilter converging to but not containing , contradicting induced openness. Hence the rebuilt topology is exactly .
The forward morphism direction is [L3]: every continuous map preserves unique ultrafilter limits and is an algebra homomorphism.
Conversely, let be an algebra homomorphism. If is induced-open in and , then , so and hence . Thus every preimage of an induced-open set is induced-open, and is continuous.
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 .
Under the ultrafilter lemma, compact Hausdorff spaces are monadic over sets
Statement
Assume UL/BPI. The underlying-set functor 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 .
Facts & Assumptions
Given: UL/BPI and the ultrafilter monad on .
Compact Hausdorff spaces and ultrafilter algebras are recovered by inverse object and morphism constructions over (Under the ultrafilter lemma, compact Hausdorff spaces and ultrafilter algebras are recovered by the two limit constructions).
The Eilenberg–Moore adjunction of a monad induces that monad on the nose (The free–forgetful Eilenberg–Moore adjunction induces the given monad).
A right adjoint is monadic when its comparison functor is an equivalence of categories (Monadic and strictly monadic functors).
Proof
By [L1], the category with its underlying-set functor is isomorphic over to the Eilenberg–Moore category .
Transport the Eilenberg–Moore free-forgetful adjunction across this isomorphism. Its right adjoint is the compact-Hausdorff underlying-set functor.
By [L2], the monad induced by this adjunction is the ultrafilter monad on the nose.
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].
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 between compact Hausdorff spaces.
Every monadic functor reflects isomorphisms (Every monadic functor is conservative).
Under UL/BPI, compact Hausdorff spaces are monadic over sets (Under the ultrafilter lemma, compact Hausdorff spaces are monadic over sets).
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
By [L1] and [L2], the underlying-set functor from compact Hausdorff spaces reflects isomorphisms.
The underlying function of is a bijection, hence an isomorphism in . Conservativity from step 1.1 makes an isomorphism in the category of compact Hausdorff spaces.
The categorical inverse of is a continuous map, so is a continuous bijection with continuous inverse and is a homeomorphism by [L3]. This includes empty and singleton spaces.
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
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 of torsion-free abelian groups and group homomorphisms, with underlying-set functor .
The full subcategory of torsion-free abelian groups is reflective in (Torsion-free abelian groups form a reflective full subcategory of abelian groups).
For , the Eilenberg–Moore category of the free-module monad is isomorphic over 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).
A -module is torsion-free when no nonzero integer annihilates a nonzero element (Annihilators, torsion elements and the torsion subset of a module).
The quotient group is on the same underlying congruence classes (For every , the congruence-class group is the quotient group ).
Counterexample
Free abelian groups are torsion-free, so the usual free-abelian-group functor lands in and is left adjoint to . Equivalently, this adjunction is obtained by combining the free-abelian adjunction with the reflective inclusion in [L1].
A bijective homomorphism of torsion-free abelian groups has an inverse that preserves addition, so it is an isomorphism. Hence reflects isomorphisms and is conservative.
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 over .
The comparison from to is the inclusion and misses the group in [L4]. The nonzero class of is killed by the nonzero integer , so this group is not torsion-free by [L3].
Thus the comparison is not essentially surjective and is not an equivalence, so is not monadic, while step 1.2 shows it is conservative.
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.
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).
A monadic right adjoint creates coequalizers of its split pairs in the ordinary isomorphism-invariant sense (Beck's monadicity theorem in data-supplied form).
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).
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
Let have objects tagged sets with and let every morphism be a function . The forgetful functor has a left adjoint .
The unit and counit of this adjunction act as identity functions, so the induced monad on is the identity monad.
Its object map is not injective because and are distinct objects with the same image. Hence the comparison is not an isomorphism by [L3] and is not strictly monadic.
The comparison is itself. It is fully faithful because every function is a morphism and no two morphisms have the same underlying function, and the assignment splits it on objects, since on the nose. By [L4] it is therefore an equivalence, so is monadic in the sense of [L1].
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.
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.
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.
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).
A conservative functor reflects isomorphisms (Conservative functor).
Refutation
Apply the false implication to the underlying-set functor from [L1].
The functor has a left adjoint and reflects isomorphisms, so it is a conservative right adjoint and satisfies the antecedent by [L1] and [L2].
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.
FALSE: every -split pair is split in the domain
Statement
False claim: if a parallel pair in is -split for a functor , then that pair is split in .
Facts & Assumptions
Given: The Eilenberg–Moore forgetful functor for the free-monoid monad.
A parallel pair is -split when its image under extends to a split coequalizer diagram (-split pairs and ordinary or strict creation of their coequalizers).
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
Take the canonical presentation of the two-element monoid with as an algebra for the free-monoid monad. By [L1] and [L2], its underlying pair is -split.
If the coequalizer evaluation had a monoid-homomorphic section , then because . 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 , not , so no such section exists.
Hence this pair becomes split after applying but is not split in the algebra category. The -split condition therefore does not imply a splitting in the domain.
FALSE: the underlying-set functor from topological spaces is monadic
Statement
False claim: the underlying-set functor is monadic.
Facts & Assumptions
Given: The underlying-set functor on topological spaces.
Every monadic functor reflects isomorphisms (Every monadic functor is conservative).
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).
Topological spaces and continuous maps form the category (Topological spaces and continuous maps form the large locally small category ).
Refutation
By [L1], conservativity is necessary for the underlying-set functor to be monadic.
On , let be discrete and let have the Sierpiński topology . The identity function is a continuous bijection, but its inverse is not continuous because is open in and not in . This is the failure recorded in [L2] inside the category [L3].
The underlying function is an isomorphism in , while is not an isomorphism in because it is not a homeomorphism. Thus does not reflect this isomorphism.
The functor is not conservative by step 2.1 and therefore cannot be monadic by step 1.1.
Sources
- E. Riehl, Category Theory in Context, 2nd ed., Exercise 3.4.vi(iii) and Lemma 5.4.6
- E. Riehl, Category Theory in Context, 2nd ed., Definition 5.4.4
- S. Mac Lane, Categories for the Working Mathematician, 2nd ed., Section VI.6
- E. Riehl, Category Theory in Context, 2nd ed., Lemma 5.4.6
- E. Riehl, Category Theory in Context, 2nd ed., Proposition 5.5.8
- E. Riehl, Category Theory in Context, 2nd ed., Definition 5.4.8
- E. Riehl, Category Theory in Context, 2nd ed., Proposition 5.4.2
- E. Riehl, Category Theory in Context, 2nd ed., Example 5.4.7
- E. Riehl, Category Theory in Context, 2nd ed., Proposition 5.4.10
- E. Riehl, Category Theory in Context, 2nd ed., proof of Theorem 5.5.1
- E. Riehl, Category Theory in Context, 2nd ed., Theorem 5.5.1
- D. Mehrle, Category Theory Part III, Theorem 5.16
- S. Mac Lane, Categories for the Working Mathematician, 2nd ed., Theorem VI.7.1
- E. Riehl, Category Theory in Context, 2nd ed., Exercise 5.5.i
- E. Riehl, Category Theory in Context, 2nd ed., Example 5.1.4(iv) and Corollary 5.5.3(i)
- E. Riehl, Category Theory in Context, 2nd ed., Example 5.1.4(iii) and Corollary 5.5.3(ii)
- E. Riehl, Category Theory in Context, 2nd ed., Corollary 5.5.3
- E. Riehl, Category Theory in Context, 2nd ed., Example 4.1.10(vi)
- D. Mehrle, Category Theory Part III, Example 5.18
- D. Mehrle, Category Theory Part III, Example 5.20(b)
- E. Riehl, Category Theory in Context, 2nd ed., Corollary 5.5.3(ii) and Exercise 5.5.iv
- E. Riehl, Category Theory in Context, 2nd ed., Lemma 5.5.10
- D. Mehrle, Category Theory Part III, Exercise 5.22
- E. Riehl, Category Theory in Context, 2nd ed., Theorem 5.5.9
- D. Mehrle, Category Theory Part III, Theorem 5.21
- E. Riehl, Category Theory in Context, 2nd ed., Definition 5.5.4
- E. Riehl, Category Theory in Context, 2nd ed., Definition 5.5.5
- E. Riehl, Category Theory in Context, 2nd ed., Proposition 5.6.11
- E. Riehl, Category Theory in Context, 2nd ed., proof of Theorem 5.6.12
- E. Riehl, Category Theory in Context, 2nd ed., Theorem 5.6.12
- E. Riehl, Category Theory in Context, 2nd ed., Corollary 5.6.14
- J. Goubault-Larrecq, Algebras of filter-related monads: I. Ultrafilters and Manes' theorem
- E. Riehl, Category Theory in Context, 2nd ed., Corollary 5.5.6
- J. Goubault-Larrecq, Algebras of filter-related monads: I. Ultrafilters and Manes' theorem, Lemma A
- J. Goubault-Larrecq, Algebras of filter-related monads: I. Ultrafilters and Manes' theorem, Lemmas B and C
- E. Riehl, Category Theory in Context, 2nd ed., Corollary 5.6.2
- D. Mehrle, Category Theory Part III, Example 5.20(d)
- E. Riehl, Category Theory in Context, 2nd ed., monadicity examples in Section 5.5
- E. Riehl, Category Theory in Context, 2nd ed., Definition 5.3.1 and Theorem 5.5.1
- D. Mehrle, Category Theory Part III, Example 5.20(e)
- E. Riehl, Category Theory in Context, 2nd ed., Section 5.6