# Presheaf categories are Cartesian closed

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!

Comments: To comment on this post, send me an email following the template below. Your email address will not be posted, unless you choose to include it in thelink:field. An md5sum of it will however be sent to Gravatar to obtain any possible avatar.`To: Ryan Kavanagh <rak@rak.ac> Subject: [blog-comment] /academia/2016/08/24/Presheaf-categories-are-Cartesian-closed post_id: /academia/2016/08/24/Presheaf-categories-are-Cartesian-closed author: [How should you be identified? Usually your name or "Anonymous"] link: [optional link to your website] Your comments here. Markdown syntax accepted.`

## 1 Comment

## Tom Hirschowitz

Hi!

First a comment: you might save some work by applying MacLane’s Theorem IV.2.(iv) (page 81 on the first edition of CWM).

This says that an adjunction is entirely determined by the candidate left adjoint $F$, an assignment for the right adjoint $G$ on objects, and an arrow $e_A: FGA -> A$ for all $A$, universal from $F$ to $A$. So in fact you don’t need to construct the whole functor $G$, nor to prove naturality of $e$.

Now regarding your problem, I think the way out is to use naturality of $\phi’$. Indeed, you want to prove that each

is entirely determined by the requirements on $\phi’$, for all $s \in SC$.

The only involved requirement is that for any $C$ and $s \in SC$ and $q \in QC$, we have

Let us thus compute the image of any $(f,q)$ with $f: D o C$ and $q \in QD$.

By naturality of $\phi’$, you get a commuting square from

$\phi’_C : SC o [y_C imes Q, R]$

to

$\phi’_D : SD o [y_D imes Q, R]$

by action of $f$. Taken at $s \in SC$, this precisely says that

$$\phi’_C(s)