Alphabeta MathHow 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 and be categories. An adjunction consists of functors and , a natural transformation
called the unit, and a natural transformation
called the counit, such that the two triangle identities hold:
Here whiskering and vertical composition are those of Whiskering and horizontal composition of natural transformations. Componentwise, for every and ,
The direction means that is left adjoint to and is right adjoint to . If and are natural isomorphisms, this is precisely the adjunction data occurring in an adjoint equivalence (Equivalence, quasi-inverse, and adjoint equivalence of categories).
Depends on
Used by
- A componentwise family of morphisms need not be a natural transformation and hence need not be a unit Counterexample
- A wrong counit can be natural while both triangle identities fail Counterexample
- Adjoint triple L dashv M dashv R Definition
- Adjuncts and transposition under an adjunction Definition
- The unit inserts basis vectors and the counit evaluates formal linear combinations in the free-vector-space adjunction Example
- The unit inserts generators as one-letter words and the counit evaluates words in the free-group adjunction Example
- A unit and counit determine an adjunction without the triangle identities False statement
- The hom-set form of an adjunction needs no size hypothesis False statement
- The unit and counit transpose formulas are mutually inverse Lemma
- An adjoint equivalence is an adjunction whose unit and counit are natural isomorphisms Proposition
- An adjunction induces postcomposition and precomposition adjunctions on legitimate functor categories Proposition
- An adjunction restricts to an equivalence on the subcategories fixed by its unit and counit Proposition
- The unit-counit definition imposes no local-smallness hypothesis Remark
- Adjoints are unique up to a unique natural isomorphism compatible with the adjunction data Theorem
- Adjunctions compose with the composite unit and counit formulas Theorem
- Natural transformations have mates under a pair of adjunctions Theorem
- Right adjoints preserve every limit that exists Theorem
- The unit-counit, hom-set, unit-universal, and counit-universal encodings of an adjunction are equivalent Theorem
- Unit components are initial in comma categories, and counit components are terminal Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 10 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
- Emily Riehl, Category Theory in Context, 2nd ed., Definition 4.2.5 (standard reference, not scraped)
- Tom Leinster, Basic Category Theory, Theorem 2.2.5 (standard reference, not scraped)