nicer proof of basic functor category fact?

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).

• It's true in any cartesian closed category. The quickest way to verify it is by using the Yoneda lemma. Commented Jan 2, 2015 at 1:15

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.

• Thanks, I'll look into that. How would you remove the size issues in general? In order to use this approach, must we assume that $\mathcal A$, $\mathcal B$, $\mathcal C$ are objects in some larger category? Commented Jan 2, 2015 at 17:09
• @HewWolff For example, you can use Grothendieck's universes, and there will be a universe $\mathbb U$ large enough so that $\mathcal A,\mathcal B,\mathcal C$ are all three $\mathbb U$-small. So you can work in the category of $\mathbb U$-small categories.
– Pece
Commented Jan 2, 2015 at 17:32
• @QiaochuYuan, can you say more about what you mean by $\operatorname{Hom}(X, Y^Z) \cong \operatorname{Hom}(X \times Z, Y)$? Is this an isomorphism between functors $\operatorname{Cat}^3 \to \operatorname{Set}$, or maybe just a bijection between sets? Commented Jan 11, 2015 at 20:12
• Also, I notice that in the books I'm using, this exercise appears just before Yoneda's Lemma, which suggests that we should be able to do the exercise without using Yoneda. But I'm curious about any approach which works. Commented Jan 11, 2015 at 20:20
• @Hew: yes, it's a natural isomorphism between functors, although you missed an op. I mean, you can always deprive yourself of your tools if you want, but if you aren't using the universal property then you have no choice but to use the construction, which as you've seen results in an annoyingly and pointlessly long proof if you want the full details. Commented Jan 12, 2015 at 12:45