Alphabeta Math
Session-authored (Fable 5 assisted)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

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

Monads Comonads and Their Algebras — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17Open item page →

A Kleisli composite for the list monad computed by substitution and concatenation

Example

For the list monad, let X={0,1,2} and define

f(0)=[a,b,a],f(1)=[],f(2)=[b],

g(a)=[p],g(b)=[q,p].

Then the Kleisli composite substitutes the g-word for every letter of the f-word and concatenates.

Facts & Assumptions

Given: The displayed list-valued functions f:X{a,b} and g:{a,b}{p,q}.

[L1]

A Kleisli arrow AB for the list monad is a function AB, and Kleisli composition uses the monad multiplication (Kleisli category of a monad; The free-monoid monad has monoids as its Eilenberg–Moore algebras).

[L2]

The multiplication of the list monad concatenates a list of lists (The free-monoid monad has monoids as its Eilenberg–Moore algebras).

Verification

technique · direct
1.1

The data include an input with empty output, and all displayed values are finite words of the required types.

given
2.1

Substitution and concatenation give (gf)(0)=[p,q,p,p], (gf)(1)=[], and (gf)(2)=[q,p].

L1L2step 1.1
3.1

Define h(p)=[r] and h(q)=[s,r]. Then (h(gf))(0)=[r,s,r,r,r], while (hg)(a)=[r] and (hg)(b)=[s,r,r], so ((hg)f)(0) is the same word.

L1L2step 2.1
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17Open item page →

The Kleisli category of the maybe monad is the category of sets and partial functions

Example

Let T(Y)=Y{}. 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 T(Y)=Y{} on sets.

[L1]

A monad has natural unit and multiplication satisfying two unit laws and associativity (Monad on a category).

[L2]

A Kleisli arrow XY is an ordinary arrow XT(Y), and its composition uses the monad multiplication (Kleisli category of a monad).

Verification

technique · direct
1.1

Define T(f) to act by f on Y and fix , let ηY be the inclusion of Y, and let μY:T(TY)TY fix elements of Y 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].

L1
2.1

A function u:XY{} determines the partial function with domain Du={x:u(x)Y} and value u(x) there. Conversely, a partial function on DX extends uniquely by assigning outside D.

L2step 1.1
3.1

These constructions are inverse. Expanding Kleisli composition shows that vu is defined exactly where u is defined and v is defined at u(x), with value v(u(x)); this is the usual maximal-domain composition of partial functions.

L2step 2.1
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17Open item page →

The list monad on a two-element set

Example

For X={a,b}, the list monad gives

T(X)={[],[a],[b],[a,a],[a,b],[b,a],[b,b],}.

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 X={a,b}.

[L1]

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

technique · direct
1.1

The displayed beginning contains the empty word, the words [a],[b], and the words [a,a],[a,b],[b,a],[b,b]; T(X) continues with all finite words in a and b.

L1
2.1

One has ηX(a)=[a], ηX(b)=[b], μX([[a,b],[],[b],])=[a,b,b], μX([])=[], and μX([[]])=[].

L1step 1.1
3.1

The unit samples flatten [[a],] to [a] 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.

L1step 2.1
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17Open item page →

A monoid defines the writer monad by adjoining an accumulated output

Example

For a monoid (M,e,), define T(X)=X×M. The resulting writer monad carries a value together with an accumulated element of M.

Facts & Assumptions

Given: A monoid (M,e,).

[L1]

The element e is a two-sided identity and multiplication in M is associative (Semigroup and monoid).

[L2]

A monad consists of a functor, a natural unit, and a natural associative multiplication satisfying the unit laws (Monad on a category).

Verification

technique · direct
1.1

Define T(f)=f×1M, ηX(x)=(x,e), and μX((x,m),n)=(x,mn). These formulas have the required types.

L1L2
2.1

Naturality follows because the formulas do not change the M-coordinate except by multiplication. The two monad unit composites send (x,m) to (x,em) and (x,me), both equal to (x,m) by [L1].

L1L2step 1.1
3.1

On an element (((x,m),n),p), the two associativity composites produce (x,(mn)p) and (x,m(np)), equal by associativity in M.

L1L2step 1.1
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17Open item page →

For a group G the monad G×() on sets has the G-sets as its algebras

Example

Let G be a group with identity u. On Set put

T(X)=G×X,T(f)=1G×f,ηX(x)=(u,x),μX(g1,(g2,x))=(g1g2,x).

Then (T,η,μ) is a monad, and its T-algebras are exactly the G-sets: a structure map h:G×XX is the same thing as a left action of G on X, and a T-algebra homomorphism is the same thing as a G-equivariant map.

Facts & Assumptions

Given: A group G with identity u.

[L1]

A monad on C is an endofunctor T with natural transformations η:1CT and μ:T2T such that componentwise μAT(μA)=μAμTA and μAT(ηA)=1TA=μAηTA (Monad on a category).

[L2]

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

[L3]

A left action of G on a set X is a function G×XX, written (g,x)gx, such that ux=x and (gh)x=g(hx) for all g,hG and xX; then X is a G-set (Left group actions, transitive actions, and faithful actions).

[L4]

A function f:XY between G-sets is G-equivariant when f(gx)=gf(x) for every gG and xX (Equivariant maps and isomorphisms of group actions).

[L5]

Sets and functions form the category Set, with composition of functions and identity functions (Sets and functions form the large locally small category Set).

[L6]

The Eilenberg–Moore category CT has the T-algebras as objects and the T-algebra homomorphisms as morphisms (Eilenberg–Moore category of a monad).

Verification

technique · direct
1.1

T is an endofunctor of Set: T(1X)=1G×1X=1G×X, and T(ff)=1G×(ff)=(1G×f)(1G×f)=T(f)T(f), since both sides send (g,x) to (g,f(f(x))).

L1L5given
1.2

η is natural: for f:XY, both T(f)ηX and ηYf send x to (u,f(x)). And μ is natural: for f:XY, both T(f)μX and μYT(T(f)) send (g1,(g2,x)) to (g1g2,f(x)).

L1given
2.1

Associativity holds componentwise: on (g1,(g2,(g3,x))) the composite μXT(μX) gives (g1(g2g3),x) and μXμTX gives ((g1g2)g3,x), and these agree because multiplication in G is associative.

L1givenstep 1.1step 1.2
2.2

The unit laws hold componentwise: on (g,x) the composite μXT(ηX) gives (gu,x) and μXηTX gives (ug,x), and both equal (g,x) because u is a two-sided identity of G. Hence (T,η,μ) is a monad by [L1].

L1givenstep 1.1step 1.2
3.1

Let h:G×XX be a structure map. By [L2] the unit law hηX=1X says h(u,x)=x for every x, and the associativity law hT(h)=hμX evaluated at (g1,(g2,x)) says h(g1,h(g2,x))=h(g1g2,x). Writing gx:=h(g,x), these are exactly the two clauses of [L3], so h is a left action of G on X.

L2L3step 2.1step 2.2
4.1

Conversely, a left action of G on X is a function h:G×XX with h(u,x)=x and h(g1g2,x)=h(g1,h(g2,x)) by [L3], which are the two T-algebra laws of [L2] read backwards. So the T-algebras with underlying set X are precisely the left actions of G on X.

L2L3step 3.1
5.1

For algebras (X,h) and (Y,k) and a function f:XY, the homomorphism condition fh=kT(f) of [L2] evaluated at (g,x) reads f(h(g,x))=k(g,f(x)), that is f(gx)=gf(x), which is G-equivariance in the sense of [L4].

L2L4step 3.1step 4.1
6.1

By [L6] the Eilenberg–Moore category of this monad therefore has the G-sets as objects and the G-equivariant maps as morphisms. This proves the stated claim.

L6step 4.1step 5.1
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17Open item page →

The state monad threads a fixed state set through a computation

Example

Fix a set S. The product–exponential adjunction induces the state monad

T(X)=(X×S)S.

An element of T(X) takes an initial state and returns a value together with a new state.

Facts & Assumptions

Given: A fixed set S.

[L1]

The functor ×S is left adjoint to ()S on Set (Currying gives the adjunction ×A()A in Set).

[L2]

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

technique · direct
1.1

Applying [L2] to [L1] gives T(X)=(X×S)S.

L1L2
2.1

The unit is ηX(x)(s)=(x,s). For kT(TX), write k(s)=(c,s) with c:SX×S and define μX(k)(s)=c(s): the outer computation selects the inner computation and intermediate state, then the inner computation runs at that state.

L1L2step 1.1
3.1

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 S=, every relevant function has empty domain and the same equations hold vacuously.

L2step 2.1
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck passaudited 2026-08-17Open item page →

Topological closure is a monad on the preorder of subsets

Example

For a topological space X, topological closure defines a monad on the poset (P(X),). Its algebras are exactly the closed subsets of X.

Facts & Assumptions

Verification

technique · direct
1.1

On P(X) ordered by inclusion, [L1] says AA is monotone and satisfies AA.

L1
2.1

The identity A=A gives the multiplication comparison and, with step 1.1, makes closure a monad by [L2].

L1L2step 1.1
3.1

By [L3], its algebra objects are the subsets A with A=A, exactly the closed subsets. The boundary subsets and X are fixed by [L1].

L1L3step 2.1
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17Open item page →

Topological interior is a comonad on the preorder of subsets, with the open subsets as its coalgebras

Example

For a topological space X, topological interior defines a comonad on the poset (P(X),). Its coalgebras are exactly the open subsets of X.

Facts & Assumptions

Given: A topological space X.

[L1]

The interior int(A) is the largest open subset of A; in particular int(A)A, and A is open if and only if A=int(A) (Interior, closure, boundary, exterior, derived set and isolated point in a topological space).

[L3]

A coalgebra structure on A is an arrow AG(A) satisfying the coalgebra equations (Coalgebra and coalgebra homomorphism for a comonad).

Verification

technique · direct
1.1

If AB, then int(A) is an open subset of B, so maximality in [L1] gives int(A)int(B). Also [L1] gives int(A)A, and, since int(A) is open, it gives int(int(A))=int(A). These arguments include A= and the empty ambient space.

L1
2.1

By [L2], the interior operator therefore defines a comonad.

L2step 1.1
3.1

By [L3], a coalgebra structure on A is the inclusion Aint(A). Together with the reverse inclusion from [L1], this is equality, which holds exactly when A is open.

L1L3step 2.1
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17Open item page →

Adjoining one of two fixed points defines commuting closure-operator monads whose distributive law yields their composite

Example

On P({a,b,c}) ordered by inclusion, define

S(A)=A{a},T(A)=A{b}.

These closure-operator monads commute, and their equality ST=TS gives a distributive law whose composite adjoins both a and b.

Facts & Assumptions

Given: The inclusion poset P=P({a,b,c}) and the displayed maps S,T:PP.

[L2]

A distributive law STTS must satisfy the unit and multiplication compatibility diagrams (Distributive law between two monads).

[L3]

Such a distributive law gives a monad structure on TS (A distributive law makes the composite endofunctor a monad).

Verification

technique · direct
1.1

Union with a fixed subset is monotone, extensive, and idempotent. Thus S and T are closure-operator monads by [L1].

L1
2.1

For every A, S(T(A))=A{a,b}=T(S(A)). This equality gives λ:STTS; all diagrams in [L2] commute because P is thin and the parallel arrows have the displayed common endpoints.

L2step 1.1
3.1

On ,{a},{b},{c},{a,b},{a,c},{b,c},{a,b,c}, both composites respectively give {a,b},{a,b},{a,b},{a,b,c},{a,b},{a,b,c},{a,b,c},{a,b,c}. This checks the formula at every object, including the empty set.

step 2.1
4.1

By [L3], the distributive law makes TS a monad; its unit is the inclusion AA{a,b} and its multiplication is the idempotence equality for the closure operator adjoining both fixed points.

L1L3step 2.1step 3.1
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck passaudited 2026-08-17Open item page →

The free-abelian-group monad sends a set to its finite formal integer combinations

Example

Specialising the free-module monad to R=Z gives the free-abelian-group monad

T(X)=Z(X),

the set of finitely supported integer combinations of elements of X. Its algebras are abelian groups.

Facts & Assumptions

Given: The ring of integers Z.

[L1]

The integers form a commutative unital ring (The integers form a commutative ring).

[L2]

The free module on X consists of finitely supported formal linear combinations of its standard basis (The free module on a set and its standard basis).

[L3]

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

[L4]

The free abelian group on X has the same finite formal integer-combination description (Free abelian group on a set).

Verification

technique · direct
1.1

By [L1]–[L4], the free-Z-module on X is Z(X). For a function u:XA into an abelian group, the unique extension sends xnx[x] to xnxu(x), so this is also exactly the universal property of the free abelian group on X.

L1L2L3L4
2.1

Its unit is x1[x]. Its multiplication flattens ini[jmij[xij]] to i,jnimij[xij].

L2L3step 1.1
3.1

Every Z-module is an abelian group under addition. Conversely, on an abelian group define nx by repeated addition for positive n, by 0 for n=0, and by negatives for negative n; the abelian-group laws give the module laws, and group homomorphisms are exactly the resulting Z-linear maps. Hence the algebras are precisely abelian groups.

L1L3step 1.1step 2.1
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-17Open item page →

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 ηX:XβX is a natural isomorphism, so the ultrafilter monad restricts to the identity monad up to natural isomorphism. Assuming the ultrafilter lemma, this fails on N.

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.

[L1]

An ultrafilter containing a finite union contains one of its members (Ultrafilters are prime: a union in U has a member in U).

[L2]
[L3]

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 N then exists (FALSE, once the ultrafilter lemma is available: every ultrafilter is principal).

[L4]

A filter contains the whole carrier, excludes the empty set, is upward closed, and is closed under finite intersections (Filter on a set).

[L5]

A finite set is equinumerous with a natural number (The cardinality A of a finite set), and an ultrafilter is in particular a proper filter (Ultrafilter).

Verification

technique · direct
1.1

If X is nonempty and finite, [L5] makes its singleton partition finite, and its union X belongs to every ultrafilter. Repeated use of [L1] selects a singleton {x}, and no distinct singleton can also belong because their intersection is empty.

L1L4L5
2.1

Upward closure now shows that the ultrafilter consists exactly of the subsets containing x, namely ηX(x). Thus ηX is bijective for nonempty finite X. If X=, no proper filter exists because the whole carrier is also empty, so βX= and ηX is again bijective.

L2L4step 1.1
3.1

Naturality in [L2] makes these bijections a natural isomorphism on finite sets. Under the identification, ηX is the identity and μX sends the principal ultrafilter at ηX(x) to ηX(x), so the restricted monad is naturally isomorphic to the identity monad.

L2step 2.1
4.1

Assuming [L3], let U be the nonprincipal ultrafilter on N supplied there. Every value of ηN is principal, so U is outside its image and that unit component is not invertible.

L2L3step 3.1
CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-17Open item page →

A two-element idempotent monoid is an algebra for the free-monoid monad but is not free

Counterexample

Let M={1,e} with 1 a two-sided identity and e2=e. This is an algebra for the free-monoid monad, but it is not a free algebra.

Facts & Assumptions

Given: The displayed multiplication on M.

[L1]

A monoid is a set with associative multiplication and a two-sided identity (Semigroup and monoid).

[L2]

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

technique · direct
1.1

The multiplication table is 11=1, 1e=e1=e, and ee=e. The element 1 is an identity, and every triple product containing e evaluates to e, so multiplication is associative.

L1
2.1

Hence M is a monoid and therefore an Eilenberg–Moore algebra by [L2].

L2step 1.1
3.1

The free monoid on the empty set is a singleton. On a nonempty set, choosing a generator x yields the distinct words [],[x],[x,x],, so the free monoid is infinite. Therefore the two-element algebra M is not free.

L2step 2.1
CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17Open item page →

The group coequalizer of doubling and zero on the integers is not its underlying-set coequalizer

Counterexample

In groups, the coequalizer of f,g:ZZ defined by f(n)=2n and g(n)=0 is Z/2Z. 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 f(n)=2n and g(n)=0.

[L1]

A coequalizer is universal among arrows q satisfying qf=qg (Equalizers and coequalizers as limits and colimits of a parallel pair).

[L2]

Reduction modulo 2 is the quotient homomorphism ZZ/2Z (For every nN, the congruence-class group (Z/n,+) is the quotient group (Z,+)/nZ).

[L3]

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

technique · direct
1.1

Reduction modulo 2 coequalizes f and g. If a group homomorphism h:ZH satisfies hf=hg, then h(2n) is the identity for every n, so h kills 2Z and factors uniquely through Z/2Z. Thus this is the group coequalizer by [L1]–[L2].

L1L2
1.2

In Set, the generated equivalence relation identifies every even integer with 0, because the generating pairs are (2n,0). No odd integer occurs in such a pair, so each odd integer remains a singleton equivalence class. The quotient map coequalizes f and g, and every function u with uf=ug is constant on the even class and therefore factors uniquely through this quotient, proving its Set universal property.

L1
2.1

The set coequalizer is therefore infinite, while the underlying set of the group coequalizer has the residue classes of 0 and 1. The underlying-set functor, including the one in the free-group adjunction of [L3], does not preserve this coequalizer.

L3step 1.1step 1.2
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck passaudited 2026-08-17Open item page →

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 Set and Setop. The induced monad on Set is the covariant double-power-set functor XPPX.

Facts & Assumptions

Given: The contravariant power-set operation, acting on functions by inverse image.

[L2]

Every adjunction induces a monad on the domain of its left adjoint (Every adjunction induces a monad on the domain of its left adjoint).

[L3]

P(X) is the set of all subsets of X (The power set P(x)={z:zx}).

Verification

technique · direct
1.1

A function XP(Y) is the characteristic assignment of a relation RX×Y; transposing R gives a function YP(X). This natural bijection Set(X,PY)Set(Y,PX) supplies the self-adjunction by [L1].

L1L3
2.1

Applying [L2], the induced endofunctor is T(X)=PPX, and its unit is ηX(x)={AX:xA}.

L2L3step 1.1
3.1

For WP(P(P(PX))), the multiplication is μX(W)={AX:{APX:AA}W}. This has type T2XTX. In particular, the construction does not assert a natural map PPXX.

L2L3step 2.1

Sources