DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-16

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.

Adjunction by unit, counit, and the triangle identities

Definition

Let $C$ and $D$ be categories. An adjunction $F ⊣ G$ consists of functors $F : C \to D$ and $G : D \to C$ , a natural transformation

$η : 1_{C} \Rightarrow G F$

called the unit, and a natural transformation

$ε : F G \Rightarrow 1_{D}$

called the counit, such that the two triangle identities hold:

$(ε F) \circ (F η) = 1_{F}, (G ε) \circ (η G) = 1_{G} .$

Here whiskering and vertical composition are those of Whiskering and horizontal composition of natural transformations. Componentwise, for every $c \in C$ and $d \in D$ ,

$ε_{F c} \circ F (η_{c}) = 1_{F c}, G (ε_{d}) \circ η_{G d} = 1_{G d} .$

The direction $F ⊣ G$ means that $F$ is left adjoint to $G$ and $G$ is right adjoint to $F$ . If $η$ and $ε$ are natural isomorphisms, this is precisely the adjunction data occurring in an adjoint equivalence (Equivalence, quasi-inverse, and adjoint equivalence of categories).

Adjunction by unit, counit, and the triangle identities

Definition

Depends on

Dependency tree · 2 levels

Sources