「‍」 Lingenic

Yoneda Lemma

(⤓.md ≡ ◇.md); γ ≜ [2026-07-17T135416.643, 2026-10-22T054143.488] ∧ |γ| = 3

Yoneda Lemma

Origin. Nobuo Yoneda (1954), via correspondence reported by Saunders Mac Lane. The central lemma of category theory: an object is determined, up to isomorphism, by the pattern of maps into (or out of) it. Underlies representability, universal properties, and categorical semantics of logic.

Models. Objects known through their relationships. The lemma formalizes "an object is what it does": the functor of all morphisms into an object encodes the object completely. It converts objects into presheaves, embedding any category into a well-behaved functor category where limits, exponentials, and logical structure are available.

Formalism.

Representable functors: For a locally small category C and object A, the hom-functor Hom(−, A) : Cᵒᵖ → Set (a presheaf) sends X ↦ Hom(X, A) and f : X → Y to precomposition (−∘f).

The Yoneda lemma: For any presheaf F : Cᵒᵖ → Set and object A, there is a bijection Nat(Hom(−, A), F) ≅ F(A) natural in both A and F. A natural transformation out of a representable is determined by the image of the identity id_A.

The Yoneda embedding: よ : C → [Cᵒᵖ, Set], A ↦ Hom(−, A). It is full and faithful: Hom_C(A, B) ≅ Nat(Hom(−,A), Hom(−,B)). Hence A ≅ B iff their representables are isomorphic.

Consequences: Universal properties are representability statements: a construction is characterized by a representing object, unique up to unique isomorphism. The embedding preserves limits and exponentials, presenting C inside a topos of presheaves. Density: every presheaf is a colimit of representables.

Co-Yoneda (dual): Using covariant Hom(A, −) : C → Set gives Nat(Hom(A,−), G) ≅ G(A).

Symbols.

SymbolUnicodeNameMeaning
よU+3088YoThe Yoneda embedding C → [Cᵒᵖ, Set]
≅U+2245IsomorphismThe natural bijection of the lemma
−U+2212Minus signThe argument placeholder in Hom(−, A)
→U+2192ArrowA morphism, or a functor
↦U+21A6Maps toThe action of a functor on an object, X ↦ Hom(X, A)
∘U+2218CompositionPrecomposition (−∘f) giving the functorial action
ᵒU+1D52Modifier letter oFirst letter of the superscript "op"
ᵖU+1D56Modifier letter pSecond letter of the superscript "op"
∞U+221EInfinityThe ∞-categorical form of the lemma
Hom(−, A)—Representable presheafThe presheaf represented by A
Cᵒᵖ—Opposite categoryPresheaves are contravariant functors on C
[Cᵒᵖ, Set]—Presheaf categoryFunctors Cᵒᵖ → Set and natural transformations
Nat(−, −)—Natural transformationsThe set of natural maps between two functors
id_A—IdentityThe morphism whose image determines a transformation
F, G—FunctorsA presheaf and a covariant functor
Set—SetsThe target of the hom-functors

Metatheory. The proof is short and entirely constructive: naturality forces a transformation out of Hom(−, A) to be determined by the image of id_A, and that assignment is inverse to the evident one, naturally in both arguments. Full faithfulness follows by taking F representable, so よ reflects isomorphisms and A ≅ B exactly when their representables agree, which is the precise content of "an object is what it does". Cayley's theorem is the one-object case. The embedding preserves all limits that exist in C, and exponentials when C is cartesian closed, but it does not preserve colimits — deliberately, since [Cᵒᵖ, Set] is the free cocompletion of C: left Kan extension along よ is an equivalence between functors C → D with D cocomplete and colimit-preserving functors [Cᵒᵖ, Set] → D. The density theorem, that every presheaf is a canonical colimit of representables, is the same fact. Enriched and ∞-categorical versions hold, the latter in Lurie's Higher Topos Theory (2009).

Applies to. Universal properties and adjunctions. Representable functors and classifying objects. Presheaf and sheaf semantics; topos-theoretic models of logic. Functorial semantics (Lawvere theories). Databases and type theory (presheaf models of dependent types).

Limitations. The statement needs local smallness, since Hom(X, A) must be a set; for large categories the presheaf category is not locally small and a universe has to be fixed, which is why the free cocompletion of a large category does not exist without size restrictions. The embedding creates colimits rather than preserving them, so colimits that already exist in C are destroyed by よ and presheaves are not a conservative extension for statements about them. Determination is up to isomorphism only, never up to equality, and the isomorphism is canonical but the representing object is not unique on the nose. Representability is a real restriction: the covariant powerset functor on Set is not representable, and deciding representability in general requires the adjoint functor theorem with its solution-set condition. The enriched version requires the base to be complete symmetric monoidal closed, so it does not transfer to an arbitrary monoidal base.

© 2026 Lingenic LLC