Componiendo duplicación y proyecciones

Question

Supongamos que tengo una categoría cerrada cartesiana $\mathcal{C}$ con proyección $(\pi_1)_{A \times B} : A\times B \to A$, duplicación $\delta_{A} : A \to A \times A$ y asociador $\alpha_{A,B,C} : (A \times B) \times C \to A \times (B \times C)$.

¿Lo siguiente es conmutativo?

$$ \require{AMScd} \begin{CD} A \times B @>{\delta_A \times id_B }>> (A \times A) \times B \\ @V\delta_{A \times B}VV @VV{\alpha_{A,A,B}}V \\ (A \times B) \times (A \times B) @>{(\pi_1)_{A \times B} \times id_{A \times B}}>> A \times (A \times B) \end{CD} $$

¡Me parece obvio que debería serlo, pero no puedo demostrarlo!

Answer 1

No necesitas un cierre, una categoría cartesiana está bien.

El enfoque del martillo grande es notar que el lenguaje interno de las categorías cartesianas se parece y se siente como Álgebra Universal (multiclase), es decir, una flecha $A\times B \times C \to D$ se puede pensar como un término con tres variables de tipo $A$, $B$ y $C. Es decir, tienes términos como $x:A, y:B, z:C \vdash \mathtt{f}(\mathtt{g}(x,x,y),\mathtt{h}(z))$. Una flecha $A\times B\times C \to D\times E$ es simplemente una tupla de términos. La ventaja es que puedes utilizar esencialmente una notación matemática "normal", de maneras normales, siempre y cuando solo la uses de ciertas maneras, bastante obvias, y lo que diga correspondará a afirmaciones verdaderas. Si insistes en el cierre cartesiano, puedes usar cálculo lambda simplemente tipado con productos, permitiendo operaciones matemáticas más "normales", a saber, curryficación y pasar funciones como parámetros.

Por supuesto, si quisieras demostrar las afirmaciones anteriores, necesitarías poder manejar situaciones como la que estás preguntando. El truco aquí es que estás tratando a $\delta$ y $\alpha$ como primitivos, pero se pueden definir en términos de las proyecciones y las tuplas que son $\langle -,=\rangle_{ABC} : \text{Hom}(A,B)\times\text{Hom}(A,C)\to\text{Hom}(A,B\times C)$. En particular, tenemos la propiedad universal: $$\pi_i \circ \langle f_1,f_2\rangle = f_i \quad \text{y}\quad \langle\pi_1 \circ t,\pi_2\circ t\rangle = t$$ Podemos definir $\delta \equiv \langle id,id\rangle$, $f\times g \equiv \langle f\circ\pi_1,g\circ\pi_2\rangle$, y $\alpha \equiv \langle id\times\pi_1,\pi_2\circ\pi_2\rangle$. Ahora solo tienes que expandir las definiciones y aplicar las ecuaciones proporcionadas por la propiedad universal. Para ser sistemático al respecto, para demostrar $h = k : A \to B\times C, simplemente necesitas probar $\pi_i \circ h = \pi_i \circ k$ para $i = 1,2$ (porque luego podemos usar la segunda ecuación en la propiedad universal para mostrar $h = k). Puedes aplicar esto varias veces hasta obtener una colección de ecuaciones de la forma $A \to B$ donde $B$ no es un producto. En este punto, puedes aplicar sistemáticamente la primera (pareja de) ecuación(es) de la propiedad universal hasta que desaparezcan todas las instancias de $\langle -,=\rangle$. El proceso es completamente mecánico. Si eres programador, podrías hacer un pequeño simplificador para hacerlo por ti. Sería un ejercicio bastante sencillo.

Answer 2

Primero, observa que $\alpha = \langle \pi_1 \circ \pi_1, \pi_2 \times \mathrm{id} \rangle$ y $\delta = \langle \mathrm{id}, \mathrm{id}\rangle$.

Las siguientes igualdades son válidas:

1. $\langle f , g \rangle \circ h = \langle f \circ h , g \circ h \rangle$
2. $\pi_i \circ (f_1 \times f_2) = f_i \circ \pi_i$
3. $\pi_i \circ \langle f_1, f_2 \rangle = f_i$
4. $(f_1 \times f_2) \circ (g_1 \times g_2) = (f_1 \circ g_1) \times (f_2 \circ g_2)$

\begin{align*} \alpha \circ (\delta \times \mathrm{id}) &= \langle \pi_1 \circ \pi_1, \pi_2 \times \mathrm{id} \rangle \circ (\delta \times \mathrm{id}) \tag{Def .of $\alpha$}\\ &= \langle \pi_1 \circ \pi_1 \circ (\delta \times \mathrm{id}), (\pi_2 \times \mathrm{id})\circ (\delta \times \mathrm{id}) \rangle \tag{Por 1.}\\ &= \langle \pi_1 \circ \pi_1 \circ (\langle \mathrm{id}, \mathrm{id}\rangle \times \mathrm{id}), (\pi_2 \times \mathrm{id})\circ (\langle \mathrm{id}, \mathrm{id}\rangle \times \mathrm{id}) \rangle \tag{Def. de $\delta$}\\ &= \langle \pi_1 \circ \langle \mathrm{id}, \mathrm{id}\rangle\circ \pi_1 , (\pi_2 \times \mathrm{id})\circ (\langle \mathrm{id}, \mathrm{id}\rangle \times \mathrm{id}) \rangle \tag{Por 1.}\\ &= \langle \pi_1 \circ \langle \mathrm{id}, \mathrm{id}\rangle\circ \pi_1 , ((\pi_2 \circ \langle \mathrm{id}, \mathrm{id}\rangle) \times \mathrm{id}\rangle \tag{Por 4.}\\ &= \langle \mathrm{id} \circ \pi_1 , \mathrm{id} \times \mathrm{id}\rangle \tag{Por 3.}\\ &= \langle \pi_1 , \mathrm{id}\rangle\\ &= (\pi_1 \times \mathrm{id}) \circ \delta \end{align*}