TheoremStatement: AI-adaptedProof: 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.

The co-Kleisli adjunction induces the given comonad

Statement

For a comonad $G$ on $C$ , there is an adjunction

$L_{G} : C_{G}^{c o K l} ⇄ C : R_{G}$

with $L_{G} (A) = G A$ and $R_{G} (A) = A$ . Its induced comonad $L_{G} R_{G}$ is $G$ on the nose.

Facts & Assumptions

Given: A comonad $(G, ε, δ)$ and its co-Kleisli category.

[L1]

A co-Kleisli arrow $A \to B$ is a base arrow $G A \to B$ , with composition determined by $δ$ (Co-Kleisli category of a comonad).

[L2]

The Kleisli adjunction construction induces its original monad (The Kleisli adjunction induces the given monad).

Proof

technique · direct

1.1L1L2

Define $L_{G} (A) = G A$ and $L_{G} (f) = G (f) δ_{A}$ for $f : G A \to B$ . Define $R_{G} (A) = A$ and let $R_{G} (u)$ be the co-Kleisli arrow represented by $u ε_{A} : G A \to B$ . These are the formal duals of the Kleisli functors.

2.1L1step 1.1

Co-Kleisli associativity and unit laws make both assignments functorial. The equality $C (L_{G} A, B) = C (G A, B) = C_{G}^{c o K l} (A, R_{G} B)$ is a natural identity of hom-sets, so $L_{G} ⊣ R_{G}$ .

3.1L1L2step 1.1step 2.1∎

The counit of this adjunction is $ε_{A} : G A \to A$ , while its unit at $A$ is the co-Kleisli arrow represented by $1_{G A}$ . The triangle identities are the co-Kleisli unit laws, and the induced comultiplication is $L_{G}$ of that unit, namely $δ_{A}$ . Thus the induced comonad is $(G, ε, δ)$ .

Depends on

Used by

Co-Kleisli and co-Eilenberg–Moore adjunctions have the dual extremal universal properties Corollary

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.2.12 by formal duality (standard reference, not scraped)