Sia $\mathcal C$ una categoria. Si consideri la categoria $\mathrm{Funct}(\mathcal C^\mathrm{op},\mathrm{Sets})$, i cui oggetti sono funtori controvarianti $\mathcal C\rightarrow \mathrm{Sets}$, e i cui morfismi sono trasformazioni naturali. Per ogni $Z \in \mathcal C$ si definisce il funtore controvariante
\[
\begin{array}{l@{}l}
F_Z: &\ \mathcal C \rightarrow \mathrm{Sets}\\
&\ X \mapsto \mathrm{Map}_{\mathcal C}(X,Z)=F_Z(X)\,.
\end{array}
\]
Il morfismo $f:Z_1\rightarrow Z_2$ dà origine alla trasformazione naturale
\[
f_\ast:F_{Z_1}=\mathrm{Map}_{\mathcal C}(\cdot,Z_1)\rightarrow\mathrm{Map}_{\mathcal C}(\cdot,Z_2)=F_{Z_2}.
\]
Allora può essere costruito il funtore
\[
\mathcal Y: \mathcal C \rightarrow \mathrm{Funct}(\mathcal C,\mathrm{Sets})
\]
in modo che $\mathcal Y(Z)=F_Z$. Questo funtore è detto
Yoneda embedding.
Lemma (Yoneda) L'applicazione
\[
\mathrm{Map}_{\mathcal C}(Z_1,Z_2)\rightarrow \mathrm{Nat}(F_{Z_1},F_{Z_2})
\]
è una bigezione. Qui, $\mathrm{Nat}(F_{Z_1},F_{Z_2})$ è la collezione delle trasformazioni naturali.
Dimostrazione. Per ottenere la tesi, è sufficiente provare che l'applicazione
\[
\mathrm{Map}_{\mathcal C}(Z_1,Z_2)\rightarrow \mathrm{Nat}(F_{Z_1},F_{Z_2})
\]
ammette inversa. Innanzitutto, essa opera in modo che ad ogni $\varphi \in \mathrm{Map}_{\mathcal C}(Z_1,Z_2)$ associ il suo pushforward $\varphi_\ast$, defnito come: per ogni $X \in \mathcal C$, e $f: X\rightarrow Z_1$, $\varphi_\ast(X)(f)=\varphi f$.
Si consideri dunque $\Phi \in \mathrm{Nat}(F_{Z_1},F_{Z_2})$ trasformazione naturale.
Ricordiamo che, per ogni $Z \in \mathcal C$, il funtore $F_Z$ opera come il pullback: per ogni $f \in \mathrm{Map}_{\mathcal C}(X,Y)$, e $\alpha \in \mathrm{Map}_{\mathcal C}(Y,Z)=F_Z(Y)$, si ha $F_Z(f)(\alpha)=\alpha f= f^\ast(\alpha)$. Allora, dalla definizione, si ha che:
\[
\Phi(X):\mathrm{Map}_{\mathcal C}(X,Z_1)\rightarrow\mathrm{Map}_{\mathcal C}(X,Z_2)
\]
e inoltre, per ogni $f:Y \rightarrow X$ in $\mathcal C$, il seguente diagramma è commutativo:\[
\begin{array}{c@{}c@{}ccc@{}c@{}c}
F_{Z_1}(X) &=&\mathrm{Map}_{\mathcal C}(X,Z_1)&\stackrel{\Phi(X)}{\rightarrow}&\mathrm{Map}_{\mathcal C}(X,Z_2) &=&F_{Z_2}(X)\\
&&\downarrow\scriptstyle{f^\ast=F_{Z_1}(f)}&&\downarrow\scriptstyle{F_{Z_2}(f)=f^\ast}&&\\
F_{Z_1}(Y) &=&\mathrm{Map}_{\mathcal C}(Y,Z_1)&\stackrel{\Phi(Y)}{\rightarrow}&\mathrm{Map}_{\mathcal C}(Y,Z_2) &=&F_{Z_2}(Y)
\end{array}
\]ovvero $\Phi(Y)(F_{Z_1}(f))=F_{Z_2}(f)(\Phi(X))$.
Per costruire una mappa $\mathrm{Map}_{\mathcal C}(Z_1,Z_2)\rightarrow \mathrm{Nat}(F_{Z_1},F_{Z_2})$ inversa di quella assegnata, possiamo pensare di associare alla trasformazione naturale $\Phi$ la mappa $\Phi(Z_1)(\mathrm{id}_{Z_1}) \in \mathrm{Map}_{\mathcal C}(Z_1,Z_2)$. Riassumendo, il claim è che
\[
B: \Phi \in \mathrm{Nat}(F_{Z_1},F_{Z_2}) \mapsto \Phi(Z_1)(\mathrm{id}_{Z_1}) \in \mathrm{Map}_{\mathcal C}(Z_1,Z_2)
\]
è l'inversa di
\[
A: \varphi \in \mathrm{Map}_{\mathcal C}(Z_1,Z_2) \mapsto \varphi_\ast \in \mathrm{Nat}(F_{Z_1},F_{Z_2}).
\]
Infatti
\[
\varphi \stackrel{A}{\mapsto}\varphi_\ast \stackrel{B}{\mapsto} \varphi_\ast(Z_1)(\mathrm{id}_{Z_1}) = \varphi\mathrm{id}_{Z_1}=\varphi
\]
E inoltre:
\[
\Phi \stackrel{B}{\mapsto} \Phi(Z_1)(\mathrm{id}_{Z_1}) \stackrel{A}{\mapsto} (\Phi(Z_1)(\mathrm{id}_{Z_1}))_\ast
\]
e puntualmente, per ogni $X \in \mathcal C$ e $f:X \rightarrow Z_1$ in $\mathcal C$:
\[
(\Phi(Z_1)(\mathrm{id}_{Z_1}))_\ast(X)(f)=\Phi(Z_1)(\mathrm{id}_{Z_1})(f)=f^\ast\Phi(Z_1)(\mathrm{id}_{Z_1})= \Phi(X)f^\ast(\mathrm{id}_{Z_1})= \Phi(X)(f)
\]
da cui segue la tesi. $\square$
