Showing changes from revision #1 to #2:
Added | Removed | Changed
Idea
Definition
By Lemma 9.5.3 (see product precategory), we have an induced functor which we call the yoneda embedding.
Properties
Theorem 9.5.4 (The Yoneda Lemma)
For any precategory , any , and any functor , we have an isomorphism?
Moreover this is natural in both and .
Proof. Given a natural transformation , we can consider the component . Since , we have , so that . This gives a function from left to right in (9.5.5).
In the other direction, given , we define by
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 . Then with defined as above, we have and define as above, then for any we have
Thus, both composites are equal to identities. The proof of naturality follows from this.
Corollary 9.5.6
The Yoneda embedding is fully faithful.
Proof. By the Yoneda lemma, we have
It is easy to check that this isomorphism is in fact the action of on hom-sets.
See also
Category theory precategory
References
HoTT book