CorollaryStatement: 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.

Every adjunction induces a comonad on the codomain of its left adjoint

Statement

For an adjunction $F : C ⇄ D : G$ with unit $η$ and counit $ε$ , the data

$H : = F G, ε : H \Rightarrow 1_{D}, δ : = F η G : H \Rightarrow H^{2}$

define a comonad on $D$ (Comonad on a category).

Facts & Assumptions

Given: An adjunction $F ⊣ G$ with unit $η$ and counit $ε$ .

[L1]

The adjunction induces the monad $(G F, η, G ε F)$ on $C$ (Every adjunction induces a monad on the domain of its left adjoint).

Proof

technique · direct

1.1L1

Apply [L1] to the opposite adjunction $G^{o p} ⊣ F^{o p}$ . Reversing arrows translates its endofunctor $F^{o p} G^{o p}$ , unit, and multiplication into $F G$ , $ε$ , and $F η G$ on $D$ .

2.1step 1.1∎

The translated associativity equation is $H δ \circ δ = δ H \circ δ$ , and the translated unit equations are $H ε \circ δ = 1_{H} = ε H \circ δ$ ; these are precisely coassociativity and the two counit laws, so the displayed data form a comonad.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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., Lemma 5.1.3 and Definition 5.1.6 (standard reference, not scraped)