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.
Monads Comonads and Their Algebras — Examples
1 · Prerequisites
- Adjunctions Units and Counits
- Binary Operations, Monoids, Groups and Subgroups
- Categories, Functors and Natural Transformations
- 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
- 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
- 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
- Limits and Colimits
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Monads Comonads and Their Algebras
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Ordinals, Cardinals, and Transfinite Recursion
- Reflective Subcategories and the Adjoint Functor Theorems
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Universal Properties, Representables and the Yoneda Lemma
2 · Summary
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
A Kleisli composite for the list monad computed by substitution and concatenation
Example
For the list monad, let and define
Then the Kleisli composite substitutes the -word for every letter of the -word and concatenates.
Facts & Assumptions
Given: The displayed list-valued functions and .
A Kleisli arrow for the list monad is a function , and Kleisli composition uses the monad multiplication (Kleisli category of a monad; The free-monoid monad has monoids as its Eilenberg–Moore algebras).
The multiplication of the list monad concatenates a list of lists (The free-monoid monad has monoids as its Eilenberg–Moore algebras).
Verification
The data include an input with empty output, and all displayed values are finite words of the required types.
Substitution and concatenation give , , and .
Define and . Then , while and , so is the same word.
The Kleisli category of the maybe monad is the category of sets and partial functions
Example
Let . With insertion as unit and multiplication that collapses either occurrence of , this is the maybe monad. Its Kleisli arrows are precisely partial functions.
Facts & Assumptions
Given: The assignment on sets.
A monad has natural unit and multiplication satisfying two unit laws and associativity (Monad on a category).
A Kleisli arrow is an ordinary arrow , and its composition uses the monad multiplication (Kleisli category of a monad).
Verification
Define to act by on and fix , let be the inclusion of , and let fix elements of and send both the inner and outer undefined values to . Direct inspection of the defined and undefined cases proves the unit and associativity laws in [L1].
A function determines the partial function with domain and value there. Conversely, a partial function on extends uniquely by assigning outside .
These constructions are inverse. Expanding Kleisli composition shows that is defined exactly where is defined and is defined at , with value ; this is the usual maximal-domain composition of partial functions.
The list monad on a two-element set
Example
For , the list monad gives
The unit inserts a letter as a one-letter word, and multiplication removes one level of list brackets by concatenation.
Facts & Assumptions
Given: The set .
The free-monoid monad sends a set to its finite words, has singleton-word unit, and has concatenation multiplication (The free-monoid monad has monoids as its Eilenberg–Moore algebras).
Verification
The displayed beginning contains the empty word, the words , and the words ; continues with all finite words in and .
One has , , , , and .
The unit samples flatten to and the list of singleton words to the original word; nested concatenation gives the same word under either bracketing. Thus the displayed calculations agree with the general monad equations.
A monoid defines the writer monad by adjoining an accumulated output
Example
For a monoid , define . The resulting writer monad carries a value together with an accumulated element of .
Facts & Assumptions
Given: A monoid .
The element is a two-sided identity and multiplication in is associative (Semigroup and monoid).
A monad consists of a functor, a natural unit, and a natural associative multiplication satisfying the unit laws (Monad on a category).
Verification
Define , , and . These formulas have the required types.
Naturality follows because the formulas do not change the -coordinate except by multiplication. The two monad unit composites send to and , both equal to by [L1].
On an element , the two associativity composites produce and , equal by associativity in .
For a group the monad on sets has the -sets as its algebras
Example
Let be a group with identity . On put
Then is a monad, and its -algebras are exactly the -sets: a structure map is the same thing as a left action of on , and a -algebra homomorphism is the same thing as a -equivariant map.
Facts & Assumptions
Given: A group with identity .
A monad on is an endofunctor with natural transformations and such that componentwise and (Monad on a category).
A -algebra is an object with a morphism satisfying and ; a -algebra homomorphism is a morphism with (Algebra and algebra homomorphism for a monad).
A left action of on a set is a function , written , such that and for all and ; then is a -set (Left group actions, transitive actions, and faithful actions).
A function between -sets is -equivariant when for every and (Equivariant maps and isomorphisms of group actions).
Sets and functions form the category , with composition of functions and identity functions (Sets and functions form the large locally small category ).
The Eilenberg–Moore category has the -algebras as objects and the -algebra homomorphisms as morphisms (Eilenberg–Moore category of a monad).
Verification
is an endofunctor of : , and , since both sides send to .
is natural: for , both and send to . And is natural: for , both and send to .
Associativity holds componentwise: on the composite gives and gives , and these agree because multiplication in is associative.
The unit laws hold componentwise: on the composite gives and gives , and both equal because is a two-sided identity of . Hence is a monad by [L1].
Let be a structure map. By [L2] the unit law says for every , and the associativity law evaluated at says . Writing , these are exactly the two clauses of [L3], so is a left action of on .
Conversely, a left action of on is a function with and by [L3], which are the two -algebra laws of [L2] read backwards. So the -algebras with underlying set are precisely the left actions of on .
For algebras and and a function , the homomorphism condition of [L2] evaluated at reads , that is , which is -equivariance in the sense of [L4].
By [L6] the Eilenberg–Moore category of this monad therefore has the -sets as objects and the -equivariant maps as morphisms. This proves the stated claim.
The state monad threads a fixed state set through a computation
Example
Fix a set . The product–exponential adjunction induces the state monad
An element of takes an initial state and returns a value together with a new state.
Facts & Assumptions
Given: A fixed set .
The functor is left adjoint to on (Currying gives the adjunction in ).
Every adjunction induces a monad on the domain of its left adjoint (Every adjunction induces a monad on the domain of its left adjoint).
Verification
Applying [L2] to [L1] gives .
The unit is . For , write with and define : the outer computation selects the inner computation and intermediate state, then the inner computation runs at that state.
Evaluating at any initial state, either unit inserts a computation that returns its input without changing state, and either associativity bracketing runs the same outer, selected middle, and selected inner computations in order. If , every relevant function has empty domain and the same equations hold vacuously.
Topological closure is a monad on the preorder of subsets
Example
For a topological space , topological closure defines a monad on the poset . Its algebras are exactly the closed subsets of .
Facts & Assumptions
Given: A topological space .
Closure is monotone, extensive, and idempotent; in particular and (Kuratowski: operators satisfying , , and correspond bijectively to topologies).
Closure operators on a poset are exactly monads on its associated category (On a preorder the monads are exactly the monotone extensive maps with T(Tp) below Tp; on a poset they are exactly the closure operators).
Algebras for such a monad are exactly its fixed points (Algebras for a preorder monad are exactly its fixed objects up to preorder equivalence; on a poset they are its fixed points).
Verification
On ordered by inclusion, [L1] says is monotone and satisfies .
The identity gives the multiplication comparison and, with step 1.1, makes closure a monad by [L2].
By [L3], its algebra objects are the subsets with , exactly the closed subsets. The boundary subsets and are fixed by [L1].
Topological interior is a comonad on the preorder of subsets, with the open subsets as its coalgebras
Example
For a topological space , topological interior defines a comonad on the poset . Its coalgebras are exactly the open subsets of .
Facts & Assumptions
Given: A topological space .
The interior is the largest open subset of ; in particular , and is open if and only if (Interior, closure, boundary, exterior, derived set and isolated point in a topological space).
Interior operators on a poset are exactly comonads on its associated category (On a preorder the comonads are exactly the monotone contractive maps with Gp below G(Gp); on a poset they are exactly the interior operators).
A coalgebra structure on is an arrow satisfying the coalgebra equations (Coalgebra and coalgebra homomorphism for a comonad).
Verification
If , then is an open subset of , so maximality in [L1] gives . Also [L1] gives , and, since is open, it gives . These arguments include and the empty ambient space.
By [L2], the interior operator therefore defines a comonad.
By [L3], a coalgebra structure on is the inclusion . Together with the reverse inclusion from [L1], this is equality, which holds exactly when is open.
Adjoining one of two fixed points defines commuting closure-operator monads whose distributive law yields their composite
Example
On ordered by inclusion, define
These closure-operator monads commute, and their equality gives a distributive law whose composite adjoins both and .
Facts & Assumptions
Given: The inclusion poset and the displayed maps .
A monotone, extensive, idempotent map on a poset defines a monad (On a preorder the monads are exactly the monotone extensive maps with T(Tp) below Tp; on a poset they are exactly the closure operators).
A distributive law must satisfy the unit and multiplication compatibility diagrams (Distributive law between two monads).
Such a distributive law gives a monad structure on (A distributive law makes the composite endofunctor a monad).
Verification
Union with a fixed subset is monotone, extensive, and idempotent. Thus and are closure-operator monads by [L1].
For every , . This equality gives ; all diagrams in [L2] commute because is thin and the parallel arrows have the displayed common endpoints.
On , both composites respectively give . This checks the formula at every object, including the empty set.
By [L3], the distributive law makes a monad; its unit is the inclusion and its multiplication is the idempotence equality for the closure operator adjoining both fixed points.
The free-abelian-group monad sends a set to its finite formal integer combinations
Example
Specialising the free-module monad to gives the free-abelian-group monad
the set of finitely supported integer combinations of elements of . Its algebras are abelian groups.
Facts & Assumptions
Given: The ring of integers .
The integers form a commutative unital ring (The integers form a commutative ring).
The free module on consists of finitely supported formal linear combinations of its standard basis (The free module on a set and its standard basis).
For a unital ring, algebras of the free-module monad are left modules (For a unital ring R, the free-R-module monad on sets has left R-modules as its Eilenberg–Moore algebras).
The free abelian group on has the same finite formal integer-combination description (Free abelian group on a set).
Verification
By [L1]–[L4], the free--module on is . For a function into an abelian group, the unique extension sends to , so this is also exactly the universal property of the free abelian group on .
Its unit is . Its multiplication flattens to .
Every -module is an abelian group under addition. Conversely, on an abelian group define by repeated addition for positive , by for , and by negatives for negative ; the abelian-group laws give the module laws, and group homomorphisms are exactly the resulting -linear maps. Hence the algebras are precisely abelian groups.
On finite sets the ultrafilter monad is naturally isomorphic to the identity; assuming the ultrafilter lemma, its unit is not invertible on the natural numbers
Example
On the full subcategory of finite sets, the principal-unit map is a natural isomorphism, so the ultrafilter monad restricts to the identity monad up to natural isomorphism. Assuming the ultrafilter lemma, this fails on .
Facts & Assumptions
Given: The ultrafilter monad of The ultrafilter endofunctor with principal unit and flattening multiplication and, for the infinite comparison only, the ultrafilter lemma.
An ultrafilter containing a finite union contains one of its members (Ultrafilters are prime: a union in has a member in ).
The principal map is natural, and the flattening map is the multiplication of the ultrafilter monad (The principal-ultrafilter and ultrafilter-flattening formulas are well-defined and natural; The ultrafilter endofunctor with principal unit and flattening multiplication is a monad).
Assuming the Axiom of Choice, every filter on a set is contained in an ultrafilter on that set (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter); a nonprincipal ultrafilter on then exists (FALSE, once the ultrafilter lemma is available: every ultrafilter is principal).
A filter contains the whole carrier, excludes the empty set, is upward closed, and is closed under finite intersections (Filter on a set).
A finite set is equinumerous with a natural number (The cardinality of a finite set), and an ultrafilter is in particular a proper filter (Ultrafilter).
Verification
If is nonempty and finite, [L5] makes its singleton partition finite, and its union belongs to every ultrafilter. Repeated use of [L1] selects a singleton , and no distinct singleton can also belong because their intersection is empty.
Upward closure now shows that the ultrafilter consists exactly of the subsets containing , namely . Thus is bijective for nonempty finite . If , no proper filter exists because the whole carrier is also empty, so and is again bijective.
Naturality in [L2] makes these bijections a natural isomorphism on finite sets. Under the identification, is the identity and sends the principal ultrafilter at to , so the restricted monad is naturally isomorphic to the identity monad.
Assuming [L3], let be the nonprincipal ultrafilter on supplied there. Every value of is principal, so is outside its image and that unit component is not invertible.
A two-element idempotent monoid is an algebra for the free-monoid monad but is not free
Counterexample
Let with a two-sided identity and . This is an algebra for the free-monoid monad, but it is not a free algebra.
Facts & Assumptions
Given: The displayed multiplication on .
A monoid is a set with associative multiplication and a two-sided identity (Semigroup and monoid).
The algebras for the free-monoid monad are monoids, and its free algebras are free word monoids (The free-monoid monad has monoids as its Eilenberg–Moore algebras).
Verification
The multiplication table is , , and . The element is an identity, and every triple product containing evaluates to , so multiplication is associative.
Hence is a monoid and therefore an Eilenberg–Moore algebra by [L2].
The free monoid on the empty set is a singleton. On a nonempty set, choosing a generator yields the distinct words , so the free monoid is infinite. Therefore the two-element algebra is not free.
The group coequalizer of doubling and zero on the integers is not its underlying-set coequalizer
Counterexample
In groups, the coequalizer of defined by and is . In sets, the coequalizer of the same underlying functions is infinite. Thus the underlying-set functor from groups does not preserve this coequalizer.
Facts & Assumptions
Given: The group homomorphisms and .
A coequalizer is universal among arrows satisfying (Equalizers and coequalizers as limits and colimits of a parallel pair).
Reduction modulo is the quotient homomorphism (For every , the congruence-class group is the quotient group ).
The Eilenberg–Moore category of the free-group monad is the category of groups (The free-group monad has groups as its Eilenberg–Moore algebras).
Verification
Reduction modulo coequalizes and . If a group homomorphism satisfies , then is the identity for every , so kills and factors uniquely through . Thus this is the group coequalizer by [L1]–[L2].
In , the generated equivalence relation identifies every even integer with , because the generating pairs are . No odd integer occurs in such a pair, so each odd integer remains a singleton equivalence class. The quotient map coequalizes and , and every function with is constant on the even class and therefore factors uniquely through this quotient, proving its Set universal property.
The set coequalizer is therefore infinite, while the underlying set of the group coequalizer has the residue classes of and . The underlying-set functor, including the one in the free-group adjunction of [L3], does not preserve this coequalizer.
The self-adjunction of the contravariant power-set functor induces the double-power-set monad
Example
The contravariant power-set functor is self-adjoint between and . The induced monad on is the covariant double-power-set functor .
Facts & Assumptions
Given: The contravariant power-set operation, acting on functions by inverse image.
A natural hom-set bijection determines an adjunction (The unit-counit, hom-set, unit-universal, and counit-universal encodings of an adjunction are equivalent).
Every adjunction induces a monad on the domain of its left adjoint (Every adjunction induces a monad on the domain of its left adjoint).
is the set of all subsets of (The power set ).
Verification
A function is the characteristic assignment of a relation ; transposing gives a function . This natural bijection supplies the self-adjunction by [L1].
Applying [L2], the induced endofunctor is , and its unit is .
For , the multiplication is . This has type . In particular, the construction does not assert a natural map .
Sources
Standard references
Recommended treatments; not extraction sources.
- E. Riehl, Category Theory in Context, 2nd ed., Examples 5.1.4(i) and 5.2.11(i)
- E. Riehl, Category Theory in Context, 2nd ed., Example 5.1.5(iii)
- S. Mac Lane, Categories for the Working Mathematician, 2nd ed., §VI.2, Group actions
- E. Riehl, Category Theory in Context, 2nd ed., Example 5.2.11(iii)
- E. Riehl, Category Theory in Context, 2nd ed., Examples 5.1.7 and 5.2.6(iv)
- E. Riehl, Category Theory in Context, 2nd ed., Example 5.1.4(iii)
- E. Riehl, Category Theory in Context, 2nd ed., Example 5.1.4(vii)