I had never before realised the immense usefulness of the Yoneda lemma. In the past few sections of Mac Lane’s and Moerdijk’s “Sheaves in Geometry and Logic”, it’s been used both as a proof tool and as a heuristic for finding the right definition of a functor (in this case, the exponential functor in a presheaf category).
Here is a direct proof that does not require the machinery used by CWM. Seeing that there is “only one thing you can do” at any point of the proof, this proof is surely not new (indeed, I suspect it’s the same proof Prakash Panangaden gave in his category theory lectures at McGill in summer 2012).
Lemma (Yoneda). Let be a functor from a locally small category . Then for all objects of ,
and this bijection is natural in and .
Proof. We claim that the map
is the bijection we want. So see why, observe that each natural transformation is uniquely determined by the of . Indeed, let be arbitrary. Then by naturality of , we must have :
Accordingly, every element gives rise to the natural transformation determined by . So is surjective. Conversely, if for two natural transformations , , , then for all ,
So by extensionality. So is injective. So is a bijection.
We now show naturality in . Let be a natural transformation. But this is immediate by the equality :
Next, we show naturality in . Suppose . Then, by naturality of (see the first diagram), we have , so
This means that the following diagram describing the naturality of in commutes (remark the cancellation of contravariance):
So we conclude that is also natural in . Q.E.D.
As I type this up, a few questions come to mind.
What happens when is representable, that is, when it is naturally isomorphic to for some object of ? There’s no obvious reason (to me) why representability implies that every natural transformation has to be an isomorphism. Is there a way to characterise these isomorphisms by means of the Yoneda lemma?
I remember having found with a friend some cool applications of the Yoneda lemma to posets a few summers ago. Unfortunately, they were done on a whiteboard and I’ve been unable to rediscover them. So: what are some cool applications of the Yoneda lemma to posets?