TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

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

Statement

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

$(T^{2} A, μ_{T A}) \begin{array}{c} \overset{T (a)}{\to} \\ \to_{μ_{A}}^{} \end{array} (T A, μ_{A}) \overset{a}{\to} (A, a)$

is a coequalizer. Thus every $T$ -algebra is the coequalizer in $C^{T}$ of the canonical pair of free algebras.

Facts & Assumptions

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

[L1]

A $T$ -algebra is an object $A$ with a morphism $a : T A \to A$ satisfying $a η_{A} = 1_{A}$ and $a T (a) = a μ_{A}$ ; a morphism $r : (A, a) \to (B, b)$ satisfies $r a = b T (r)$ (Algebra and algebra homomorphism for a monad).

[L2]

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

[L3]

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

Proof

technique · direct

1.1

By [L2], $T (a) : (T^{2} A, μ_{T A}) \to (T A, μ_{A})$ is an algebra homomorphism. The monad associativity equation says that $μ_{A} : (T^{2} A, μ_{T A}) \to (T A, μ_{A})$ is also an algebra homomorphism.

L1L2algebra

2.1

The structure map $a : (T A, μ_{A}) \to (A, a)$ is an algebra homomorphism by the algebra associativity law, and that same law gives $a T (a) = a μ_{A}$ , so $a$ coequalizes the canonical pair.

step 1.1L1

3.1

Let $r : (T A, μ_{A}) \to (B, b)$ be an algebra homomorphism with $r T (a) = r μ_{A}$ . Define $\overset{ˉ}{r} : = r η_{A} : A \to B$ . Naturality of $η$ and the monad unit law give $\overset{ˉ}{r} a = r η_{A} a = r T (a) η_{T A} = r μ_{A} η_{T A} = r$ .

step 2.1L1construct

4.1

Since $r$ is an algebra homomorphism, $r μ_{A} = b T (r)$ . Hence $b T (\overset{ˉ}{r}) = b T (r) T (η_{A}) = r μ_{A} T (η_{A}) = r = \overset{ˉ}{r} a$ , so $\overset{ˉ}{r}$ is an algebra homomorphism.

step 3.1L1algebra

5.1

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

step 3.1step 4.1L1L3∎

Depends on

Used by

Dependency tree · two levels

10 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

E. Riehl, Category Theory in Context, 2nd ed., Proposition 5.4.2 (standard reference, not scraped)