By Lemma 9.5.3 (see product precategory), we have an induced functor $\mathbf{y} : A \to \mathit{Set}^{A^{op}}$ which we call the yoneda embedding.

Properties

Theorem 9.5.4 (The Yoneda Lemma)

For any precategory$A$, any $a:A$, and any functor $F: \mathit{Set}^{A^{op}}$, we have an isomorphism?

$hom_{\mathit{Set}^{A^{op}}}(\mathbf{y}a,F) \cong F a \qquad \qquad(9.5.5)$

Moreover this is natural in both $a$ and $F$.

Proof. Given a natural transformation$\alpha : \mathbf{y}a \to F$, we can consider the component $\alpha_a : \mathbf{y}a(a) \to F a$. Since $\mathbf{y} a(a)\equiv hom_A(a,a)$, we have $1_a:\mathbf{y}a(a)$, so that $\alpha_a(1_a):F a$. This gives a function $\alpha \mapsto \alpha_a(1_a)$ from left to right in (9.5.5).

In the other direction, given $x: F a$, we define $\alpha : \mathbf{y} a \to F$ by

$\alpha_{a'}(f) \equiv F_{a,a'}(f)(x)$

Naturality is easy to check, so this gives a function from right to left in (9.5.5).

To show that these are inverses, first suppose given $x: F a$. Then with $\alpha$ defined as above, we have $\alpha : \mathbf{y}a \to F$ and define $x$ as above, then for any $f:hom_A(a',a)$ we have