9.5 The Yoneda lemma
Recall that we have a category whose objects are sets and whose morphisms are functions. We now show that every precategory has a -valued hom-functor. First we need to define opposites and products of (pre)categories.
For a precategory , its opposite is a precategory with the same type of objects, with , and with identities and composition inherited from .
For precategories and , their product is a precategory with and
Identities are defined by and composition by
Given , for any we obviously have a functor . This gives a function . Next, for any , we have for any the morphism . These are the components of a natural transformation . Functoriality in is easy to check, so we have a functor .
Conversely, suppose given . Then for any and we have the object , giving a function . And for and , we have the morphism
in . Functoriality is again easy to check, so we have a functor .
Now for any precategory , we have a hom-functor
It takes a pair to the set . For a morphism , by definition we have and , so we can define
Functoriality is easy to check.
By \autorefct:functorexpadj, therefore, we have an induced functor , which we call the Yoneda embedding.
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 .
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.4).
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.4).
To show that these are inverses, first suppose given . Then with defined as above, we have . On the other hand, if we suppose given and define as above, then for any we have
Thus, both composites are equal to identities. We leave the proof of naturality to the reader. ∎
The Yoneda embedding is fully faithful.
By \autorefct:yoneda, we have
It is easy to check that this isomorphism is in fact the action of on hom-sets. ∎
If is a category, then is an embedding. In particular, if , then .
By \autorefct:yoneda-embedding, induces an isomorphism on sets of isomorphisms. But as and are categories and is a functor, this is equivalently an isomorphism on identity types, which is the definition of being an embedding. ∎
A functor is said to be representable if there exists and an isomorphism .
If is a category, then the type “ is representable” is a mere proposition.
By definition “ is representable” is just the fiber of over . Since is an embedding by \autorefct:yoneda-mono, this fiber is a mere proposition. ∎
In particular, in a category, any two representations of the same functor are equal. We can use this to give a different proof of \autorefct:adjprop. First we give a characterization of adjunctions in terms of representability.
For any precategories and and a functor , the following types are equivalent.
is a left adjoint.
For each , the functor from to is representable.
An element of the type 2 consists of a function together with, for every and an isomorphism
such that for .
Given this, for we define , and for we define . Now for we define
The verifications that is a functor and and are natural transformations satisfying the triangle identities are exactly as in the classical case, and as they are all mere propositions we will not care about their values. Thus, we have a function 21.
In the other direction, if is a left adjoint, we of course have specified, and we can take to be the composite
This is clearly natural since is, and it has an inverse given by
so it agrees with the old one.
[\autorefct:adjprop] If is a category and , then the type “ is a left adjoint” is a mere proposition.
By \autorefct:representable-prop, if is a category then the type in \autorefct:adj-repr2 is a mere proposition. ∎
|Title||9.5 The Yoneda lemma|