Productos en teoría de categorías versus productos en teoría de conjuntos

En la teoría de conjuntos (tradicional),$A\times B$se refiere a un conjunto en particular. Qué conjunto es algo arbitrario, pero tienes que tomar alguna decisión. Una vez que tome esa decisión, todas las demás elecciones que podría haber hecho para la definición de$A \times B$ya no es el producto binario; está solo en biyección con su bendito producto binario "real". Estas elecciones arbitrarias pero técnicamente necesarias impregnan la teoría de conjuntos porque preguntas como "es$\{\{a\},\{a,b\}\}$un miembro de$A\times B$?" son preguntas válidas con una respuesta particular.

La historia en la teoría de categorías depende de cómo se formalice. El enfoque típico es definir una categoría como un modelo "grande" de una teoría en (una extensión adecuadamente poderosa de) la teoría de conjuntos. En este contexto, la propiedad universal de los productos no selecciona ningún objeto en particular. De hecho, hay una clase apropiada de objetos en$\mathbf{Set}$que satisfacen la propiedad universal de$A\times B$para una dada$A$y$B$. Todos ellos son igualmente"$A\times B$". Similarmente,$(A\times B)\times C$y$A\times(B\times C)$tienen tanto derecho a ser$A\times B\times C$como cualquier otro objeto isomorfo. Por otro lado, si realmente queremos usar la notación$A\times B$, eso es si queremos un funtor$-\,\times =\, : \mathbf{Set}\times\mathbf{Set}\to\mathbf{Set}$, entonces esto requiere hacer una elección específica. A partir de ahí, la situación es bastante similar a la situación en la teoría de conjuntos.

Un enfoque diferente para formalizar la teoría de categorías es usar un marco lógico más apropiado. En el extremo más débil del espectro está FOLDS . En el extremo más poderoso del espectro se encuentra la teoría de tipos dependientes o incluso la teoría de tipos homotópicos . Dado que este libro parece tratar sobre lógica matemática, es posible que adopte ese enfoque. El hecho clave en este caso es que la igualdad de objetos ya no es un concepto definido y la igualdad de flechas solo tiene sentido entre flechas en el mismo "conjunto" hom. Ahora, la asociatividad (estricta) del producto categórico simplemente no es una pregunta que pueda hacer. Simplemente no tiene sentido preguntar si$(A\times B)\times C = A\times(B\times C)$. Es una declaración mal formada como$3\land P$es. Todavía es significativo preguntar si$(A\times B)\times C\cong(A\times B)\times C$aunque.

Este es un enfoque formal para validar el principio categórico de equivalencia que establece que todas las propiedades categóricas (superiores) deben ser invariantes con respecto al isomorfismo (/ equivalencia). Este es el principio detrás de la práctica omnipresente (tanto dentro como fuera de la teoría de categorías) de tratar los objetos isomórficos como iguales. Este principio no suele ser cierto.$\{\{a\},\{a,b\}\}\in A\times B$no es una propiedad que sea invariante con respecto al isomorfismo. En una formalización de categorías en FOLDS, esto es cierto en el sentido de que para cualquier fórmula de FOLDS podemos escribir, si se cumple para un objeto, se cumple para todos los objetos isomorfos. En la teoría de tipos de homotopía (que está íntimamente relacionada con la teoría de categorías superiores) esto se lleva aún más lejos. El axioma de univalencia es básicamente el principio de equivalencia tomado como axioma. establece que para todo tipo$A$y$B$,$(A =_{\mathsf{Type}} B)\simeq (A \simeq B)$que establece que el tipo de "igualdades" entre tipos$A$y$B$es equivalente al tipo de equivalencias entre$A$y$B$. El resultado es que en la teoría de tipos homotópicos, los tipos equivalentes pueden tratarse como iguales. Entonces$(A\times B)\times C=_{\mathsf{Type}}A\times(B\times C)$es "verdadero" en la teoría del tipo de homotopía. El costo de esto es una noción mucho más sutil de "igualdad".

Casari no estaba pensando en la teoría del tipo de homotopía ya que no existía cuando se publicó el libro, pero los PLIEGUES (o marcos similares) y el principio de equivalencia son mucho más antiguos.

El producto de conjuntos no es asociativo de hecho:

... fundamentalmente porque las "tuplas" (independientemente de cómo elija construirlas en la construcción de su teoría de conjuntos) no son asociativas. Ahora, puedo decir que hay un isomorfismo natural entre estos dos productos, tomados en diferentes órdenes: tomo las tuplas en la 'mitad izquierda' de cada elemento del primer conjunto y las reagrupo para obtener los elementos del segundo conjunto. Puedo mostrar que esto siempre es biyectivo. Entonces, para cualquier conjunto$A, B, C$, hay un isomorfismo natural$\phi$tal que$\phi((A\times B)\times C) = A\times(B\times C)$

Pero que tenga que hablar explícitamente sobre este isomorfismo es, en cierto sentido, preocupante. ¿Cómo se verá esto cuando tome productos de 4 cosas, con todas sus diferentes agrupaciones? ¿Y si quiero llevarme un producto infinito? Y de hecho habrá mucho más trabajo en cada paso porque, en realidad, solo hay isomorfismos.

La definición teórica de la categoría es, en cierto sentido, más limpia. La definición de la teoría de conjuntos está un poco atascada como una operación binaria, porque está construida usando pares/tuplas. Pero la definición de la categoría simplemente dice "hay una colección de flechas tales que yada yada conmuta". Esa colección generalmente es solo 2 flechas, para un producto binario normal, pero puede tener muchas flechas arbitrariamente, y todos los mismos argumentos se mantendrán bien. En este sentido, la definición teórica de categoría de producto se generalizará mucho más fácilmente.