Presheaf categories are Cartesian closed

\(\gdef{\Hom}{\mathsf{Hom}}\) \(\gdef{\C}{\mathbf{C}}\) \(\gdef{\hC}{\hat\C}\)

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 \(\phi’\) 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 \(\C\), the presheaf \(\hC\) is Cartesian closed.

Proof. We must show that \(\hC\) has a terminal object \(1\), finite products, and exponentials.

The terminal \(1 : \C^{op} \to \mathbf{Sets}\) is given by the constant functor onto \(1\) in \(\mathbf{Sets}\).

The product \(P \times Q : \C^{op} \to \mathbf{Sets}\) of \(P, Q : \C^{op} \to \mathbf{Sets}\) is given pointwise, that is, \((P \times Q)(C) = P(C) \times Q(C)\).

So it remains to find an exponential \(Q^P\). Recall that, by analogy with the motivating example in \(\gdef{\S}{\mathbf{Sets}}\S\), we define exponentiation to be right adjoint to the right product, explicitly, \(({-}) \times Q \dashv ({-})^Q\). In particular, for all \(P, Q, R\), we want

$$ \tag{*}\Hom(P\times Q,R) \simeq Hom(P, R^Q) $$

natural in \(P\) and \(Q\).

A first guess of \(R^Q(C) = \Hom(Q(C), R(C))\) fails to work in any sensible functorial way (it’s not at all clear what \(R^Q(f)\) should be).

Suppose now that \(P\) is representable. Then there exists a \(C\) such that \(P \simeq \Hom(-, C) = y(C)\). Then (*) becomes

$$ \Hom(y(C)\times Q, R) \simeq \Hom(y(C), R^Q). $$

But by the Yoneda lemma, assuming \(R^Q\) exists,

$$ \Hom(y(C), R^Q) \simeq R^Q(C) $$

So we make an educated guess and define

$$ R^Q(C) = \Hom(y(C) \times Q, R) $$

and for \(f : C \to D\), let \(R^Q(f) : R^Q(D) \to R^Q(C)\) be given by

$$ R^Q(f) = \Hom(y(f) \times Q, R). $$

That’s to say, for any \(\gdef{\naturalto}{\Rightarrow} \eta : y(D)\times Q \naturalto R\),

$$ R^Q(f)(\eta) = \eta \circ (y(f) \times Id_Q) : y(C)\times Q \naturalto R. $$

So we’ve defined \((-)^Q\) on objects. Now we must define \(\xi^Q : P^Q \to R^Q\) for arrows \(\xi : P \to Q\) of \(\hC\). What we need is a natural transformation \({ (\xi^Q)_C : P^Q(C) \to R^Q(C) }_C\), that is, a family \({ (\xi^Q)_C : Hom(y(C) \times Q, P) \naturalto Hom(y(C) \times Q, R) }_C\) of arrows of \(\S\). Here, we make use of our intuition from \(\S\) and define:

$$(\xi^Q)_C(\gamma : y(C) \times Q \naturalto P) = (\xi \circ \gamma) : y(C) \times Q \naturalto R.$$

It is straightforward to check that \(\xi^Q\) is a natural transformation, that is, for each \(f : D \to C\) in \(\C\), we have

Indeed, given a \(\gamma : y(C) \times Q \naturalto P\), going around the top right side of the square gives

$$ \begin{aligned} &R^Q(f)((\xi^Q)_C \gamma)\\ &= R^Q(f)(\xi \circ \gamma)\\ &= \xi \circ \gamma \circ (y(f) \times Id_Q), R^Q(f)((\xi^Q)_C \gamma) \end{aligned} $$

while going around the bottom left side of the square gives

$$ \begin{aligned} &(\xi^Q)_D (P^Q(f)(\gamma))\\ &= (\xi^Q)_D(\gamma \circ (y(f) \times Id_Q))\\ &= \xi \circ \gamma \circ (y(f) \times Id_Q). \end{aligned} $$

Now that we have a candidate for \((-)^Q\), we need to show that it is actually an exponential, that’s to say, that for all \(Q\), we have the adjunction \({-} \times Q \dashv ({-})^Q\). We do so by means of a counit \(e : (-)^Q \times Q \naturalto I\). Observe that in \(\S\), this counit is exactly function evaluation, i.e., \(e_R : \Hom(Q, R)\times Q \to R\) is given by \((f, q) \mapsto f(q)\). Hence why we call the counit \(e\) “evaluation”.

Recall that a counit \(\epsilon\) for an adjunction \(F \dashv G\) is a “natural transformation \(\epsilon : FG \naturalto I\) such that each arrow \(\epsilon_a\) is universal from \(a\) to \(F\) while each \(g : x \to Ga\) has left adjunct \(\epsilon_a \circ Fg : Fx \to a\)” [CWM].

So to show that \(e\) is a counit for \({-} \times Q \dashv (-)^Q\), we must show that it is a natural transformation \((-)^Q\times Q \naturalto I\) such that \(e_P\) is universal from \((-) \times Q\) to \(P\). That’s to say, for every \(\phi : S\times Q \naturalto P\), we must have a unique \(\phi’ : S \naturalto P^Q\) such that the following triangle commutes:

We see that our choices are heavily constrained by the types at hand. For every \(P\), we need a natural transformation \(e_P : P^Q \times Q \naturalto P\), i.e., a family \({ e_{P,C} : P^Q(C) \times Q(C) \to P(C) }C\), i.e., a family of morphisms \({ e{P,C} : \mathsf{Nat}(y(C) \times Q, P) \times Q(C) \to P(C) }C\) in \(\S\). So each \(e{P,C}\) receives a pair \((\eta, q)\),

$$ \begin{aligned} \eta &: \Hom(-, C)\times Q \naturalto P\\ q &\in Q(C) \end{aligned} $$

and must produce an \(e_{P,C}(\eta, q) \in P(C)\). The only arrow into \(C\) we know must exist is the identity \(1_C : C \to C\). Observe also that \(\eta_C : Hom(C, C)\times Q(C) \to P(C)\). So we take

$$ e_{P,C}(\eta, q) = \eta_C(1_C, q). $$

Though we were in a sense “forced” to make this definition by the types, we must still check that \(e_P\) is a natural transformation. Let \(f : D \to C\) be arbitrary in \(C\). We must show that

To see why \((Pf \circ \eta_C)(1_C, q) = (\eta\circ(y(f) \times Id))_D(1_D, Q(f)(q))\), first observe:

$$ \begin{aligned} &(\eta\circ(y(f) \times Id))_D(1_D,Q(f)(q))\\ &= \eta_D(y(f)(1_D), Q(f)(q))\\ &= \eta_D(f, Q(f)(q)). \end{aligned} $$

But \(\eta : \Hom(-, C)\times Q(C) \naturalto P\) is natural, so we have \(P(f) \circ \eta_C = \eta_D \circ (\Hom(f, C) \times Q(f))\), in particular, that \((P(f) \circ \eta_C)(1_C, q) = (\eta\circ(y(f) \times Id))_D(1_D,Q(f)(q)) = \eta_D(f, Q(f)(q))\). So by transitivity, we have the desired equality in the bottom right corner of the naturality diagram. So we conclude that \(e_P\) is a natural transformation and is thus eligible to be component of the (candidate) natural transformation \(e : (-)^Q \times Q \naturalto I\). (There is no confusion here: because the morphisms of \(\hC\) are natural transformations, the components \(e_P\) of \(e\), being arrows of \(\hC\), are natural transformations. To the best of my understanding, this is an instance of a 2-category.) We must now show that \(e\) is a natural transformation between the functors \((-)^Q \times Q : \hC \to \hC\) and \(I : \hC \to \hC\). Let \(P\) and \(R\) be arbitrary objects (functors) in \(\hC\) and let \(\xi : P \naturalto R\) 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 \(C\) in \(\C\), the following diagram commutes in \(\S\):

Given a pair \((\eta : y(C) \times Q \naturalto P, q \in Q(C))\), going around the top right corner of the square gives us

$$ \begin{aligned} &\xi_C(e_{P,C}(\eta, q)\\ &= \xi_C(\eta_C(1_C, q))\\ &= (\xi \circ \eta)_C (1_C, q), \end{aligned} $$

while going around the bottom left gives us

$$ \begin{aligned} &e_{R,C}((\xi^Q)_C\; \eta, q)\\ &=e_{R,C}(\xi \circ \eta, q)\\ &= (\xi \circ \eta)_C(1_C, q). \end{aligned} $$

So we can finally conclude that \(e : (-)^Q \times Q \naturalto I\) 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 \(\hC\) has exponents, that’s to say, a right adjoint \({-}\times Q \dashv (-)^Q\). We’ve found a candidate functor \((-)^Q : \hC \to \hC\), as well as a natural transformation \(e : (-)^Q \times Q \naturalto I\). All that remains is to show that \(e : (-)^Q \times Q \naturalto I\) is a counit for the adjunction. This involves finding for every \(\phi : S \times Q \naturalto P\) a unique \(\phi’ : S \naturalto P^Q\) such that the above-given triangle commutes.

So we need for all \(C\), \(s \in S(C)\), \(q \in Q(C)\),

$$\phi_c(s, q) = e_{P,C}(\phi'_C (s), q) = (\phi'_C (s))_C(1_C, q),$$

where \(\phi’_C(s) : y(C)\times Q \naturalto P\) is a natural transformation. So we must find a family of maps

$$\{ (\phi'_C (s))_D : \Hom(D, C)\times Q(D) \to P(D) \}_D$$

natural in \(D\). Let’s draw inspiration from the types at hand: again they will force our hand.

$$ \begin{aligned} \phi_D &: S(D) \times Q(D) \to P(D)\\ S(f) &: S(C) \to S(D) \text{ for } f \in \Hom(D, C)\\ s &\in S(C)\\ q &\in Q(D)\\ \end{aligned} $$

So the obvious candidate is:

$$ (\phi'_C(s))_D(f,q) = \phi_D(S(f)(s), q). $$

Let’s check commutativity:

$$ \begin{aligned} e_{P,C}(\phi'_C(s), q) &= (\phi'_C(s))_C(1_C, q)\\ &= \phi_C(S(1_C)(s), q)\\ &= \phi_C(s, q). \end{aligned} $$

So the triangle commutes as desired.

Checking naturality is straightforward.

All that remains is to show the uniqueness of \(\phi’\). And this, dear reader, is where I’m stuck. Any hints would be greatly appreciated, please comment below!

To: Ryan Kavanagh <rak@rak.ac>
Subject: [blog-comment] /blog/2016-08-24-presheaf-categories-are-cartesian-closed/

post_id: /blog/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.