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.

The inclusion of a reflective full subcategory is monadic

Statement

If $A$ is a reflective full subcategory of $C$ , then its inclusion $I : A \to C$ is monadic.

Facts & Assumptions

Given: A reflection $R ⊣ I$ as in Reflective full subcategory and reflector.

[L1]

A reflection is an adjunction $R : C ⇄ A : I$ with $I$ the full inclusion (Reflective full subcategory and reflector).

[L2]

Algebras for an idempotent monad are exactly the objects whose unit is invertible, with the unique inverse-unit structure (Algebras for an idempotent monad form a reflective subcategory).

[L3]

An adjunction induces the monad formed from its right adjoint after its left adjoint (Every adjunction induces a monad on the domain of its left adjoint).

[L4]

Every component of the counit of a reflection is an isomorphism (The counit of a reflection is an isomorphism).

Proof

technique · direct

1.1

By [L1] and [L3], the reflection induces the monad $T = I R$ on $C$ with multiplication $I ε R$ . By [L4] this multiplication is a natural isomorphism, so $T$ is idempotent (Idempotent monad).

L1L3L4

2.1

By [L2], the Eilenberg–Moore category of $T$ is the full subcategory of objects $C$ for which the reflection unit $C \to I R C$ is invertible. The comparison sends $A \in A$ to $(I A, I ε_{A})$ , and its essential image is exactly this fixed-object subcategory.

step 1.1L2

3.1

Fullness of $I$ makes the comparison fully faithful, and every algebra $(C, η_{C}^{- 1})$ has the specified isomorphism $η_{C} : C \to I R C$ to the comparison image of $R C$ . Thus the comparison is an equivalence, so $I$ is monadic by Monadic and strictly monadic functors.

step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 24 results over 12 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(ii) (standard reference, not scraped)