Category Theory
The Yoneda Lemma
"An object is completely determined by its relationships" sounds like philosophy, but the Yoneda lemma turns it into an exact theorem. It explains Church encoding in lambda calculus, parametricity in type systems, and representing objects in algebraic geometry. It is one of the most "useful" theorems in mathematics-and one of the simplest to state.
- **Church encoding**: natural numbers as functions `type Nat = <R>(f: (r: R) => R, z: R) => R`-this is precisely the Yoneda embedding for natural numbers viewed as a monoid
- **Parametricity**: Reynolds's theorem about parametric types is a direct consequence of the Yoneda lemma. The polymorphic function `id: <A>(a: A) => A` is unique-that is Yoneda
- **Algebraic geometry**: Grothendieck's schemes are defined via their points (morphisms from other schemes). "Representability of the functor of points" is the central problem in moduli theory
Предварительные знания
Yoneda
The Yoneda lemma is possibly the deepest result in category theory. It can be stated as: **an object is completely determined by how other objects map into it**-or, dually, by how it maps into others. This is the categorical embodiment of the principle that an object's friends determine the object itself.
**Yoneda Lemma**: for any locally small category C, any object A ∈ C, and any functor F: C → Set, there is a natural bijection: Nat(Hom(A, -), F) ≅ F(A). Here Nat denotes the set of all natural transformations. The bijection sends α: Hom(A,-) ⇒ F to the element α_A(id_A) ∈ F(A).
Informally: to specify a natural transformation from Hom(A,-) to F, it suffices to choose one element of F(A). Everything else is determined automatically. This is remarkable: from a single "seed" element, the entire infinite family of morphisms α_B is uniquely recovered.
Nobuo Yoneda
Nobuo Yoneda (1930-1996) was a Japanese mathematician and computer scientist. According to legend, the lemma was formulated in a conversation with Mac Lane on a Paris Metro platform in 1954. Yoneda worked on both category theory and early programming languages, and he participated in developing one of the first Japanese COBOL compilers.
According to the Yoneda lemma, a natural transformation α: Hom(A,-) ⇒ F is completely determined by:
Representable
A functor F: C → Set is called **representable** if it is isomorphic to Hom(A,-) for some A ∈ C. Representable functors are "functors that remember an object". The Yoneda lemma says: object A is completely determined by the functor Hom(A,-). This means C can be "embedded" into the category of functors without losing information.
A functor F: C → Set is **representable** if there exists an object A ∈ C and an isomorphism F ≅ Hom(A,-). The object A is called the **representing object** for F. The pair (A, u) where u ∈ F(A) is the **universal element**-it uniquely determines the representation.
**Examples of representable functors**: in Top, the functor π₀: Top → Set (connected components) is represented by the two-point discrete space {0,1}-morphisms {0,1} → X correspond to pairs of points in different components. The functor U: Grp → Set (underlying set) is represented by ℤ: Hom_Grp(ℤ, G) ≅ U(G), because a homomorphism from ℤ is determined by the image of 1.
| Functor F: C → Set | Representing object A | Category C |
|---|---|---|
| F(B) = Hom(A, B) | A (tautologically) | Any C |
| F(B) = B × B (pairs) | A = 1 + 1 = {0,1} | Set |
| F(B) = |B| (underlying set of group) | A = ℤ (free group on one generator) | Grp |
| F(B) = B^n (n-tuples) | A = {1,...,n} | Set |
A functor F: C → Set is representable if:
Presheaf
A **presheaf** on a category C is a contravariant functor F: C^{op} → Set, i.e., a functor from the opposite category into Set. A presheaf assigns to each object a set of "sections" and to each morphism a "restriction" operation. The category of all presheaves on C, denoted Ĉ = Set^{C^{op}}, is a central object in category theory.
A **presheaf** on C is a functor F: C^{op} → Set. For an object U: the set F(U) of "sections over U". For a morphism f: V → U: the restriction map F(f): F(U) → F(V). The category Ĉ = [C^{op}, Set] is called the **category of presheaves** on C. It has all limits and colimits.
The most important example: **topological sheaves**. A presheaf on the open sets of a topological space X assigns "local data" to each open U, with restriction operations. If the data "glue together" consistently, the presheaf is a **sheaf**. Sheaves are the foundation of modern algebraic geometry (Grothendieck).
Sheaves and Grothendieck
In the 1950s and 60s, Alexander Grothendieck built algebraic geometry on sheaves and categories. His notion of a "topos" (a generalized topological space) is a category of presheaves with additional properties. Grothendieck used this to prove the Weil conjectures-deep results in number theory that required 30 years of work.
A presheaf on category C is:
Embedding
The Yoneda lemma immediately gives the **Yoneda embedding**: a full and faithful functor y: C → Ĉ = [C^{op}, Set] sending A to the presheaf Hom(-, A). This means: any category C embeds into the richer category of presheaves without loss of information. In Ĉ all limits and colimits exist-even if they do not exist in C.
The **Yoneda embedding** y: C → [C^{op}, Set] is defined by y(A) = Hom_C(-, A). It is **fully faithful**: Hom_C(A, B) ≅ Nat(y(A), y(B)). Consequence: A ≅ B in C if and only if y(A) ≅ y(B) in Ĉ. An object is determined by its "incoming arrows".
**Practical consequence**: to verify an isomorphism A ≅ B it suffices to check that for all X the functions Hom(X, A) → Hom(X, B) are bijections, natural in X. This is called the **Yoneda principle**: an object is determined by its "points" from all other objects. In programming this is the parametricity principle: a type is determined by its behavior for arbitrary arguments.
**Density theorem**: every presheaf F: C^{op} → Set is a colimit of representable presheaves. This is the categorical analogue of the theorem that every function is a limit of delta functions. The Yoneda embedding is a "basis" in the category of presheaves.
The Yoneda lemma is just a technical result about functors with no practical significance
The Yoneda lemma is a philosophical principle: an object is determined by its relationships with other objects. It is the foundation of the "point-free" style in mathematics and programming
In programming: parametricity (types are determined by behavior), encoding via universal properties, Church encoding (natural numbers as functions). In mathematics: representable functors are the foundation of algebraic geometry, deformation theory, and moduli spaces. The Yoneda lemma is a powerful practical tool.
The Yoneda embedding y: C → [C^{op}, Set] is "fully faithful". What does this mean?
Key Ideas
- **Yoneda Lemma**: Nat(Hom(A,-), F) ≅ F(A)-a natural transformation from Hom(A,-) is determined by a single element
- **Representable functor** F ≅ Hom(A,-): a functor that "remembers" object A; the pair (A, u) with u ∈ F(A) is unique up to isomorphism
- **Presheaf**: a contravariant functor C^{op} → Set; the presheaf category Ĉ is both complete and cocomplete
- **Yoneda embedding** y: C ↪ [C^{op}, Set] is fully faithful: an object is determined by its incoming arrows
Related Topics
The Yoneda lemma connects to most constructions in category theory:
- Toposes — A topos is a category of presheaves with additional axioms. The Yoneda lemma is the foundation of the internal logic of a topos
- Adjoint Functors — Representable functors are closely related to adjunctions: a right adjoint is representable via Hom
Вопросы для размышления
- Church encoding of natural numbers: `type Nat = <R>(s: (r: R) => R, z: R) => R`. Show that this is the Yoneda embedding for natural numbers viewed as a monoid (ℕ, +, 0).
- A functor F: C → Set is called "corepresentable" if F ≅ Hom(-,A). How does this relate to the Yoneda embedding? Build the dual version of the lemma.
- Why does the fully faithful property of y mean that "an object is determined by its arrows"? Formulate this as a concrete statement about isomorphisms.