nicer proof of basic functor category fact?

Question

In functor categories, there's a nice isomorphism ${\mathcal C}^{\mathcal A \times \mathcal B} \cong ({\mathcal C}^{\mathcal B})^{\mathcal A}$. Proving this is a good exercise. It's not exactly hard, but there are a lot of details. Lambek and Scott refer to the proof as "lengthy", and they are not kidding. Below is a fairly careful proof, which needs roughly a hundred equations.

Question. Can we improve this proof? For example, we might derive it from some other result; or we might argue that the functor ${\mathcal C}^{\mathcal A \times \mathcal B} \to ({\mathcal C}^{\mathcal B})^{\mathcal A}$ is bijective in some sense and therefore must have an inverse, or we might just pull out a lemma to simplify the argument.

PROOF

The proof is in four parts. In part 0 we set up basic definitions and notation; in part 1 we build a functor from the left side to the right; in part 2 we do the same from right to left; and in part 3 we show that that these two functors are inverses.

0. BASIC DEFINITIONS AND NOTATION

$F \in \operatorname{Ob} {\mathcal B}^{\mathcal A}$ means $F$ is a functor $\mathcal A \to \mathcal B$: for $A \in \operatorname{Ob} \mathcal A$,

$$F(1_A) = 1_{F(A)}, \tag{F0}$$

and for $a_0 \in {\mathcal A}(A_0, A_1), a_1 \in {\mathcal A}(A_1, A_2)$,

$$F(a_1 a_0) = F(a_1)F(a_0). \tag{F1}$$

$\epsilon \in {\mathcal B}^{\mathcal A}(F_0, F_1)$ means $\epsilon$ is a natural transformation $F_0 \to F_1$: for $a \in {\mathcal A}(A_0, A_1)$,

$$F_1(a)\epsilon(A_0) = \epsilon(A_1)F_0(a). \tag{FC0}$$

We also have, for $\epsilon_0 \in {\mathcal B}^{\mathcal A}(F_0, F_1)$, $\epsilon_1 \in {\mathcal B}^{\mathcal A}(F_1, F_2)$, $A \in \operatorname{Ob} A$,

$$(\epsilon_1 \epsilon_0)(A) = \epsilon_1(A) \epsilon_0(A); \tag{FC1}$$

and for $F \in \operatorname{Ob} {\mathcal B}^{\mathcal A}$, $A \in \operatorname{Ob} \mathcal A$,

$$1_F(A) = 1_{F(A)}. \tag{FC2}$$

1. LEFT-TO-RIGHT FUNCTOR

We'll define a functor $-^*: {\mathcal C}^{\mathcal A \times \mathcal B} \to ({\mathcal C}^{\mathcal B})^{\mathcal A}$.

For $F \in \operatorname{Ob} {\mathcal C}^{\mathcal A \times \mathcal B}$, $A \in \operatorname{Ob} \mathcal A$, $B \in \operatorname{Ob} \mathcal B$, $b \in \operatorname{Mor} \mathcal B$, define $F^*(A)$ by

$$\begin{align} & F^*(A)(B) := F(A, B), \tag{LTR0}\\ & F^*(A)(b) := F(1_A, b). \tag{LTR1} \end{align}$$

$F^*(A)$ is a functor in $\operatorname{Ob} {\mathcal C}^{\mathcal B}$:

$$\begin{align} & F^*(A)(1_B) = \\ & F(1_A, 1_B) = \\ & F(1_{(A, B)}) = \\ & 1_{F(A, B)} = \\ & 1_{F^*(A)(B)}; \end{align}$$

and for $b_0 \in {\mathcal B}(B_0, B_1), b_1 \in {\mathcal B}(B_1, B_2)$,

$$\begin{align} & F^*(A)(b_1 b_0) = \\ & F(1_A, b_1 b_0) = \\ & F(1_A, b_1) F(1_A, b_0) = \\ & F^*(A)(b_1) F^*(A)(b_0). \end{align}$$

For $a \in {\mathcal A}(A_0, A_1)$, define $F^*(a)$ by

$$\begin{align} & F^*(a)(B) := F(a, 1_B). \tag{LTR2} \end{align}$$

$F^*(a)$ is a natural transformation in ${\mathcal C}^{\mathcal B}(F^*(A_0), F^*(A_1))$: for $b \in {\mathcal B}(B_0, B_1)$,

$$\begin{align} & F^*(A_1)(b) F^*(a)(B_0) = \\ & F(1_{A_1}, b) F(a, 1_{B_0}) = \\ & F(1_{A_1} a, b 1_{B_0}) = \\ & F(a, b) = \\ & F(a 1_{A_0}, 1_{B_1} b) = \\ & F(a, 1_{B_1}) F(1_{A_0}, b) = \\ & F^*(a)(B_1) F^*(A_0)(b). \end{align}$$

$F^*$ is a functor in $\operatorname{Ob} ({\mathcal C}^{\mathcal B})^{\mathcal A}$:

$$\begin{align} & F^*(1_A)(B) = \\ & F(1_A, 1_B) = \\ & F(1_{(A, B)}) = \\ & 1_{F(A, B)} = \\ & 1_{F^*(A)(B)} = \operatorname{(by} \operatorname{(FC2))} \\ & {1_{F^*(A)}}(B); \end{align}$$

and for $a_0 \in {\mathcal A}(A_0, A_1), a_1 \in {\mathcal A}(A_1, A_2)$,

$$\begin{align} & F^*(a_1 a_0)(B) = \\ & F(a_1 a_0, 1_B) = \\ & F((a_1, 1_B)(a_0, 1_B)) = \\ & F(a_1, 1_B)F(a_0, 1_B)) = \\ & F^*(a_1)(B) F^*(a_0)(B) = \\ & (F^*(a_1) F^*(a_0))(B). \end{align}$$

For $\phi \in {\mathcal C}^{\mathcal A \times \mathcal B}(F_0, F_1)$, define $\phi^*(A)$ by

$$\begin{align} & \phi^*(A)(B) := \phi(A, B). \tag{LTR3} \end{align}$$

$\phi^*(A)$ is a natural transformation in ${\mathcal C}^{\mathcal B}(F_0^*(A), F_1^*(A))$: for $b \in {\mathcal B}(B_0, B_1)$,

$$\begin{align} & F_1^*(A)(b) \phi^*(A)(B_0) = \\ & F_1(1_A, b) \phi(A, B_0) = \\ & \phi(A, B_1) F_0(1_A, b) = \\ & \phi^*(A)(F_1) F_0^*(A)(b). \end{align}$$

$\phi^*$ is a natural transformation in $({\mathcal C}^{\mathcal B})^{\mathcal A}(F_0^*, F_1^*)$: for $a \in {\mathcal A}(A_0, A_1)$,

$$\begin{align} & (F_1^*(a) \phi^*(A_0))(B) = \\ & F_1^*(a)(B) \phi^*(A_0)(B) = \\ & F_1(a, 1_B) \phi(A_0, B) = \\ & \phi(A_1, B) F_0(a, 1_B) = \\ & \phi^*(A_1)(B) F_0^*(a)(B) = \\ & (\phi^*(A_1) F_0^*(a))(B). \end{align}$$

Finally, $-^*$ is a functor:

$$\begin{align} & {1_F}^*(A)(B) = \\ & {1_F}(A, B) = \\ & 1_{F(A, B)} = \\ & 1_{F^*(A)(B)} = \\ & {1_{F^*(A)}}(B) = \\ & {1_{F^*}}(A)(B), \end{align}$$

and for $\phi_0 \in {\mathcal C}^{\mathcal A \times \mathcal B}(F_0, F_1)$, $\phi_1 \in {\mathcal C}^{\mathcal A \times \mathcal B}(F_1, F_2)$,

$$\begin{align} & (\phi_1 \phi_0)^*(A)(B) = \\ & (\phi_1 \phi_0)(A, B) = \\ & \phi_1(A, B) \phi_0(A, B) = \\ & \phi_1^*(A)(B) \phi_0^*(A)(B) = \\ & (\phi_1^*(A) \phi_0^*(A))(B) = \\ & (\phi_1^* \phi_0^*)(A)(B). \end{align}$$

2. RIGHT-TO-LEFT FUNCTOR

We'll define a functor $-': ({\mathcal C}^{\mathcal B})^{\mathcal A} \to {\mathcal C}^{\mathcal A \times \mathcal B}$.

For a functor $G \in \operatorname{Ob} ({\mathcal C}^{\mathcal B})^{\mathcal A}$, define $G'$ by

$$\begin{align} & G'(A, B) := G(A)(B) \tag{RTL0} \end{align}$$

and for $a \in {\mathcal A}(A_0, A_1)$, $b \in {\mathcal B}(B_0, B_1)$, define

$$\begin{align} & G'(a, b) := G(A_1)(b) G(a)(B_0). \tag{RTL1} \end{align}$$

$G'$ is a functor:

$$\begin{align} & G'(1_{(A, B)}) = \\ & G'(1_A, 1_B) = \\ & G(A)(1_B) G(1_A)(B) = \\ & 1_{G(A)(B)} 1_{G(A)}(B) = \\ & 1_{G(A)(B)} 1_{G(A)(B)} = \\ & 1_{G(A)(B)} = \\ & 1_{G'(A, B)}; \\ \end{align}$$

and for $(a_0, b_0) \in ({\mathcal A \times \mathcal B})((A_0, B_0), (A_1, B_1))$, $(a_1, b_1) \in ({\mathcal A \times \mathcal B})((A_1, B_1), (A_2, B_2))$,

$$\begin{align} & G'((a_1, b_1)(a_0, b_0)) = \\ & G'(a_1 a_0, b_1 b_0) = \\ & G(A_2)(b_1 b_0) \cdot G(a_1 a_0)(B_0) = \\ & G(A_2)(b_1)G(A_2)(b_0) \cdot (G(a_1)G(a_0))(B_0) = \\ & G(A_2)(b_1)G(A_2)(b_0) \cdot G(a_1)(B_0)G(a_0)(B_0) = \\ & G(A_2)(b_1) \cdot G(A_2)(b_0) G(a_1)(B_0) \cdot G(a_0)(B_0) = \\ & G(A_2)(b_1) \cdot G(a_1)(B_1) G(A_1)(b_0) \cdot G(a_0)(B_0) = \\ & G(A_2)(b_1)G(a_1)(B_1) \cdot G(A_1)(b_0)G(a_0)(B_0) = \\ & G'(a_1, b_1) G'(a_0, b_0). \end{align}$$

For $\psi \in ({\mathcal C}^{\mathcal A})^{\mathcal B}(G_0, G_1)$, define $\psi'$ by

$$\begin{align} & \psi'(A, B) := \psi(A)(B). \tag{RTL2} \end{align}$$

$\psi'$ is a natural transformation in ${\mathcal C}^{\mathcal A \times \mathcal B}(G_0', G_1')$: for $(a, b) \in ({\mathcal A \times \mathcal B})((A_0, B_0), (A_1, B_1))$,

$$\begin{align} & G_1'(a, b) \psi'(A_0, B_0) = \\ & G_1(A_1)(b) G_1(a)(B_0) \cdot \psi(A_0)(B_0) = \\ & G_1(A_1)(b) \cdot G_1(a)(B_0) \psi(A_0)(B_0) = \\ & G_1(A_1)(b) \cdot (G_1(a)\psi(A_0))(B_0) = \\ & G_1(A_1)(b) \cdot (\psi(A_1)G_0(a))(B_0) = \\ & G_1(A_1)(b) \cdot \psi(A_1)(B_0) G_0(a)(B_0) = \\ & G_1(A_1)(b) \psi(A_1)(B_0) \cdot G_0(a)(B_0) = \\ & \psi(A_1)(B_1) G_0(A_1)(b) \cdot G_0(a)(B_0) = \\ & \psi(A_1)(B_1) \cdot G_0(A_1)(b) G_0(a)(B_0) = \\ & \psi'(A_1, B_1) G_0'(a, b). \end{align}$$

$-'$ is a functor:

$$\begin{align} & 1_G'(A, B) = \\ & 1_G(A)(B) = \\ & 1_{G(A)}(B) = \\ & 1_{G(A)(B)} = \\ & 1_{G'(A, B)} = \\ & 1_{G'}(A, B); \end{align}$$

and for $\psi_0 \in ({\mathcal C}^{\mathcal B})^{\mathcal A}(G_0, G_1)$, $\psi_1 \in ({\mathcal C}^{\mathcal B})^{\mathcal A}(G_1, G_2)$,

$$\begin{align} & (\psi_1 \psi_0)'(A, B) = \\ & (\psi_1 \psi_0)(A)(B) = \\ & (\psi_1(A) \psi_0(A))(B) = \\ & \psi_1(A)(B) \psi_0(A)(B) = \\ & \psi_1'(A, B) \psi_0'(A, B). \end{align}$$

3. INVERSES

${-^*}' = 1$:

$$\begin{align} & {F^*}'(A, B) = \\ & F^*(A)(B) = \\ & F(A, B); \end{align}$$

for $(a, b) \in ({\mathcal A \times \mathcal B})((A_0, B_0), (A_1, B_1))$,

$$\begin{align} & {F^*}'(a, b) = \\ & F^*(A_1)(b) F^*(a)(B_0) = \\ & F(1_{A_1}, b) F(a, 1_{B_0}) = \\ & F(1_{A_1}a, b 1_{B_0}) = \\ & F(a, b); \end{align}$$

and

$$\begin{align} & {\phi^*}'(A, B) = \\ & \phi^*(A)(B) = \\ & \phi(A, B). \end{align}$$

${-'}^* = 1$:

$$\begin{align} & G'^*(A)(B) = \\ & G'(A, B) = \\ & G(A)(B); \end{align}$$

for $b \in {\mathcal B}(B_0, B_1)$,

$$\begin{align} & G'^*(A)(b) = \\ & G'(1_A, b) = \\ & G(1_A)(B_0) G(A)(b) = \\ & 1_{G(A)}(B_0) G(A)(b) = \\ & 1_{G(A)(B_0)} G(A)(b) = \\ & G(A)(b); \end{align}$$

for $a \in {\mathcal A}(A_0, A_1)$,

$$\begin{align} & G'^*(a)(B) = \\ & G'(a, 1_B) = \\ & G(a)(B)G(A_1)(1_B) = \\ & G(a)(B)1_{G(A_1)(B)} = \\ & G(a)(B); \end{align}$$

and finally

$$\begin{align} & \psi'^*(A)(B) = \\ & \psi'(A, B) = \\ & \psi(A)(B). \end{align}$$

QED (and congratulations on reading this far).

Answer 1

You're working too hard. Let's restrict attention to small categories so that we can ignore set-theoretic issues. The construction of the functor category is a special case of the construction of the exponential object in a cartesian closed category; in particular, by definition it has the universal property

$$\text{Hom}(X, Y^Z) \cong \text{Hom}(X \times Z, Y)$$

where $X, Y, Z$ are objects in a cartesian closed category, which in our case is the category of small categories. (There is some work to be done here in verifying that the standard construction of the functor category actually has this universal property, which I will omit.) Now observe that

$$\text{Hom}(X, Y^{Z_1 \times Z_2}) \cong \text{Hom}(X \times Z_1 \times Z_2, Y) \cong \text{Hom}(X \times Z_2, Y^{Z_1}) \cong \text{Hom}(X, (Y^{Z_1})^{Z_2}).$$

Hence, as Zhen Lin says in the comments, we conclude that $Y^{Z_1 \times Z_2} \cong (Y^{Z_1})^{Z_2}$ by the Yoneda lemma. This proof works in any cartesian closed category, and the size issues are a distraction.