Naturality of exponential objects in cartesian closed categories

cartesian-closed-categoriescategory-theory

A category with finite products $C$ is cartesian closed if for each $X \in C$ the functor $- \times X \colon C \to C$ has a right adjoint $(-)^X$. This is to say that for each $Y,Z \in C$ we have bijections

$$
\hom(Y \times X, Z) \simeq \hom(Y,Z^X) \tag{1}
$$

that are natural both in $Y$ and $Z$.

Now, a map $f \colon X \to X'$ induces a natural transformation $1 \times f \colon – \times X \Rightarrow – \times X'$ and so we have a natural map

$$
\hom(-,(-)^{X'}) \simeq \hom(-\times X', -) \xrightarrow{(-\times f)^\ast} \hom(- \times X,-) \simeq \hom(-,(-)^{X}).
$$

Does this define a functorial assignment $X \mapsto (-)^X$?

Fixing $Y$, the above yields a natural transformation $\hom(-,Y^{X'}) \to \hom(-,Y^{X})$ which by Yoneda comes from a map $\eta_Y \colon Y^{X'} \to Y^{X}$. This looks natural on $Y$, but so far I haven't succeeded in proving so.

And in case the assignment is indeed functorial:

Is the adjunction-induced ismorphism on the hom-sets also natural in $X$? In other words, is $(1)$ a natural isomorphism of functors $C^{op} \times C^{op} \times C \to \mathsf{Set}$?

Best Answer

$\require{AMScd}$ Let's say you have a morphism $g : Y\to Z$ in addition to $f : X \to X'$. By Yoneda, the square $$ \begin{CD} Y^{X'} @>f^*>> Y^X \\ @Vg_*VV @VVg_*V \\ Z^{X'} @>>f^*> Z^X \end{CD} $$ (where $f^*$ is precomposition, $g_*$ is postcomposition) commutes if and only if the square of natural transformations $$ \begin{CD} \hom(-,Y^{X'}) @>>> \hom(-,Y^X) \\ @VVV @VVV \\ \hom(-,Z^{X'}) @>>> \hom(-,Z^X) \end{CD} $$ from which you obtained the former commutes. This second square is isomorphic to the square of natural transformations $$ \begin{CD} \hom(X'\times-,Y) @>>> \hom(X\times -,Y) \\ @VVV @VVV \\ \hom(X'\times -,Z) @>>> \hom(X\times -,Z) \end{CD} $$ This is commutative if and only if for every object $A$ the square $$ \begin{CD} \hom(X'\times A,Y) @>>> \hom(X\times A,Y) \\ @VVV @VVV \\ \hom(X'\times A,Z) @>>> \hom(X\times A,Z) \end{CD} $$ commutes. It does -even naturally in $A$-.

RE the last question: yes, there is a isomorphism of functors $$ \hom(-_1\times-_2,-_3)\cong \hom(-_1, -_3^{-_2}) \cong \hom(-_2, -_3^{-_1}) $$ (with obvious meaning of the placeholders). See the notion of adjunction of two variables for a more general look on this.

Related Question