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.

Symbol	Unicode	Meaning
Hom(−, A)	—	presheaf represented by A
[Cᵒᵖ, Set]	—	category of presheaves on C
Nat(−, −)	—	set of natural transformations
よ	U+3088	Yoneda embedding
≅	U+2245	natural isomorphism / iso
id_A	—	identity morphism on A

Metatheory. The bijection is natural in F and A (a statement of naturality that is itself an instance of the lemma). Full faithfulness of よ makes the presheaf category a conservative, structure-rich extension of C; representability provides the uniform definition of universal constructions (products, exponentials, adjoints). In categorical logic the presheaf topos supplies a Kripke-style/internal-logic setting, tying Yoneda to sheaf and topos semantics.

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. Requires local smallness (hom-sets, not proper classes) for the target Set; size issues need care for large categories. The lemma characterizes objects but computing the representing object or checking representability can be hard. It is a structural, not a constructive, tool — it says the correspondence exists and is natural, not how to build a given natural transformation without the identity witness.