El enfoque algebraico de Fokkinga frente a la construcción tradicional de flechas de un producto

Question

En su documento: "Calculate Categorically", Maarten Fokkinga invita a los lectores a comparar los cálculos algebraicos con las pruebas pictóricas habituales de la teoría de categorías.

Me gustaría hacer precisamente eso, utilizando "Categorías elementales, topos elementales" (Colin McClarty) como texto "habitual".

McClarty presenta el teorema 2.1 como Si P, $p_1$ , $p_2$ es un diagrama de producto para A y B, y hay una iso $f:Q \rightarrow P$ entonces Q, $p_1 \circ f$ , $p_2 \circ f$ es también un diagrama de producto para A y B.

Mi formulación de ese teorema comenzó estableciendo la verdad de la teoría de Fokkinga $(\vartriangle-TYPE)$ cuya instancia para el teorema 2.1 es:

$f;p_1:Q \rightarrow A \wedge f;p_2:Q \rightarrow B \Rightarrow f;p_1 \vartriangle f ; p_2 : Q \rightarrow A \times B $

Pero ahora no sé qué hacer. ¿Establecer $(\vartriangle-TYPE)$ ¿es suficiente para demostrar que hemos construido un producto para A y B? El estudio de la prueba de McClarty me sugiere que tengo que hacer más, pero no estoy seguro de qué es lo siguiente.

Answer 1

Que no usas el hecho de que $f$ es un isomorfismo en absoluto debería ser un fuerte indicador de que no has terminado. Creo que puedes estar malinterpretando lo que dice el teorema. Ya sabes que hay un producto, a saber $A\times B$ , para $A$ y $B$ . Lo que se quiere demostrar es que si $Q \cong A\times B$ entonces $Q$ es un producto. Para todas las construcciones de "Calcular categóricamente", el único resultado que necesita establecer es el de CHARN (caracterización). Por lo tanto, todo lo que necesita hacer es definir concretamente un $\vartriangle_Q$ que producirá una flecha en $Q$ y tienes que mostrar $\vartriangle$ -CHARN con eso $\vartriangle_Q$ y $exl = f;p_1$ y $exr = f;p_2$ . Eso es lo que hay que demostrar: $$x;f;p_1 = h\ \land\ x;f;p_2 = k\ \iff\ x = h\vartriangle_Q k $$ Para empezar, la definición de $\vartriangle_Q$ es $$h \vartriangle_Q k \equiv h\vartriangle k;f^{-1}$$