Homotopy Type Theory
Yoneda lemma (Rev #3)



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


Theorem 9.5.4 (The Yoneda Lemma)

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

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

Moreover this is natural in both aa and FF.

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

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

α a(f)eqivF a,a(f)(x)\alpha_{a'}(f) \eqiv 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:Fax: F a. Then with α\alpha defined as above, we have α:yaF\alpha : \mathbf{y}a \to F and define xx as above, then for any f:hom A(a,a)f:hom_A(a',a) we have

α a(f) =α a(ya a,a(f)(1 a)) =(α aya a,a(f))(1 a) =(F a,a(f)α a)(1 a) =F a,a(f (α a(1 a)) =F a,a(f)(x). \begin{aligned} \alpha_{a'}(f) &= \alpha_{a'}(\mathbf{y} a_{a,a'}(f)(1_a))\\ &= (\alpha_{a'} \circ \mathbf{y}a_{a,a'}(f))(1_a)\\ &= (F_{a,a'}(f) \circ \alpha_a)(1_a)\\ &= F_{a,a'}(f_(\alpha_a(1_a))\\ &= F_{a,a'}(f)(x). \end{aligned}

Thus, both composites are equal to identities. The proof of naturality follows from this. \square

Corollary 9.5.6

The Yoneda embedding y:ASet A op\mathbf{y} : A \to \mathit{Set}^{A^{op}} is fully faithful.

Proof. By the Yoneda lemma, we have

hom Set A op(ya,yb)yb(a)hom A(a,b)hom_{\mathit{Set}^{A^{op}}}(\mathbf{y}a,\mathbf{y}b) \cong \mathbf{y} b(a) \equiv hom_A(a,b)

It is easy to check that this isomorphism is in fact the action of y\mathbf{y} on hom-sets. \square

See also

Category theory precategory


HoTT book

category: category theory

Revision on September 19, 2018 at 14:11:49 by Ali Caglayan. See the history of this page for a list of all contributions to it.