We gave a weak, “half-enriched” version of the Yoneda Lemma earlier. Now it’s time to pump it up to a fully-enriched version.
Given a -functor and an object , then the functor defines a -natural map . We also have the (ordinary) adjunction
and under this adjunction we find corresponding to a -natural transformation . Now the strong form of the Yoneda Lemma says that this family is actually the counit of the end , so by the definition of the functor category we have an isomorphism in :
So, how do we verify that is the end in question? Consider any other -natural family . Now we run the above adjunction backwards to get a -natural family . But this is now a -natural transformation from the functor represented by to the functor , and so the weak form of the Yoneda Lemma tells us that for a unique . Running this back through the adjunction says that , and the universal property is satisfied.
Let’s hit this isomorphism with the underlying set functor to get a bijection . This sends an arrow to , which is a -natural family with components given by . But this is exactly the bijection asserted by the weak form of the Yoneda Lemma, so the weaker form is implied by the stronger one.
If we consider the special case where our functor is representable, we find that
When exists, we can convert the functor to a functor by the exponential adjunction in . By the case of representable functors given above, this Yoneda embedding is fully faithful. From this -functor we can establish that the Yoneda isomorphism is -natural in and .
More interesting to me is Rigorous Trivialities, which is being sporadically written by a new graduate student at UPenn. I wonder if Isabel put him up to it. Either way, this means we’re only one seminar invitation from having three Ivy-league-educated math bloggers in one room (hint, hint).