Well, a way to prove the lemma struck me to work today -- you can show that any natural transformation η: Hom(_, A) --> K is completely determined by its action on the identity morphism of A, η
Hom(A, A)(1
A). Since this object function takes values in K(A), we get the natural isomorphsim.
This isn't entirely enlightening, though.
Wikipedia describes the Yoneda lemma as a vast generalization of Cayley's theorem, so maybe understanding will come from looking at it from that perspective?
I'm using the convention that fg is in arrow order. That is, codom f = dom g. (Writing this, I'm beginning to feel like I should also write function application on the right too! Ah well)
If C is a category that is a group, then the content of the Yoneda lemma is:
K : C --> Set is simply a group representation of C. That is, C acts on the set K(1) through the group action described by K.
Hom(_, 1) amounts to the Cayley representation of a group. Hom(1, 1) is simply the elements of the group, and Hom(f, 1) is simply the set function that gives right multiplication by f.
So, the Yoneda lemma says that the set of natural transformations Hom(_, 1) --> K is isomorphic to the set K(1). A natural transformation, here, is simply a function from Hom(1, 1) --> K(1) that respects the group action. There is a clear 1-1 correspondence between the natural transformations and the set K(1): the identity can go anywhere, and the rest is determined by the group action.
Categories, Allegories (Freyd, Scedrov) describes a concept of category action, and a Cayley representation for categories.
A (right-)category action of C on a set S is just like a group action. There's a "target" function S --> C, and any morphism f is a partial operation f^ on S. The domain of f^ is precisely those elements of S whose target is f's source.
So, you can think of each element of S as being labelled with an object of C, and any morphism A --> B maps any object labelled as A to an object labelled with B.
The Cayley representation is a functor C --> Set given by:
Cayley(A) is the set of all morphisms whose target is A
Given f:A-->B, Cayley(f) is a set function Cayley(A) --> Cayley(B) which is defined by right multiplication. IOW, Cayley(f)(g) = gf
In other words, it's just the category acting on itself! (on the right)
This is a faithful embedding, BTW.
So now, let's consider a functor K : C --> Set. Let's assume the objects in the image of K are all disjoint. Then, K gives rise to a right C-set. (That is, a set with a right action by C)
The set is simply the union of all the objects in the image of K.
The target operation is simply the inverse of K. That is, the target of any element of K(A) is A.
The action is given by K. If the target of x is A, and f:A-->B, then xf := K(f)(x)
So, K is describing a category action on some set.
Hom(_, A) is also describing a category action... on the set of all morphisms whose target is A. Note that this is a subset of the Cayley representation!
Now, any natural transformation Hom(_, A) --> K is simply a set function that respects the category action, and is again uniquely determined by its action on the identity morphism of A. So, we have the isomorphism Nat(Hom(_, A), K) ~ K(A). (It's K(A) because it has to respect the target operation!)
But the cool thing is that it's a
natural isomorphism. (Right?) So we have this natural isomorphism Nat(Hom(_, ?), K) --> K(?). This is surely saying something important about the two representations of the category C! There's probably some really nice higher-dimensional picture that explains it all really nicely.
But for now, I think the key is understanding Nat(Hom(_, ?), K) --> K(?) as being natural in ?...