TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

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.

A monad morphism induces restriction of algebras and a natural comparison of free algebras

Statement

A monad morphism $α : T \Rightarrow S$ on $C$ induces a functor $α^{*} : C^{S} \to C^{T}$ over $C$ , defined by restriction of algebra structure. Its components also define a natural transformation from the free $T$ -algebra functor to the free $S$ -algebra functor followed by $α^{*}$ .

Facts & Assumptions

Given: A monad morphism $α : (T, η^{T}, μ^{T}) \Rightarrow (S, η^{S}, μ^{S})$ on $C$ .

[L1]

The equations for $α$ are $α η^{T} = η^{S}$ and $α μ^{T} = μ^{S} S α α T$ (Morphisms between monads on one category).

[L2]

An $S$ -algebra $(A, a)$ satisfies $a η_{A}^{S} = 1_{A}$ and $a μ_{A}^{S} = a S (a)$ , and its homomorphisms satisfy $f a = b S (f)$ (Algebra and algebra homomorphism for a monad).

[L3]

The free $T$ -algebra on $A$ is $(T A, μ_{A}^{T})$ (Free algebra for a monad).

Proof

technique · direct

1.1L1L2

For an $S$ -algebra $(A, a)$ , put $a_{T} = a α_{A} : T A \to A$ . By [L1]–[L2], $a_{T} η_{A}^{T} = a η_{A}^{S} = 1_{A}$ , while naturality of $α$ and the two multiplication equations give $a_{T} μ_{A}^{T} = a_{T} T (a_{T})$ . Thus $(A, a_{T})$ is a $T$ -algebra.

2.1L1L2step 1.1

If $f : (A, a) \to (B, b)$ is an $S$ -algebra homomorphism, then $f a α_{A} = b S (f) α_{A} = b α_{B} T (f)$ by naturality of $α$ . Hence the unchanged underlying arrow is a $T$ -algebra homomorphism, and unchanged identities and composites define a functor $α^{*}$ over $C$ .

3.1L1L3step 2.1∎

For every $A$ , the multiplication equation in [L1] says precisely that $α_{A} : (T A, μ_{A}^{T}) \to (S A, μ_{A}^{S} α_{S A})$ is a $T$ -algebra homomorphism. Naturality of $α$ makes these maps natural in $A$ , giving the claimed comparison of free algebras.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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

S. Mac Lane, Categories for the Working Mathematician, 2nd ed., Exercise VI.2.3 (standard reference, not scraped)