If the presheaf Hom$_\mathcal{C}(- \times A, B) : \mathcal{C}^\text{op} \to \textbf{Set}$ is representable, then $\mathcal{C}$ is ccc

We consider a small category $$\mathcal{C}$$ with binary products, and we consider, for any objects $$A, B$$ of $$\mathcal{C}$$, the assignments

$$\begin{eqnarray*} F :\,\, &\mathcal{C}^\text{op} &\longrightarrow \textbf{Set} \\ &X &\mapsto \text{Hom}_{\mathcal{C}}(X \times A, B) \\ &X'\xrightarrow{\bar{f}} X &\mapsto - \circ f\times \text{id}_A. \end{eqnarray*}$$

After some fidgeting with compositions and reversals of the order of morphisms in opposite categories, I managed to prove this is a functor, and therefore, in fact, arbitrariness of $$A, B$$ will show that the category is Cartesian closed (a ccc) if $$B^A$$ exists with a suitable evaluation map.

I want to be constructive about this, and to avoid confusion (for myself, mainly), I will be very formal because my syllabus is, and I don't want to diverge from it. Their, its definition is given via a universal property I will write down explicitly.

Datum: $$F$$ is a representable presheaf.

Required to prove: $$(\exists E \in \mathcal{C}_0)(\exists e : E \times A \to B)(\forall D' \in \mathcal{C}_0)(\forall h \in \text{Hom}_\mathcal{C}(D'\times A, B))(\exists ! H \in \text{Hom}_\mathcal{C}(D', D))(h = e \circ H \times \text{id}_A)$$

As we assume the $$F$$ is representable-- $$F \cong \text{Hom}_\mathcal{C}(-, D)$$ for some object $$D$$ -- our first candidate for $$E$$ will be this $$D$$. We can now simplify the demonstrandum slightly:

R.T.P.: $$(\exists e : D \times A \to B)(\forall D' \in \mathcal{C}_0)(\forall h \in \text{Hom}_\mathcal{C}(D'\times A, B))(\exists ! H \in \text{Hom}_\mathcal{C}(D', D))(h = e \circ H \times \text{id}_A)$$.

Note that there is a natural isomorphism $$\mu : F \,\tilde \Longrightarrow \,y(D)$$. Consider its component $$\mu_D : \text{Hom}_{\mathcal{C}}(D \times A, B) \, \tilde\longrightarrow \text{Hom}_{\mathcal{C}}(D, D) \ni \text{id}_D$$ at $$D$$, and define $$\delta := \mu_D^{-1}(\text{id}_D) : D \times A \to B$$. This will be our canditate for $$e$$. Now we let $$D' \in \mathcal{C}_0$$ and $$h \in \text{Hom}_\mathcal{C}(D'\times A, B)$$ be arbitrarily given. Our goal is now to provide (existence of) a unique $$H: D' \to D$$ such that $$h = \delta \circ H \times \text{id}_A$$.

As $$\mu$$ is a natural transformation, the naturality square gives, for any $$f : D' \to D$$, the equality $$\mu_D(\delta) \circ f = (- \circ f) \circ \mu_D (\delta) = y(D)(f) \circ \mu_D (\delta) = \mu_{D'} \circ F_1(f)(\delta) = \mu_{D'} \circ (- \circ f \times \text{id}_A)(\delta) = \mu_{D'}(\delta \circ f \times \text{id}_A).$$

However, by construction, $$f = \mu_D(\mu_D^{-1}(\text{id}_D)) \circ f = \mu_D(\delta) \circ f = \mu_{D'}(\delta \circ f \times \text{id}_A).$$

I only now realise, that if there is any $$H : D' \to D$$ which works, it must be $$H := f$$, as $$f$$ is now completely determined. (Right..? No, wait, not right, because $$f$$ is still defined in terms of itself: $$f = \mu_{D'}(\delta \circ f \times \text{id}_A)$$. Confusing..)

Regardless, we can now simply compute the expression $$\delta \circ H \times \text{id}_A$$, of which we want it to be equal to our arbitrary $$h : D' \times A \to B$$. Here we go: $$\delta \circ H \times \text{id}_A = \mu_D^{-1}(\text{id}_D) \circ (\mu_{D'}(\delta \circ H \times \text{id}_A) \times \text{id}_A)).$$

Everything typechecks: $$\mu_{D'}(\delta \circ H \times \text{id}_A) : D' \to D$$, so $$\mu_{D'}(\delta \circ H \times \text{id}_A) \times \text{id}_A : D' \times A \to D \times A$$. As $$\mu_D^{-1}(\text{id}_D)) \in \text{Hom}_\mathcal{C}(D \times A, B)$$, the two perfectly compose to a map $$D' \times A \to B$$, That's good news, as $$h$$ also has these domain and codomain.

Unfortunately, I have no idea why they should in fact be equal! If feels like I'm 95% of the way there, but this is where I get stuck. If so, can anyone give me the final push? If not, where did I go wrong?

• You wrote "because $f$ is still defined in terms of itself: $f = \mu_{D'}(\delta \circ f \times \text{id}_A)$", but no, what you have proved is that any $f$ would satisfy that. It isn't an equation that defines anything, it is an identity that holds for everything. Use this equation twice, and you're done. Commented May 22, 2023 at 5:26
• Aaah, you mean substitute $f$ into the second expression?! But then I get: $H = \mu_{D'}(\delta \circ H \times \text{id}_A) = \mu_{D'}(\delta \circ \mu_{D'}(\delta \circ H \times \text{id}_A) \times \text{id}_A).$ (Or with $f$ for $H$, if you wish.) II... still don't see how that makes it the unique map to satisfy $\delta \circ H \times \text{id}_A = h$.. Not in the least because I seem to know nothing about $h$.. Commented May 22, 2023 at 5:34

Use the naturality of the given isomorphism $$\mu : \mathcal{C}(- \times A, B) \cong \mathcal{C}(-,E)$$.

As you have observed, the arrow $$e : E \times A \rightarrow B$$ is just $$(\mu_E)^{-1}(1_E)$$.

Now, take any morphism $$C\times A \xrightarrow{h} B$$ and as you said, take $$H := \mu_C(h)$$.

The naturality of the above isomorphism applied to the arrow $$C \xrightarrow{H} E$$ gives you a commutative square :

$$\require{AMScd}$$ $$\begin{CD} \mathcal{C}(E \times A, B) @>{\mu_E}>> \mathcal{C}(E,E)\\ @V{- \circ (H \times 1_A)}VV @V{- \circ H}VV\\ \mathcal{C}(C \times A, B) @>{\mu_C}>> \mathcal{C}(C, E) \end{CD}$$

Applying the two (equal) composites in this diagram on $$e$$ and using the fact that the component of $$\mu$$ at $$C$$ is an isomorphism gives you $$h = e \circ (H \times 1_A)$$.

Now, suppose that $$C \xrightarrow{H'} E$$ is another arrow such that $$h = e \circ (H' \times 1_A)$$.

Again, using naturality, you get a similar commutative square :

$$\require{AMScd}$$ $$\begin{CD} \mathcal{C}(E \times A, B) @>{\mu_E}>> \mathcal{C}(E,E)\\ @V{- \circ (H' \times 1_A)}VV @V{- \circ H'}VV\\ \mathcal{C}(C \times A, B) @>{\mu_C}>> \mathcal{C}(C, E) \end{CD}$$

Applying the two equal composites again on $$e$$ says that $$\mu_C(h) = H'$$ which gives $$H = H'$$.

• Beautiful, many thanks! Commented May 22, 2023 at 6:09