TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passaudited 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.

Algebras for an idempotent monad form a reflective subcategory

Statement

Let $(T, η, μ)$ be an idempotent monad on $C$ . An object $A$ admits a $T$ -algebra structure if and only if $η_{A} : A \to T A$ is an isomorphism, and then the structure is uniquely $η_{A}^{- 1}$ . The forgetful functor identifies $C^{T}$ with the full reflective subcategory of such objects, with reflector $T$ .

Facts & Assumptions

Given: An idempotent monad (Idempotent monad), its algebras (Algebra and algebra homomorphism for a monad), and its Eilenberg–Moore category (Eilenberg–Moore category of a monad).

Proof

technique · direct

1.1

If $a : T A \to A$ is an algebra structure, then $a \circ η_{A} = 1_{A}$ . Naturality of $η$ at $a$ and idempotence, which gives $η_{T A} = T (η_{A})$ , imply $η_{A} \circ a = T (a) \circ η_{T A} = T (a \circ η_{A}) = 1_{T A}$ ; hence $a = η_{A}^{- 1}$ .

given

2.1

Conversely, if $η_{A}$ is invertible, put $a = η_{A}^{- 1}$ . The unit axiom is immediate, and naturality of $η$ together with the monad unit laws gives $a \circ T (a) = a \circ μ_{A}$ ; step 1.1 shows this structure is unique.

givenstep 1.1

3.1

Naturality of $η$ shows every base morphism between two such fixed objects commutes with their inverse-unit algebra structures, so the subcategory is full. The unit $η_{A} : A \to T A$ is universal from $A$ to this subcategory, since $T A$ is fixed and every map to a fixed object extends uniquely through $η_{A}$ ; hence $T$ is its reflector in the sense of Reflective full subcategory and reflector.

step 1.1step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 13 results over 8 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

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