As I’ve been working through “Sheaves in Geometry and Logic”, I’ve been skimming proofs and attempting to rederive them. I normally end up with a better understanding of the material, but sometimes I get stuck. Here’s one case where I’ve gotten stuck: can anybody tell me why the counit for the exponential is universal? In particular, I can’t manage to show the uniqueness of at the end of the proof. I started this entry back in April, and figured I should finally finish it off and ask for help.
Theorem. Given any small category , the presheaf category is Cartesian closed.
Proof. We must show that has a terminal object , finite products, and exponentials.
The terminal is given by the constant functor onto in .
The product of is given pointwise, that is, .
So it remains to find an exponential . Recall that, by analogy with the motivating example in , we define exponentiation to be right adjoint to the right product, explicitly, . In particular, for all , we want
natural in and .
A first guess of fails to work in any sensible functorial way (it’s not at all clear what should be).
Suppose now that is representable. Then there exists a such that . Then (*) becomes
But by the Yoneda lemma, assuming exists,
So we make an educated guess and define
and for , let be given by
That’s to say, for any ,
So we’ve defined on objects. Now we must define for arrows of . What we need is a natural transformation , that is, a family of arrows of . Here, we make use of our intuition from and define:
It is straightforward to check that is a natural transformation, that is, for each in , we have
Indeed, given a , going around the top right side of the square gives
while going around the bottom left side of the square gives
Now that we have a candidate for , we need to show that it is actually an exponential, that’s to say, that for all , we have the adjunction . We do so by means of a counit . Observe that in , this counit is exactly function evaluation, i.e., is given by . Hence why we call the counit “evaluation”.
Recall that a counit for an adjunction is a “natural transformation such that each arrow is universal from to while each has left adjunct ” [CWM].
So to show that is a counit for , we must show that it is a natural transformation such that is universal from to . That’s to say, for every , we must have a unique such that the following triangle commutes:
We see that our choices are heavily constrained by the types at hand. For every , we need a natural transformation , i.e., a family , i.e., a family of morphisms in . So each receives a pair ,
and must produce an . The only arrow into we know must exist is the identity . Observe also that . So we take
Though we were in a sense “forced” to make this definition by the types, we must still check that is a natural transformation. Let be arbitrary in . We must show that
To see why , first observe:
But is natural, so we have , in particular, that . So by transitivity, we have the desired equality in the bottom right corner of the naturality diagram. So we conclude that is a natural transformation and is thus eligible to be component of the (candidate) natural transformation . (There is no confusion here: because the morphisms of are natural transformations, the components of , being arrows of , are natural transformations. To the best of my understanding, this is an instance of a 2-category.) We must now show that is a natural transformation between the functors and . Let and be arbitrary objects (functors) in and let be an arbitrary morphism (natural transformation) between them. Then we want to show that the following diagram commutes:
This diagram commutes if and only if for every object in , the following diagram commutes in :
Given a pair , going around the top right corner of the square gives us
while going around the bottom left gives us
So we can finally conclude that is a natural transformation.
Let’s briefly recap what we’ve accomplished so far and where we’re trying to go. We’re trying to show that has exponents, that’s to say, a right adjoint . We’ve found a candidate functor , as well as a natural transformation . All that remains is to show that is a counit for the adjunction. This involves finding for every a unique such that the above-given triangle commutes.
So we need for all , , ,
where is a natural transformation. So we must find a family of maps
natural in . Let’s draw inspiration from the types at hand: again they will force our hand.
So the obvious candidate is:
Let’s check commutativity:
So the triangle commutes as desired.
Checking naturality is straightforward.
All that remains is to show the uniqueness of . And this, dear reader, is where I’m stuck. Any hints would be greatly appreciated, please comment below!