En las categorías de funtores, hay un bonito isomorfismo ${\mathcal C}^{\mathcal A \times \mathcal B} \cong ({\mathcal C}^{\mathcal B})^{\mathcal A}$ . Probar esto es un buen ejercicio. No es exactamente difícil, pero hay muchos detalles. Lambek y Scott se refieren a la prueba como "larga", y no bromean. A continuación se muestra una prueba bastante cuidadosa, que necesita aproximadamente un centenar de ecuaciones.
Pregunta . ¿Podemos mejorar esta prueba? Por ejemplo, podríamos derivarla de algún otro resultado; o podríamos argumentar que el functor ${\mathcal C}^{\mathcal A \times \mathcal B} \to ({\mathcal C}^{\mathcal B})^{\mathcal A}$ es biyectiva en algún sentido y, por lo tanto, debe tener una inversa, o podríamos simplemente sacar un lema para simplificar el argumento.
PROOF
La prueba consta de cuatro partes. En la parte 0 establecemos las definiciones básicas y la notación; en la parte 1 construimos un funtor de la izquierda a la derecha; en la parte 2 hacemos lo mismo de derecha a izquierda; y en la parte 3 demostramos que estos dos funtores son inversos.
0. DEFINICIONES BÁSICAS Y NOTACIÓN
$F \in \operatorname{Ob} {\mathcal B}^{\mathcal A}$ significa $F$ es un functor $\mathcal A \to \mathcal B$ : para $A \in \operatorname{Ob} \mathcal A$ ,
$$F(1_A) = 1_{F(A)}, \tag{F0}$$
y para $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)$ significa $\epsilon$ es una transformación natural $F_0 \to F_1$ : para $a \in {\mathcal A}(A_0, A_1)$ ,
$$F_1(a)\epsilon(A_0) = \epsilon(A_1)F_0(a). \tag{FC0}$$
También tenemos, para $\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}$$
y para $F \in \operatorname{Ob} {\mathcal B}^{\mathcal A}$ , $A \in \operatorname{Ob} \mathcal A$ ,
$$1_F(A) = 1_{F(A)}. \tag{FC2}$$
1. FUNCTOR DE IZQUIERDA A DERECHA
Definiremos un functor $-^*: {\mathcal C}^{\mathcal A \times \mathcal B} \to ({\mathcal C}^{\mathcal B})^{\mathcal A}$ .
Para $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$ , definir $F^*(A)$ por
$$\begin{align} & F^*(A)(B) := F(A, B), \tag{LTR0}\\ & F^*(A)(b) := F(1_A, b). \tag{LTR1} \end{align}$$
$F^*(A)$ es un functor en $\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}$$
y para $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}$$
Para $a \in {\mathcal A}(A_0, A_1)$ , defina $F^*(a)$ por
$$\begin{align} & F^*(a)(B) := F(a, 1_B). \tag{LTR2} \end{align}$$
$F^*(a)$ es una transformación natural en ${\mathcal C}^{\mathcal B}(F^*(A_0), F^*(A_1))$ : para $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^*$ es un functor en $\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}$$
y para $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}$$
Para $\phi \in {\mathcal C}^{\mathcal A \times \mathcal B}(F_0, F_1)$ , definir $\phi^*(A)$ por
$$\begin{align} & \phi^*(A)(B) := \phi(A, B). \tag{LTR3} \end{align}$$
$\phi^*(A)$ es una transformación natural en ${\mathcal C}^{\mathcal B}(F_0^*(A), F_1^*(A))$ : para $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^*$ es una transformación natural en $({\mathcal C}^{\mathcal B})^{\mathcal A}(F_0^*, F_1^*)$ : para $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}$$
Finalmente, $-^*$ es un 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}$$
y para $\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. FUNCTOR DE DERECHA A IZQUIERDA
Definiremos un functor $-': ({\mathcal C}^{\mathcal B})^{\mathcal A} \to {\mathcal C}^{\mathcal A \times \mathcal B}$ .
Para un functor $G \in \operatorname{Ob} ({\mathcal C}^{\mathcal B})^{\mathcal A}$ , definir $G'$ por
$$\begin{align} & G'(A, B) := G(A)(B) \tag{RTL0} \end{align}$$
y para $a \in {\mathcal A}(A_0, A_1)$ , $b \in {\mathcal B}(B_0, B_1)$ , definir
$$\begin{align} & G'(a, b) := G(A_1)(b) G(a)(B_0). \tag{RTL1} \end{align}$$
$G'$ es un 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}$$
y para $(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}$$
Para $\psi \in ({\mathcal C}^{\mathcal A})^{\mathcal B}(G_0, G_1)$ , definir $\psi'$ por
$$\begin{align} & \psi'(A, B) := \psi(A)(B). \tag{RTL2} \end{align}$$
$\psi'$ es una transformación natural en ${\mathcal C}^{\mathcal A \times \mathcal B}(G_0', G_1')$ : para $(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}$$
$-'$ es un 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}$$
y para $\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. INVIERTE EN
${-^*}' = 1$ :
$$\begin{align} & {F^*}'(A, B) = \\ & F^*(A)(B) = \\ & F(A, B); \end{align}$$
para $(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}$$
y
$$\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}$$
para $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}$$
para $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}$$
y finalmente
$$\begin{align} & \psi'^*(A)(B) = \\ & \psi'(A, B) = \\ & \psi(A)(B). \end{align}$$
QED (y enhorabuena por haber leído hasta aquí).
