Adjunctions

Origin. Kan (1958). Fundamental concept of category theory. F ⊣ G: left adjoint to right. Universal property characterization. Unifies constructions across mathematics. Foundation for categorical logic.

Models. Two functors F: C → D, G: D → C. Natural bijection: D(FA, B) ≅ C(A, GB). Unit and counit: η, ε. Represents "best approximation."

Formalism.

Adjunction: F ⊣ G (F left adjoint to G) Hom-set bijection: D(FA, B) ≅ C(A, GB) natural in A, B.

Unit and counit: η: Id_C → GF (unit) ε: FG → Id_D (counit)

Triangle identities: εF ∘ Fη = id_F Gε ∘ ηG = id_G

Universal property: η_A: A → GFA is universal arrow from A to G. For any f: A → GB, ∃! g: FA → B with Gg ∘ η_A = f.

Examples: Free ⊣ Forgetful (groups, monoids, etc.) F × — ⊣ —^F (product/exponential) Σ_f ⊣ f* ⊣ Π_f (dependent sums/products) ∃ ⊣ Δ ⊣ ∀ (quantifiers as adjoints)

Properties: Left adjoints preserve colimits: F(colim) = colim(F—). Right adjoints preserve limits: G(lim) = lim(G—).

Monads from adjunctions: T = GF is a monad. η: Id → T (unit) μ = GεF: T² → T (multiplication)

Symbols.

Symbol	Unicode	Name	Meaning
⊣	U+22A3	Adjoint	Left adjoint
η	U+03B7	Eta	Unit
ε	U+03B5	Epsilon	Counit
≅	U+2245	Isomorphism	Natural bijection
→	—	Arrow	Morphism

Metatheory. Adjoints unique up to isomorphism. Adjoint functor theorems. Kan extensions as adjoints. Double adjoints.

Applies to. Universal algebra. Logic (quantifiers). Type theory (dependent types). Functional programming (monads). Topos theory.

Limitations. Abstract machinery. Existence not guaranteed. Computational interpretation sometimes unclear. Category theory prerequisites.