Posterior a de una larga búsqueda de datos pudimos resolver este contratiempo que suelen tener ciertos de nuestros lectores. Te compartimos la respuesta y esperamos que te sea de mucha ayuda.
Solución:
Desde un punto de vista formal, es posible estudiar la teoría de categorías dentro de la teoría de categorías, utilizando la noción de topos. La teoría de Topos hace muchas cosas, pero una cosa que proporciona es una base alternativa de teoría de categorías para las matemáticas.
Al aumentar la teoría topos con suficientes axiomas adicionales, es teóricamente posible reconstruir todo el ZFC dentro de la teoría topos. Entonces, si alguien puede estudiar la teoría de categorías en ZFC, ¡puede hacer lo mismo estudiando la teoría de categorías dentro de ZFC dentro de la teoría de topos! O simplemente pueden estudiar la teoría de categorías usando la teoría topos sin usar ZFC como paso intermedio. Un desafío práctico para hacer esto es que los axiomas de un topos son posiblemente más complicados que los axiomas de ZFC, que además del reemplazo pueden justificarse en términos de propiedades relativamente básicas de los conjuntos.
Otra forma de ver algunas cuestiones planteadas en este hilo es observar la noción de escribe. Existe una buena analogía para la diferencia entre ZFC y algunos fundamentos categóricos: es como la diferencia entre un lenguaje de programación sin tipo (como Scheme) y un lenguaje fuertemente tipado (como Java o C ++).
En Scheme y otros lenguajes sin tipo, no hay separación entre el código y los datos: dados dos objetos cualesquiera, podemos tratar el primero como una función, el segundo como una entrada y (intentar) calcular la salida correspondiente. Entonces, por ejemplo, podríamos definir números naturales usando números de la Iglesia, tratar “$ 5 $” como una función y calcular su valor en el par ordenado $ (0,17) $. Por supuesto, nadie hace esto en serio en la práctica. De manera similar, en ZFC, podemos preguntarnos si $ pi $ es un miembro del par ordenado $ (8, mathbb R) $, aunque en la práctica nadie lo hace en serio.
En Java y C ++, existen definiciones estrictas de cada tipo de datos. Por ejemplo, si tengo un objeto de “número natural” y quiero un objeto de “número real”, necesito convertir (“emitir”) el objeto original para que tenga el tipo apropiado. Por lo tanto, no puedo agregar directamente $ 1_ mathbb N $ y $ pi_ mathbb R $. Esto es similar a la forma en que algunas fundaciones categóricas manejan las cosas. En lugar de hablar de “casting”, estos fundamentos se centran en el “mapa de inclusión natural” desde $ mathbb N $ a $ mathbb R $, etc.
Vale la pena saber que existen muchas otras teorías de tipos, además de las inspiradas en la teoría topos. Existe la teoría de tipos intuicionista, que es muy poderosa, y la aritmética clásica de segundo orden, que es mucho más débil pero que todavía es capaz de formalizar casi todas las matemáticas de pregrado.
Creo que, al igual que muchos que trabajan en los fundamentos de las matemáticas, las ingenuas matemáticas informales que se encuentran en la práctica se realizan en una especie de teoría de tipos complicada (e informal). Esto hace que los fundamentos de la teoría de tipos sean mucho más naturales para muchos matemáticos; muchas de las objeciones planteadas a ZFC se basan en la falta de tipeo en la teoría de conjuntos. Los fundamentos simples de la teoría de tipos serían posiblemente un sistema formal más natural que ZFC para muchos propósitos prácticos, al igual que Java es un lenguaje más práctico que Scheme para muchos propósitos.
Por otro lado, la falta de tipeo en ZFC, como la falta de tipeo en Scheme, es útil para muchos propósitos teóricos, por lo que es bueno para los matemáticos estar al tanto de los sistemas sin tipear. Por ejemplo, para hacer un modelo de ZFC solo necesitamos definir una relación indefinida, $ in $. Para hacer un modelo de teoría de tipos, tenemos que diseñar el sistema de tipos, luego establecer nuestro dominio a para cada tipo y también diseñar todos los mapas entre tipos y operaciones en cada tipo individual. Esto es mucho más complicado. De manera análoga, es un ejercicio común en las clases de informática pedir a los estudiantes que escriban un intérprete de esquemas en Scheme, o incluso que escriban un compilador de Scheme en lenguaje ensamblador, pero no es común pedirles a los estudiantes que escriban un intérprete de Java completo en Java. mucho menos en lenguaje ensamblador.
La teoría de conjuntos ZF, en aras de la especificidad, le permite hacer preguntas que yo (y probablemente muchos otros teóricos de categorías) considero sin sentido: porque los elementos de conjuntos son otros conjuntos, para cualquier par de conjuntos $ X $ y $ Y $ , es significativo en ZF preguntar si $ X $ es un elemento o un subconjunto de $ Y $. Por ejemplo, puede preguntar si $ mathbb R $ es un elemento o un subconjunto de $ pi $. Mi principal motivación para evitar la teoría de conjuntos es evitar este tipo de preguntas sin sentido, que creo que realmente hacen que las matemáticas sean más difíciles de aprender.
(Los enunciados sobre conjuntos que considero significativos son los que puede hacer en la teoría elemental de la categoría de conjuntos; por ejemplo, puede preguntar si dos conjuntos son isomorfos, cuál es el límite o colimit de un diagrama de conjuntos, etc. .)
(Por ejemplo, en matemáticas. SE Una vez vi la pregunta “¿Se supone que los homsets en una categoría son disjuntos o pueden tener una intersección no trivial?” Y la respuesta correcta es que esta es una pregunta sin sentido, pero dependiendo de cuán profundamente alguien bebido el kool-aid de ZF, esta puede ser una explicación molestamente difícil de tragar).
Los “objetos” en una descripción directa de categorías tienen el mismo estatus ontológico que los “conjuntos” en una descripción directa de modelos de la teoría de conjuntos.
Como ha señalado Kevin en los comentarios, una posible axiomatización de la “teoría de categorías” es la teoría elemental de la categoría de categorías. La mejor referencia que he podido encontrar es un artículo de McLarty (que no es necesariamente la formulación original de Lawvere).
En él, McClarty presenta una teoría de dos ordenadas, con un tipo de variables que van por categorías y el otro por functores. Él muestra cómo a partir de 8 axiomas (uno por esquema), esta teoría puede formular y probar muchos resultados estándar de la teoría de categorías, incluidas propiedades que uno no podría esperar de inmediato, por ejemplo, propiedades de la categoría de grupos $ G $ en una categoría dada $ A $ (aquí $ G $ y $ A $ son ambos objetos de la teoría), y de una mónada (triple) en una categoría.
Por tanto, es posible que en esta línea se puedan dar axiomas suficientes para el razonamiento habitual utilizado por los teóricos de categorías.
Sin embargo, no me parece que esto se haya hecho todavía de manera concluyente: hay muchas nociones que usan los teóricos de categorías (al echar un vistazo a los títulos en el último número de la revista de teoría de una categoría, vemos una fuerte homotopía, categorías modelo, trenzado débil categorías monoidales, extensiones kan algebraicas, etc.), la mayoría de las cuales son mucho más complicadas que las que trata McClarty. Además, a los teóricos de las categorías siempre se les ocurren nuevas nociones, por ejemplo, bastante recientemente (creo …), $ infty $ -categories y cosas por el estilo. Cuando se formulan estas nociones, no funcionan en ETCC: las construcciones utilizadas para definir un nuevo tipo de categoría y dar ejemplos de ella son a menudo (en la base) en términos de conjuntos; por ejemplo, una categoría $ infty $ tiene una categoría infinita torre de conjuntos de morfismos (morfismos, morfismos entre morfismos, etc.). Eso podría ser que un día a alguien se le ocurrirá una definición de $ infty $ -categories en términos de ETCC: pero (que yo sepa) esto no se ha hecho, y no hay una manera uniforme de traducir las caracterizaciones teóricas de conjuntos que son en realidad dado de “tipos” de categorías (como $ infty $ -categories) en el lenguaje de ETCC.
Si esto es correcto, no parece que se hayan propuesto axiomas suficientes para las prácticas actuales de la teoría de categorías (que incluye la opción de definir nuevos tipos de categorías). En este sentido, la teoría de categorías todavía necesita en la actualidad la formulación de la teoría de conjuntos.
EDITAR: Aunque en realidad parece que puede hacer análogos de muchos razonamientos teóricos de conjuntos en ETCS, probablemente también en ETCC, por lo que es posible que pueda traducir el tipo de construcciones teóricas de conjuntos que mencioné anteriormente a ETCC después de todo. Posiblemente, la principal diferencia entre tales teorías categóricas y la teoría de conjuntos es entonces lo que menciona Qiaochu: que las teorías categóricas no permiten la formulación de ciertas preguntas irrelevantes.
Sección de Reseñas y Valoraciones
Recuerda algo, que tienes la capacidad de aclarar tu experiencia si te fue preciso.