Yoneda Embedding

The Yoneda embedding y: Cat_tau -> PSh(Cat_tau) sends X to Hom(-, X). In thin Cat_tau, representable presheaves are subterminal (all hom-sets are singletons).

Yoneda Embedding

Summary

The Yoneda embedding y: Cat_tau -> PSh(Cat_tau) sends X to Hom(-, X). In thin Cat_tau, representable presheaves are subterminal (all hom-sets are singletons).

Statement

%
\label{def:yoneda-embedding}
The \textbf{Yoneda embedding} is the functor
\[
    \boxed{%
    y : \mathrm{Cat}_\tau \to \mathrm{PSh}(\mathrm{Cat}_\tau),
    \qquad
    y(X) := \Hom(-, X).}
\]
For each object $X$,
$y(X)$ is the representable presheaf
sending $Y$ to $\Hom(Y, X)$.
For a morphism $f : X_1 \to X_2$,
the induced map
$y(f) : y(X_1) \Rightarrow y(X_2)$
has components
$y(f)_Y : g \mapsto f \circ g$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 128
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part14/ch54-functors.tex lines 309-327

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Topos.Functors
• Name: Tau.Topos.yoneda

Dependencies

• Canonical: I.D52, I.D53

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.