Principio de reflexión vs universos
En las discusiones de teoría de categorías, a menudo existe la tentación de mirar la categoría de todos los grupos abelianos, o de todas las categorías, etc., lo que rápidamente conduce a los problemas habituales de la teoría de conjuntos. Estos a menudo se evitan mediante el uso de universos de Grothendieck. En el lenguaje de la teora de conjuntos, uno corrige algunos aspectos cardinales fuertemente inaccesibles$\kappa$ -- esto significa que $\kappa$ es un cardenal incontable tal que para todos $\lambda<\kappa$, además $2^\lambda<\kappa$y para cualquier conjunto de $<\kappa$ muchos conjuntos $S_i$ de tamaño $<\kappa$, también su unión es de tamaño $<\kappa$. Esto implica que el escenario$V_\kappa\subset V$ de "conjuntos de tamaño $<\kappa$"es en sí mismo un modelo de ZFC: al aplicar cualquiera de las operaciones en conjuntos, como tomar conjuntos de potencias o uniones, nunca puedes irte $V_\kappa$. Estos conjuntos se denominan entonces "pequeños", y luego la categoría de pequeños grupos abelianos está definitivamente bien definida.
Históricamente, este enfoque fue utilizado por primera vez por Grothendieck; un texto fundamental más reciente es el trabajo de Lurie sobre$\infty$-categorías. Sin embargo, su uso siempre ha creado una especie de reacción violenta, y algunas personas no están dispuestas a dejar que los axiomas más allá de ZFC se cuelen en la literatura establecida. Por ejemplo, creo que en algún momento hubo una larga discusión sobre si el último teorema de Fermat había sido probado en ZFC, ahora resuelto por McLarty. Más recientemente, he visto surgir argumentos similares para teoremas cuyas demostraciones se refieren al trabajo de Lurie. (Personalmente, no tengo fuertes sentimientos sobre esto y entiendo los argumentos de cualquier manera).
Por otro lado, siempre ha sido el caso que una inspección más cercana reveló que cualquier uso de universos era, de hecho, innecesario. Por ejemplo, el Proyecto Stacks no usa universos. En cambio, (ver Tag 000H dice) efectivamente debilita la hipótesis de que$\kappa$ es fuertemente inaccesible, a algo así como un fuerte límite cardinal de incontable cofinalidad, es decir: para todos $\lambda<\kappa$, uno tiene $2^\lambda<\kappa$, y siempre que tenga una colección contable de conjuntos$S_i$ de tamaño $<\kappa$, también la unión de la $S_i$ tiene tamaño $<\kappa$. ZFC prueba fácilmente la existencia de tales$\kappa$, y casi todos los argumentos que uno podría imaginarse haciendo en la categoría de grupos abelianos en realidad también funcionan en la categoría de $\kappa$-pequeños grupos abelianos para tales $\kappa$. Si uno hace argumentos más complicados, en consecuencia, puede fortalecer la hipótesis inicial sobre$\kappa$. Tuve la oportunidad de jugar este juego yo mismo, consulte la Sección 4 de www.math.uni-bonn.de/people/scholze/EtCohDiamonds.pdf para ver el resultado. A partir de esta experiencia, estoy bastante seguro de que uno puede reescribir de manera similar la "Teoría del Topos Superior" de Lurie, o cualquier otro trabajo de teoría de categorías similar, de manera de eliminar todos los cardenales fuertemente inaccesibles, reemplazándolos por cuidadosamente elegidos$\kappa$ con propiedades como las anteriores.
De hecho, parece haber un teorema de ZFC, el principio de reflexión (discutido brevemente en Tag 000F del proyecto Stacks, por ejemplo), que parece garantizar que esto siempre sea posible. Es decir, para cualquier conjunto finito dado de fórmulas de teoría de conjuntos, hay algunos$\kappa$ de tal manera que, en términos generales, estas fórmulas se mantienen en $V_\kappa$ si y solo si aguantan $V$. Esto parece decir que para cualquier conjunto finito dado de fórmulas, uno puede encontrar algunos$\kappa$ tal que $V_\kappa$se comporta como un universo con respecto a estas fórmulas, pero por favor corríjame en mi muy ingenua comprensión del principio de reflexión. (Un hecho relacionado es que ZFC demuestra la consistencia de cualquier fragmento finito dado de los axiomas de ZFC).
Por otro lado, cualquier texto matemático dado sólo contiene un número finito de fórmulas (a menos que establezca un "esquema de teorema", lo que no suele suceder, creo). Por tanto, la pregunta está formulada de forma ligeramente provocativa:
¿El principio de reflexión implica que debe ser posible reescribir la teoría del Topos superior de una manera que evite el uso de universos?
Editar (28.01.2021): ¡ Muchas gracias por todas las respuestas tan útiles! Creo que ahora tengo una imagen mucho más clara de la situación, pero todavía no estoy exactamente seguro de cuál es la respuesta a la pregunta.
Por lo que entiendo, (aproximadamente) el mejor meta-teorema en esta dirección es el siguiente (especializado en HTT). Recuerde que HTT corrige dos cardenales fuertemente inaccesibles$\kappa_0$ y $\kappa_1$, dejando espacio para pequeños (en $V_{\kappa_0}$), grande (en $V_{\kappa_1}$), y muy grande (en $V$) objetos. A continuación, se puede intentar leer HTT en el siguiente sistema de axiomas (este es esencialmente el del artículo de Feferman "Fundamentos de la teoría de conjuntos de la teoría de categorías", y también se ha propuesto en la respuesta de Rodrigo Freire más adelante).
(i) Los axiomas habituales de ZFC
(ii) Otros dos símbolos $\kappa_0$ y $\kappa_1$, con los axiomas de que son cardinales, que la cofinalidad de $\kappa_0$ es incontable, y que la cofinalidad de $\kappa_1$ Es mas grande que $\kappa_0$.
(iii) Un esquema de axioma, diciendo que para cada fórmula $\phi$ de la teoría de conjuntos, $\phi\leftrightarrow \phi^{V_{\kappa_0}}$ y $\phi\leftrightarrow \phi^{V_{\kappa_1}}$.
Luego, el principio de reflexión se puede usar para mostrar (consulte la respuesta de Rodrigo Freire a continuación para ver un bosquejo de la prueba):
Teorema. Este sistema de axiomas es conservador sobre ZFC. En otras palabras, cualquier teorema en este sistema formal que no se refiera a$\kappa_0$ y $\kappa_1$ también es un teorema de ZFC.
Esta es precisamente la conclusión que me gustaría llegar.
Tenga en cuenta que $V_{\kappa_0}$ y $V_{\kappa_1}$ son modelos de ZFC, pero (¡críticamente!) esto no se puede probar dentro del sistema formal, ya que ZFC no es finitamente axiomatizable, y solo cada axioma individual de ZFC es postulado por (iii).
Una cosa buena de este sistema de axiomas es que permite explícitamente los argumentos ocasionales de la forma "probamos este teorema para categorías pequeñas, pero luego también podemos aplicarlo a categorías grandes".
Entonces, una pregunta más precisa es:
¿Funcionan los argumentos de HTT en este sistema formal?
Mike Shulman en la Sección 11 de https://arxiv.org/abs/0810.1279da una exposición muy clara de cuál es el problema potencial aquí. Es decir, si tiene un conjunto$I\in V_{\kappa_0}$ y conjuntos $S_i\in V_{\kappa_0}$ por $i\in I$, no se le permite concluir que la unión del $S_i$ es en $V_{\kappa_0}$. Esta conclusión solo está garantizada si la función$i\mapsto S_i$ también se define en $V_{\kappa_0}$ (o si $I$es contable, por el supuesto adicional de cofinalidad incontable). En la práctica, esto significa que cuando uno quiere afirmar que algo es "pequeño" (es decir, en$V_{\kappa_0}$), este juicio se refiere no sólo a los objetos, sino también a los morfismos, etc. Ahora no me queda claro cuánto problema es esto en realidad, tendría que pensar más en ello; De hecho, podría imaginar que es bastante fácil leer HTT para cumplir con este sistema formal. Shulman dice que, con esta salvedad, se puede demostrar el teorema del functor adjunto y, como dice Lurie en sus respuestas, los argumentos en HTT tienen una complejidad similar en la teoría de conjuntos. Sin embargo, todavía me interesaría juzgar si la respuesta a la pregunta es "Sí, como está escrito" o más bien "Probablemente sí, pero tienes que esforzarte un poco" o, de hecho, "No realmente". (Espero sinceramente que los expertos puedan ponerse de acuerdo aproximadamente sobre dónde cae la respuesta en este espectro).
Una observación final: uno puede encontrar la suposición de "incontables" anterior un poco arbitraria; ¿Por qué no permitir algunas uniones un poco más grandes? Una forma de solucionar esto es agregar un símbolo$\kappa_{-1}$ con las mismas propiedades, y pedir en cambio que la cofinalidad de $\kappa_0$ Es mas grande que $\kappa_{-1}$. Del mismo modo, es posible que desee reemplazar el límite$\mathrm{cf} \kappa_1>\kappa_0$ por un límite un poco más fuerte como $\mathrm{cf} \kappa_1>2^{\kappa_0}$decir. Nuevamente, si simplifica las cosas, uno podría simplemente apretar otro$\kappa_{1/2}$ en el medio, para que $\mathrm{cf} \kappa_{1/2}>\kappa_0$ y $\mathrm{cf} \kappa_1>\kappa_{1/2}$. De esta manera uno no tiene que preocuparse si alguno de los objetos "estándar" que aparecen en algunas pruebas permanece de tamaño contable, o si todavía se pueden tomar colimits en$V_{\kappa_1}$ cuando los conjuntos de índices no tienen exactamente el tamaño delimitado por $\kappa_0$ pero han sido manipulados un poco.
PD: Solo ahora estoy encontrando todas las preguntas y respuestas relevantes de MO anteriores. Algunas muy relevantes son las respuestas de Joel Hamkins aquí y aquí .
Respuestas
Voy a arriesgarme y sugerir que el libro HTT nunca use nada más fuerte que el reemplazo de $\Sigma_{15}$-fórmulas de teoría de conjuntos. (Aquí$15$ es un gran número elegido al azar, y HTT es un libro de matemáticas elegido al azar que no trata específicamente de la teoría de conjuntos).
Reflexionando sobre el comentario de Gabe sobre mi respuesta original, ahora creo que lo que escribí es engañoso porque combina dos afirmaciones separadas (pero relacionadas):
La existencia de cardenales fuertemente inaccesibles no es realmente necesaria en la teoría de categorías.
En realidad, no se necesita toda la fuerza de ZFC en la teoría de categorías.
Estoy de acuerdo con estas dos afirmaciones, pero creo que la mejor manera de convencer a alguien de 1) no sería combinar 2) con un principio de reflexión: es decir, no se debe intentar reemplazar el uso de un cardenal fuertemente inaccesible. $\kappa$ por uno para el cual $V_{\kappa}$ modela una gran parte de ZFC.
A mi modo de ver, el "problema" que resuelven los universos es justificar la combinación de dos tipos de razonamiento:
A) A veces es útil probar teoremas sobre categorías pequeñas. $\mathcal{C}$ incrustándolos en categorías "grandes" (por ejemplo, utilizando la incrustación de Yoneda) que tienen características adicionales interesantes: por ejemplo, la existencia de límites y colimits.
B) Las categorías grandes también son categorías, por lo que cualquier teorema que se aplique a las categorías en general también debería aplicarse a las categorías grandes.
Si solo le preocupaba B), entonces un principio de reflexión podría ser relevante. Elegir un cardenal$\kappa$ tal que $V_{\kappa}$ satisface una gran parte de ZFC, puede redefinir "categoría pequeña" para que signifique "categoría que pertenece a $V_{\kappa}$"y" categoría grande "significa" categoría que no pertenece necesariamente a $V_{\kappa}$", y puede estar seguro de que todos los teoremas básicos que desee son válidos en ambos casos.
Pero si también le preocupa A), entonces esto no es necesariamente útil. Digamos que comienzas con una categoría$\mathcal{C}$ perteneciendo a $V_{\kappa}$y desea alguna versión de la incrustación de Yoneda. Una suposición natural sería incrustar en la categoría de functores de$\mathcal{C}^{\mathrm{op}}$ a la categoría de conjuntos de tamaño $<\tau$ (o algún modelo equivalente de la misma), para algunos cardinales $\tau$. Una primera suposición es que deberías tomar$\tau = \kappa$, pero creo que esto solo tiene sentido $\kappa$es muy inaccesible (de lo contrario, algunos conjuntos de Hom serán demasiado grandes). En todo caso garantiza que esta construcción tiene buenas propiedades, vas a querer exigir diferentes propiedades del cardenal.$\tau$. Por ejemplo, si desea que esta categoría de pre-olas tenga muchos colimits, entonces querrá$\tau$tener una gran cofinalidad. Y si empiezas a pensar en qué tipo de suposiciones adicionales podrías necesitar hacer, estás de vuelta donde empezaste: pensando en qué tipo de estimaciones de cardinalidad garantizan que "pre-oleadas de conjuntos de tamaño$< \tau$"son una buena aproximación a la categoría de todas las premoniciones de conjuntos. Por lo tanto, el principio de reflexión no ayuda realmente a evitar esos problemas.
(Editar: después de escribir, me di cuenta de que el texto a continuación reitera principalmente la publicación original de Peter. Pero lo dejaré aquí en caso de que alguien lo encuentre útil).
Si desea una formalización rigurosa en algo como ZFC, probablemente lo mejor que puede hacer es eliminar por completo las categorías grandes. Entonces, B) no es un problema. Para tratar con A), permítanme comentar que muchas de las categorías "grandes" de las que a uno le gustaría hablar surgen de una manera particular: uno comienza con una categoría pequeña$\mathcal{C}$ que ya tiene ciertos tipos de colimits, y agranda formalmente $\mathcal{C}$ para hacer una categoría más grande $\mathcal{C}^{+}$que tiene colimits arbitrarios (sin cambiar los con los que comenzó). Las categorías que surgen de esta manera se denominan presentables localmente , y hay una fórmula simple para$\mathcal{C}^{+}$: es la categoría de functores $F: \mathcal{C}^{\mathrm{op}} \rightarrow \mathrm{Set}$ que conservan los límites con los que comenzaste (es decir, los colimits con los que comenzaste en $\mathcal{C}$).
Ahora bien, si desea imitar esto en el mundo de las categorías pequeñas, puede elegir algún cardinal $\kappa$ y en cambio contemplar functores $F: \mathcal{C}^{\mathrm{op}} \rightarrow \{ \text{Sets of size < $\kappa$} \}$, que equivale a una categoría pequeña $\mathcal{C}^{+}_{\kappa}$. La pregunta que se encuentra es si este es un reemplazo suficientemente bueno para la categoría grande.$\mathcal{C}^{+}$sobre. Por ejemplo, ¿tiene muchos límites y colimits? No es razonable pedir que tenga todos los colimits, pero podría preguntar lo siguiente:
P) ¿La categoría $\mathcal{C}^{+}_{\kappa}$ tienen colimits indexados por diagramas de tamaño $< \kappa$?
La respuesta a la pregunta es "no en general, pero sí si $\kappa$ está muy bien elegido ". Por ejemplo, si tiene un infinito cardinal $\lambda$ delimitando el tamaño de $\mathcal{C}$ y la cantidad de diagramas de colimit con los que comienzas, entonces creo que puedes garantizar (i) tomando $\kappa = (2^{\lambda})^{+}$ (y la categoría $\mathcal{C}^{+}_{\kappa}$puede caracterizarse por la propiedad universal esperada). Además, para probar esto, no necesita ningún tipo de reemplazo.
Ahora también puedes preguntar lo siguiente:
Q ') ¿La categoría $\mathcal{C}^{+}_{\kappa}$ tienen límites indexados por diagramas de tamaño $< \kappa$?
Aquí la respuesta suele ser "no" a menos que $\kappa$es muy inaccesible. Pero si solo le interesan los límites de un tipo en particular (por ejemplo, si está estudiando los topoi de Grothendieck, es posible que le interesen especialmente los límites finitos), la respuesta será nuevamente "sí para$\kappa$ bien elegido ". Y esto es algo que puede probar con muy poco de ZFC.
Ahora bien, mi afirmación es que, según mi experiencia, la discusión anterior es representativa del tipo de preguntas con las que se encontrará al tratar de navegar por la distinción entre categorías "pequeñas" y "grandes" (sin duda, es representativa de la forma en que estas cosas aparecen en mi libro, sobre el que se hacía la pregunta original). En la práctica, nunca es necesario hablar sobre la totalidad de una categoría grande como$\mathcal{C}^{+}$; es suficiente para construir una pieza lo suficientemente grande (como$\mathcal{C}^{+}_{\kappa}$) con las funciones que desea ver, que puede organizar eligiendo $\kappa$ con cuidado.
Me parece conceptualmente más claro ignorar la cuestión de cómo se formalizan las cosas en ZFC y expresar las cosas en términos de la categoría "grande". $\mathcal{C}^{+}$, refiriéndose a sus "pequeñas" aproximaciones $\mathcal{C}^{+}_{\kappa}$sólo como auxiliares en una prueba (¡que inevitablemente seguirá apareciendo en alguna parte!). La invocación de "universos" es solo una forma de escribir así sin dejar de prestar atención al marco axiomático de ZFC, y definitivamente no es esencial.
Me gustaría mencionar algo que creo que aún no se ha señalado. La pregunta original comenzaba con
En el lenguaje de la teora de conjuntos, uno corrige algunos aspectos cardinales fuertemente inaccesibles $\kappa$... Esto implica que el escenario $𝑉_\kappa\subset 𝑉$ de "conjuntos de tamaño $<\kappa$"es en sí mismo un modelo de ZFC.
Sin embargo, la afirmación de que $V_\kappa$ es un modelo de ZFC es significativamente más débil que decir que $\kappa$es inaccesible. De hecho, si$\kappa$ es inaccesible, entonces $\{ \lambda\mid V_\lambda$ es un modelo de ZFC $\}$ está parado en $\kappa$. Por lo tanto, el más pequeño inaccesible (si lo hay) es mucho más grande que el más pequeño.$\kappa$ tal que $V_\kappa$ modelos ZFC.
En la medida en que el principio de reflexión es útil (que, como han señalado algunas otras respuestas, al menos uno puede cuestionar), solo es directamente útil para argumentos en los que la propiedad relevante de un universo de Grothendieck es que es un modelo de ZFC. Sin embargo, al menos cuando se formula ingenuamente, hay muchos lugares donde la teoría de categorías usa más que esto. Específicamente, usamos el hecho de que un universo de Grothendieck satisface el reemplazo de segundo orden , lo que significa que cualquier función$f:A\to V_\kappa$, dónde $A \in V_\kappa$, tiene una imagen. Diciendo que$V_\kappa$modelos ZFC solo implica que satisface el reemplazo de primer orden , lo que solo nos permite concluir que tal$f$ tiene una imagen si $f$ es definible a partir de $V_\kappa$ por una fórmula lógica.
Creo que el reemplazo de segundo orden es omnipresente en la teoría de categorías basada en el universo, tal como se formula habitualmente. Por ejemplo, si${\rm Set}_\kappa$ denota la categoría de conjuntos en $V_\kappa$, luego para demostrar que ${\rm Set}_\kappa$ es "completo y cocompleto" en el sentido ingenuo de que admite un límite y un colimit para cualquier funtor cuyo dominio sea pequeño, necesitamos un reemplazo de segundo orden para recopilar las imágenes de dicho funtor en un solo conjunto.
Ahora bien, hay formas de reformular la teoría de categorías para evitar esto. El artículo de McLarty lo hace de alguna manera basada en la teoría de conjuntos. Un enfoque categóricamente consistente es reemplazar las "categorías grandes" ingenuas (es decir, categorías cuyos conjuntos de objetos y morfismos pueden no pertenecer a$V_\kappa$) con gran ${\rm Set}_\kappa$- categorías indexadas . Pero este es un tipo de reformulación mucho más sustancial para realizar a mano.
Si lo he entendido correctamente, lo que busca es una declaración del formulario:
"Si algo se probó en HTT usando universos, se puede probar sin ellos restringiendo a algunos $V_\kappa$ por $\kappa$ lo suficientemente grande"
La respuesta rigurosa a eso, si no tenemos más información sobre HTT, es que no puede haber tal declaración si ZFC es consistente.
De hecho, es posible que la existencia de universos sea inconsistente (de hecho, no es posible probar que sea consistente), y en esa situación, cualquier cosa puede probarse usando universos, por lo que tal declaración implicaría que cualquier cosa puede probarse. , es decir, ZFC es inconsistente.
Estoy siendo un poco descuidado acerca de lo que se puede demostrar en qué, etc., pero la idea principal está ahí.
Por supuesto, sabemos cosas sobre HTT, y si lo leemos detenidamente podemos analizar dónde usa universos y ver que, de hecho, pueden ser reemplazados con modelos transitivos de reemplazo de ZC + hasta $\Sigma_{15}$-fórmulas, como señala Jacob. En ese caso, dado que es probable que existan modelos tan bien comportados (de la forma$V_\kappa$, por $\kappa$bien elegido), esto no es un problema; y HTT se puede reescribir sin universos, pero esto no se puede probar sin conocer lo que hay en HTT.
La "moraleja" de esto es que, en la mayoría de las preguntas teóricas de las categorías principales, los universos son un dispositivo que ahorra tiempo y no una parte real de las matemáticas.
Cualquier teorema $T$ de $\mathsf{ZFC}$ se sigue de un subconjunto finito de los axiomas de $\mathsf{ZFC}$ o, para simplificar las cosas, desde $\mathsf{ZFC}$ donde el esquema de axioma de reemplazo se restringe a $\Sigma_n$ predicados¹, llama a esto $\mathsf{ZFC}_n$. Ahora$\mathsf{ZFC}$, y más precisamente $\mathsf{ZFC}_{n+1}$, prueba la existencia de cardenales arbitrariamente grandes $\kappa$, fuertes límites de incontable cofinalidad, de modo que $V_\kappa$ es un modelo de $\mathsf{ZFC}_n$, y, en particular, del teorema $T$, y tal que, además, el valor de verdad de cualquier $\Sigma_n$ declaración, con parámetros en $V_\kappa$ es lo mismo en $V_\kappa$como en el (verdadero) universo. Podemos llamar a estos$V_\kappa$ "Universos limitados" en el sentido de que están cerrados en la mayoría de las operaciones de teoría de conjuntos, como tomar conjuntos de potencia, excepto que el reemplazo debe ser contable (incluido por conveniencia) o restringido a un $\Sigma_n$predicado; y en particular, están cerrados bajo cualquier declaración de existencia$T$ hace.
Entonces la idea sería aplicar lo anterior a la conjunción $T$ de todos los teoremas que usted considera que forman parte de la Teoría del Topos Superior (y cualquier otra teoría que se utilice como prerrequisitos) y encuentre la $n$. (De hecho sospecho que$n=1$ debería ser suficiente: me sorprendería mucho encontrar un ejemplo de reemplazo en las matemáticas ordinarias que no se siga de $\Sigma_1$-remplazo.) Entonces $\mathsf{ZFC}_n$ probaría $T$ (todos los teoremas de la teoría) y $\mathsf{ZFC}_{n+1}$ probaría la existencia de un suministro interminable de universos limitados en los que utilizar la teoría.
Por supuesto, para evitar un bucle infinito, no se puede considerar ese teorema (el que afirma la existencia de un suministro interminable de$V_\kappa$) para ser parte de la teoría, o necesita pasar a una $n$.
Para explicar lo que podría parecer una contradicción lógica, aquí hay que aclarar que la afirmación de que la existencia de muchos modelos de $\mathsf{ZFC}_n$ puede ser probado en $\mathsf{ZFC}$ para cada $n$, pero no de manera uniforme (la prueba se hace más y más larga a medida que $n$ crece), entonces $n$debe ser un nmero natural concreto , el universalmente cuantificado (sobre $n$) declaración no es demostrable en$\mathsf{ZFC}$. Pero esto no es un problema siempre que su teoría sea fija y esté formulada en$\mathsf{ZFC}$ (que exige que no contenga, en sí mismo, metateoremas como "para cualquier $n$ podemos probar lo siguiente en $\mathsf{ZFC}$”). Por lo tanto, depende de usted asegurarse de que este es el caso de HTT (y, si es lo suficientemente valiente, encontrar el$n$).
(Solo para dar una idea de cómo los tipos de cardenales involucrados, los cardenales $\kappa$ tal que $V_\kappa$ es un modelo de $\mathsf{ZFC}_1$ son los puntos fijos de la $\gamma \mapsto \beth_\gamma$función. No creo que haya esperanzas de una descripción razonable de la$\kappa$ tal que $V_\kappa$ es un modelo de $\mathsf{ZFC}_n$ para cualquier hormigón $n\geq 2$. Consulte también esta pregunta .)
- Significado de predicados con como máximo $n$ conjuntos alternos de cuantificadores ilimitados, comenzando con cuantificadores existenciales, seguidos de una fórmula con cuantificadores limitados (significado de la forma $\forall x\in y$ o $\exists x\in y$).
De acuerdo, pasé gran parte del día tratando de resolver esto mirando con cierto detalle a HTT. Ha sido todo un viaje; Definitivamente he cambiado mi perspectiva varias veces en el proceso. Actualmente, me parece que la respuesta es que HTT, tal como está escrito, se puede leer en este sistema formal. (Así que esto es como en el chiste donde después de horas alguien dice "Sí, es obvio". Definitivamente hay puntos en los que se debe elegir la interpretación correcta, pero como en cualquier texto matemático, ese ya es el caso de todos modos). Con esta respuesta quiero adelantar un argumento de que HTT se puede leer en este sistema formal, tratando de explicar un poco cómo interpretar ciertas cosas en caso de que pueda surgir ambigüedad, y por qué creo que al leerlo así todo debería funcionar. Pero es bastante probable que haya pasado por alto algo importante, ¡así que corrígeme!
Como señala Tim Campion, la mayoría de las cosas iniciales funcionan sin problemas; de hecho, ni siquiera menciona los universos. Mientras no sea así, todo funciona en$V_{\kappa_0}$, en $V_{\kappa_1}$, y en $V$, y el esquema de axioma dado incluso garantiza que cualquier construcción realizada será compatible.
Hay que prestar más atención cuando se llega a los capítulos 5 y 6. Permítanme intentar presentar algunas definiciones y proposiciones de estos capítulos desde tres puntos de vista diferentes.
El punto de vista clásico de la ZFC, o (de manera equiconsistentemente) el de la teoría de von Neumann - Bernays - Gödel (NBG), que permite clases además de conjuntos, por lo que podemos hablar de la categoría (tamaño de clase) de todos los conjuntos. $\mathrm{Set}$.
El punto de vista de HTT, que son los universos ZFC + Grothendieck.
El punto de vista de la teoría de conjuntos de Feferman, en la forma planteada en la pregunta. (En realidad, ya no estoy seguro de si realmente necesito estos límites de cofinalidad. Pero es bueno saber que se pueden asumir).
Nótese que la pregunta formulada presupone que uno está realmente interesado en el primer punto de vista, y en los otros sólo en la medida en que sean convenientes para demostrar algo sobre el primer escenario. Esto se alinea con el contenido de los capítulos 5 y 6: toda la teoría de las categorías presentables encaja muy bien en el primer escenario, también filosóficamente.
Bien, recuerde que una categoría presentable, permítanme limitarme a categorías en lugar de $\infty$-categorías, la diferencia no es esencial para nuestras preocupaciones - es una categoría (del tamaño de una clase) $C$ que admite todos los colimits pequeños, y tal que para algún cardenal regular $\kappa$, hay una pequeña categoría $C_0$ y una equivalencia $C\cong \mathrm{Ind}_{\kappa}(C_0)$,
es decir $C$ se obtiene colindando libremente $\kappa$-colimits filtrados a $C_0$. (En particular,$C_0$ es necesariamente equivalente a la subcategoría completa de $\kappa$-objetos compactos de $C$.) En particular, las categorías presentables están determinadas por una pequeña cantidad de datos. Además, la idea es que$C$es realmente la categoría de todos los objetos (conjuntos, grupos, lo que sea). Este punto de vista se articula realmente más claramente en 1), mientras que en 2) y 3) la noción de presentabilidad de repente depende de nuevo del universo, y de repente, de nuevo, solo contienen pequeños conjuntos / grupos / ...; permítanme entonces, en consecuencia, llamarlos pequeños presentables. Tenga en cuenta que esta noción tiene sentido tanto en 2) como en 3), y depende solo de$V_{\kappa_0}$. Una categoría pequeña-presentable es entonces, en particular, pequeña-definible, por lo que vive en$\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$, donde esta inclusión es una igualdad en 2) (pero no en 3)).
En 2), normalmente se definiría una categoría presentable pequeño como un tipo especial de categoría grande, que es el enfoque de HTT. Pero aquí ya me estoy confundiendo un poco: parece que hay dos nociones de functores$F: C\to D$: Los definibles en $V_{\kappa_0}$, equivalentemente $F\in V_{\kappa_0+1}$ (a saber, $V_{\kappa_0+1}$ son exactamente las clases de $V_{\kappa_0}$), o todos los functors en $V_{\kappa_1}$. No me parece obvio que cualquier functor$F: C\to D$ en $V_{\kappa_1}$ yace en $V_{\kappa_0+1}$, como $C$ y $D$ ellos mismos solo viven en $V_{\kappa_0+1}$. La diferencia entre estas dos nociones desaparece cuando se restringe a los functores accesibles, todos los cuales son definibles. ¡Tenga en cuenta que 1) dice que es realmente la primera noción que debería importarnos! (Antes de escribir esta publicación, no sabía la diferencia).
En 3), la forma correcta de proceder es utilizar la perspectiva dictada por 1), que es la de "$V_{\kappa_0}$-categorías definibles ", por lo que viven en $\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$. Uno puede volver a considerar estos como$\kappa_1$-pequeñas categorías. Al principio pensé que aquí habría una diferencia sustancial entre los enfoques de 2) y 3), pero en realidad parece que en ambos casos se llega a dos nociones diferentes de functores, que se concilian una vez que se restringe a functores accesibles.
Uno de los teoremas principales es el teorema del functor adjunto: Si $F: C\to D$es un functor de categorías presentables que conserva todos los colimits pequeños, luego admite un adjunto derecho. ¿Qué significa realmente este teorema?
En 1), significa que hay un functor $G: D\to C$ - lo que en particular significa que debe ser definible mediante fórmulas, ya que esto es lo que son los functores entre categorías de tamaño de clase - junto con (¡definibles!) transformaciones de unidades y contadores que satisfacen las condiciones habituales.
En 2), se trata simplemente de $C$ y $D$ como pequeño cuando se considera en $V_{\kappa_1}$y luego afirma la existencia del adjunto derecho allí. Sin más información, esto en realidad no parece dar lo que queríamos en 1), a priori$G$(y las transformaciones de unidades y contadores) se encuentran en el universo más grande. Pero esta información se puede obtener recordando que$G$ es realmente accesible (una parte del teorema del functor adjunto que omití indicar anteriormente, pero debería incluirse), por lo que todo se determina en un conjunto.
En 3), a uno le gustaría llegar nuevamente al resultado de 1), pero puede intentar hacer esto como en 2) probando primero la existencia de tales datos en $V_{\kappa_1}$ y luego probar la accesibilidad, lo que da como resultado que todo esté en $\mathrm{Def}(V_{\kappa_0})$.
Veamos cómo se desarrolla esto en un par de lugares tempranos en el Capítulo 5 donde se usan universos.
Definición 5.1.6.2: Sea $C$ser una categoría que admita todos los colimits pequeños. Un objeto$X\in C$es completamente compacto si el funtor$j_X: C\to \widehat{\mathrm{Set}}$ copresentado por $X$ conserva pequeños colimits.
Aquí $\widehat{\mathrm{Set}}$ es la categoría (muy grande) de conjuntos en $V_{\kappa_1}$. Interpretemos lo que significa esta definición en los sistemas anteriores.
Aquí $C$es cualquier categoría (posiblemente del tamaño de una clase). Tenga en cuenta que, especialmente en HTT, "localmente pequeño" no es una hipótesis estándar, por lo que esto permite que incluso los morfismos entre dos objetos sean conjuntos adecuados. Por esta razón, el functor realmente tiene que ir a$\widehat{\mathrm{Set}}$, y esto es algo de lo que no podemos hablar en este entorno. Por tanto, habría que reformular la condición para responder a esta objeción; esto no debería ser difícil, pero puede ser un poco desagradable.
Creo que está implícito en la definición que $C$ es cualquier categoría que se encuentre en $V_{\kappa_1}$. Esto captura estrictamente la configuración de 1) en el sentido de que si$C$ es pequeño-definible como proveniente de 1), entonces cualquier pequeño diagrama colimit en $C$ es automáticamente de pequeña definición.
Aquí tenemos dos opciones: la de 1) o la de 2), y dan nociones diferentes. En caso de conflicto, la perspectiva de 1) es la correcta, por lo que$C$es pequeño-definible, y se pide la conmutación con colimits de diagramas pequeños-definibles. Pero mientras que en 1) tuvimos problemas para formular la condición, los universos en cuestión en 3) significan que la condición ahora se puede formular: podemos pedir que se requieran pequeños colimits definibles en$C$ a colimits en $\widehat{\mathrm{Set}}$. Aquí$\widehat{\mathrm{Set}}$ son los sets en $V_{\kappa_1}$.
Entonces, en este caso, el resultado es que uno tiene que ser un poco cuidadoso en 3) con la interpretación, pero guiado por 1) uno puede dar la definición correcta; y luego el sistema realmente ayuda.
Proposición 5.2.6.2: Sea $C$ y $D$ser categorías. Entonces las categorias$\mathrm{Fun}^L(C,D)$ de functores adjuntos izquierdos de $C$ a $D$, y $\mathrm{Fun}^R(D,C)$ de functores adjuntos correctos de $D$ a $C$ son (canónicamente) equivalentes entre sí.
En esta perspectiva, esta proposición sólo tiene sentido cuando $C$ y $D$ son pequeños, como de lo contrario $\mathrm{Fun}(C,D)$Es demasiado largo. (Uno quiere considerar tales categorías de functores cuando$C$ y $D$son presentables (o accesibles), pero solo cuando se restringen a funciones accesibles. Así que esa es una discusión que aparecerá más adelante en el Capítulo 5.) Entonces la declaración es lo suficientemente clara y la prueba dada se aplica.
En esta perspectiva, creo que es lo mismo que en 1), excepto que también se puede formular el mismo resultado en un universo diferente.
Aquí igual.
Sin embargo, tenga en cuenta que, tal como está, en 1) esta proposición no puede (todavía) aplicarse en caso de $C$ y $D$son presentables. En 2) y 3), los (pequeños) presentables son categorías grandes especiales, a las que se aplica el resultado. Sin embargo, tenga en cuenta que las categorías de functor y su equivalencia viven en un universo más grande, y no obtenemos información de que se encuentren en$V_{\kappa_0+1}$ o $\mathrm{Def}(V_{\kappa_0})$.
La siguiente proposición considera la categoría de la gavilla $\mathcal P(C)=\mathrm{Fun}(C^{\mathrm{op}},\mathrm{Set})$, y la prueba es un argumento típico que implica el paso a un universo más grande para resolver problemas de coherencia de homotopía.
Proposición 5.2.6.3: Sea $f: C\to C'$ ser un functor entre categorías pequeñas y dejar $G: \mathcal P(C')\to \mathcal P(C)$ ser el functor inducido de las categorías de la gavilla inducida por la composición con $f$. Luego$G$ es adyacente a $\mathcal P(f)$.
Aquí $\mathcal P(f)$ se define como la pequeña extensión única que conserva el colimito de $f$ (debajo de la incrustación de Yoneda).
Aquí, tenemos dos categorías y functores del tamaño de una clase entre ellos, todos definibles (como debe ser). La proposición nos pediría que encontráramos (¡definibles!) Transformaciones de unidades y contadores, haciendo que algunos diagramas se conmuten. Esto no parece demasiado difícil. Pero en$\infty$-categorías, es famoso por definir los functores a mano, ¡así que no es así como procede Lurie!
Aquí $\mathcal P(C)$ y $\mathcal P(C')$son categorías grandes especiales. De hecho, Lurie aplica la gran incrustación de Yoneda en la prueba. Así que esto realmente está produciendo las adjunciones de unidad y cuenta solo en un universo más grande. Como se discutió anteriormente, creo que esta prueba en realidad no da lo que queríamos en 1).
Podemos argumentar como lo hace Lurie para producir los datos en un "universo" más grande. (Editar: en realidad, como señala Tim Campion, uno tiene que hacer un desvío mínimo para justificar lo que está escrito. Vea los comentarios a su respuesta).
Entonces, al leer esta proposición, ya sea en el sistema 2) o 3), uno debe hacer un marcador mental de que hasta ahora la declaración probada es más débil de lo que uno podría esperar ingenuamente. Pero esto se corrige más tarde, al observar que todo está determinado por una pequeña cantidad de datos.
Resultado: si bien al principio pensé que habría una diferencia sustancial entre 2) y 3), en realidad creo que (casi) no hay ninguna. Una diferencia es que$\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$ es una inclusión adecuada, pero en la práctica la forma de garantizar la contención en $V_{\kappa_0+1}$ parece probar la definibilidad en $V_{\kappa_0}$ (por ejemplo, demostrando que ciertos functores son accesibles).
¡Bien, ahora dime por qué esto no funciona! :-)
Responder a esta pregunta depende en gran medida de exactamente lo que desee de la Teoría del Topos Superior, porque expresar una alta fuerza lógica es un objetivo diferente de expresar un marco lógico adecuadamente unificado para la geometría algebraica y la teoría de números. Los fundamentos sólidos unificados para las matemáticas categóricas generales son un buen objetivo, y parecen ser el objetivo de muchos contribuyentes aquí. Para ese objetivo es relevante todo lo dicho en los comentarios y respuestas a esta pregunta. Pero un trabajo adecuado en geometría y teoría de números no requiere una gran fuerza lógica.
Si bien HTT está más entrelazado con universos que SGA, ni HTT ni SGA hacen un uso real del esquema de axioma (muy fuerte) de reemplazo. Por tanto, pueden utilizar "universos" radicalmente más débiles que el de Grothendieck. Como ejemplo típico y pertinente, Grothendieck hizo solo una apelación al esquema de axioma de reemplazo. Esa es su prueba crucial de que cada categoría AB5 con un grupo electrógeno tiene suficientes inyecciones. Y este uso de reemplazo resulta eliminable. Funcionó, pero Grothendieck en realidad no lo necesitaba para obtener su resultado.
Para ampliar el uso de reemplazo de Grothendieck: Reinhold Baer en la década de 1940 usó inducción transfinita (que requiere el esquema de axioma de reemplazo) para demostrar que los módulos (sobre cualquier anillo dado) tienen suficientes inyectores. Estaba explorando conscientemente nuevas técnicas de prueba y obtuvo un buen resultado. El Tohoku de Grothendieck emitió esa prueba en una forma que muestra que cada categoría AB5 con un pequeño conjunto de generadores tiene suficientes inyectores, y unos años más tarde Grothendieck descubrió que este era exactamente el teorema que necesitaba para la cohomología topos. Baer y Grothendieck tenían objetivos prácticos, no vinculados a las preocupaciones de las fundaciones, pero ambos también querían que las fundaciones fueran las correctas. Y lo hicieron. Pero resulta que podrían haber obtenido esos mismos teoremas, correctamente, sin reemplazo, por casi las mismas demostraciones, especificando conjuntos de funciones lo suficientemente grandes para empezar (usando el conjunto de potencias, pero no el reemplazo). Hay resultados que realmente requieren el esquema de axioma de reemplazo. Pero esos resultados rara vez ocurren fuera de la investigación fundamental.
Mucha gente que viene de ángulos muy diferentes (algunos lógicos, algunos que no les gusta la lógica) desde la década de 1960 han comentado que en el contexto de la geometría algebraica y la teoría de números, la alta fuerza lógica del axioma del universo de Grothendieck es un subproducto realmente no utilizado de El deseo de Grothendieck de un marco unificado para la cohomología. Eso ahora puede ser bastante preciso: todo el aparato de Grothendieck, que incluye no solo la cohomología de functores derivados de topos, sino la categoría 2 de topos, y las categorías derivadas, se puede formalizar casi exactamente de la misma manera que lo formalizó Grothendieck, pero en fuerza lógica muy por debajo de Zermelo-Fraenkel o incluso de la teoría de conjuntos de Zermelo. Lo mismo ocurre con HTT. Puede obtenerlo sin universos inaccesibles o reflejos siempre que no necesite la enorme (y rara vez utilizada) fuerza de reemplazo. En realidad, no se han dado pruebas para HTT. Ha sido por los usos que hace Grothendieck de los universos . Parece claro que lo mismo funcionará para HTT.
La fuerza lógica necesaria se ha expresado de diferentes formas: Teoría de tipos simples (con aritmética), Aritmética de órdenes finitos, Teoría elemental de la categoría de conjuntos, Teoría de conjuntos de Zermelo del cuantificador acotado. En pocas palabras, postula un conjunto de números naturales y postula que cada conjunto tiene un conjunto de potencias, pero no postula una iteración ilimitada de conjuntos de potencia. Una teoría de universos bastante ingenua puede ser conservadora sobre cualquiera de estos (la forma en que la teoría de conjuntos de Godel-Bernays es conservadora sobre ZFC) y adecuada para todo el gran aparato de estructura de la escuela de Grothendieck.
Consideraría una extensión conservadora de ZFC obtenida de ZFC por la adición de una constante $\alpha$ y los siguientes axiomas:
$\alpha$ es un ordinal$Ord(\alpha)$).
La frase $\phi\leftrightarrow\phi^{V_\alpha}$, para cada oración en el idioma original $\phi$ (esquema de axioma).
$V_{\alpha}$ se comporta como $V$(para todas las oraciones en el lenguaje de la teoría de conjuntos). Si se necesitan dos (o más) universos, uno puede agregar otra constante$\beta$ con los axiomas correspondientes, y el axioma $\alpha<\beta$.
La prueba de que la teoría resultante es conservadora sobre ZFC es fácil.
Asumir que $\phi$ es demostrable a partir de los nuevos axiomas (axiomas que utilizan $\alpha$), en el cual $\phi$está en el idioma original. Dado que cualquier prueba es finita, hay un número finito de oraciones$\phi_1$, ..., $\phi_n$ tal que
$Ord(\alpha)\wedge(\phi_1\leftrightarrow\phi_1^{V_{\alpha}})\wedge...\wedge(\phi_n\leftrightarrow\phi_n^{V_{\alpha}})\rightarrow \phi$
es demostrable sin nuevos axiomas. Por lo tanto, uno puede pensar en$\alpha$como una variable libre y la oración anterior se puede demostrar en ZFC (teorema de constantes). Desde$\alpha$ no ocurre en $\phi$, la siguiente implicación es demostrable en ZFC ($\exists$-Introducción):
$\exists\alpha(Ord(\alpha)\wedge(\phi_1\leftrightarrow\phi_1^{V_{\alpha}})\wedge...\wedge(\phi_n\leftrightarrow\phi_n^{V_{\alpha}}))\rightarrow \phi$
Ahora, el principio de reflexión para ZFC dice que el antecedente es un teorema de ZFC. De modus ponens, ZFC demuestra$\phi$.
Para que pueda trabajar con los nuevos axiomas y $V_{\alpha}$ se comporta como un universo, y todo lo que se prueba que no menciona $\alpha$ ya se puede probar en ZFC.
Una pregunta que surgió en los comentarios fue sobre la motivación para hacer la pregunta. Permítanme tratar de abordar esto aquí.
¡Ante todo, se trata de aprender! Como mencioné en la pregunta original, yo mismo había jugado con algunos límites cardinales "estúpidos", y solo más tarde aprendí sobre el principio de reflexión, así que quería entender qué puede hacer (y qué no puede hacer), y si puedo de alguna manera puede relegar automáticamente a esta máquina cualquier versión más complicada de tales estimaciones. Así que es lo habitual cuando estás dando tumbos en una habitación oscura y te gustaría mucho que la habitación estuviera iluminada. ¡Así que gracias a todos por las esclarecedoras respuestas!
Otra razón es que recientemente me sentí un poco frustrado con la solución de los universos de Grothendieck al problema en cuestión. Dejame explicar.
Tengo muchas ganas de hablar sobre la categoría de todos los conjuntos, o todos los grupos, etc., y quiero probar teoremas al respecto. Y, al menos en la versión von Neumann-Bernays-Gödel (NBG) de la teoría ZFC que permite clases, esta es una noción perfectamente válida. Así que me parece ontológicamente muy agradable trabajar en este escenario, y me gustaría mucho que el teorema del functor adjunto fuera un teorema sobre categorías (presentables) en ese sentido.
Ahora, las categorías presentables están determinadas por una pequeña cantidad de datos, por lo que siempre se puede trabajar con esta pequeña cantidad de datos y realizar un seguimiento cuidadoso de los tamaños relativos. De hecho, muchas pruebas en HTT realizan un seguimiento explícito de tales tamaños relativos, pero todavía hay algunos puntos en los que es bueno tener primero una "visión más amplia" y mirar estas categorías grandes como si fueran pequeñas.
De hecho, el teorema del functor adjunto trata sobre functores entre categorías grandes, y rápidamente se vuelve desagradable hablar de esto desde dentro de NBG / ZFC. Tenga en cuenta que el enunciado del teorema del functor adjunto tiene perfecto sentido: solo pide que todos los datos del adjunto sean definibles. Pero es un poco desagradable tratar de hablar de estas cosas desde "dentro". Así que definitivamente sería bueno tener algún tipo de metateoría con la que discutir sobre estas grandes categorías y pretender que son pequeñas. La sutil cuestión de la "definibilidad desde dentro" puede estar perdida a priori en esta metateoría, pero considero que esta cuestión de la "definibilidad desde dentro" es central, porque después de todo lo que quería era un teorema sobre todos los conjuntos, así que ' Estoy bien con tener que prestarle un poco de atención y, para quitar el remate, resulta que esta es precisamente la diferencia entre trabajar con los universos de Grothendieck y trabajar con los "universos" de Feferman.
Así que esto es para lo que están los universos de Grothendieck: siempre te dan un universo más grande para cualquier universo en el que estés trabajando actualmente. Encuentro la existencia de los universos de Grothendieck completamente intuitiva, y de hecho, postular su existencia parece completamente a la par con postular un conjunto infinito en primer lugar: solo estás permitiendo recolectar todo lo que ya tienes en una entidad más grande propia.
Pero ahora, de repente, lo que solía pensar en todos los conjuntos se llaman conjuntos pequeños , y también hay muchos conjuntos más grandes. Entonces, incluso si demuestro un teorema de functor adjunto en esta configuración, ya no es un teorema sobre functores entre categorías de todos los conjuntos / grupos / ..., sino solo uno de los functores entre conjuntos pequeños / grupos / ... piénselo, incluso en los universos ZFC + Grothendieck, nunca probará ese teorema que realmente quería, sobre la categoría de todos los conjuntos. (En realidad, hasta hace muy poco, asumí que el teorema del functor adjunto (para$\infty$-categories) es una declaración de ZFC que ha sido probada bajo "ZFC + Universes", pero eso no es del todo correcto: la declaración que ha sido probada solo se puede formular en ZFC + Universes.)
Lo que se ha demostrado es que es consistente que se cumple el teorema del functor adjunto. Es decir, asumiendo la coherencia de los universos ZFC +, ahora produjo un modelo de ZFC, el de conjuntos pequeños en su modelo de universos ZFC +, en el que el teorema es verdadero. Así que ahora podrías trabajar en la teoría "ZFC + el teorema del functor adjunto", en la que el teorema del functor adjunto se puede aplicar a la categoría de todos los conjuntos / grupos / ..., pero eso definitivamente me parece una trampa. ¡Ni siquiera demostró que "ZFC + Universos + el teorema del functor adjunto" es consistente! (Obtendrá eso si comienza con la consistencia de un poco más que ZFC + Universes, pidiendo$\kappa$ tal que $V_\kappa$satisface los universos ZFC +. Una vez más, eso me parece una suposición completamente justa, solo sigue adelante.) Pero ahora puedes ver el peligro de que subas inadvertidamente la escalera de la consistencia a medida que implícitamente comienzas a invocar más y más teoremas probados para conjuntos pequeños también. para todos los conjuntos.
Sería mucho mejor si supiera que, en los universos ZFC + Grothendieck, todo lo que demostró acerca de los conjuntos pequeños es también un teorema sobre la categoría ambiental completa de todos los conjuntos. Esto no es automático, pero puede agregarlo como un esquema de axioma. Mike Shulman en la Sección 12 de Teoría de conjuntos para la teoría de categorías (arXiv: 0810.1279) analiza esta idea (que denota ZMC): la encuentro ontológicamente bastante agradable, también parece tener una axiomatización muy simple (¡incluso más simple que ZFC!), pero
a) este esquema de axioma adicional no es completamente evidente para mí: ¿Por qué todo lo que es cierto en conjuntos pequeños debería ser válido también para todos los conjuntos? (Especialmente si tuvimos algún problema para demostrar el resultado deseado en primer lugar. Además, tenga en cuenta que definitivamente no es válido para ninguna noción de conjuntos pequeños: más bien, el esquema de axioma garantiza que existe alguna noción de conjuntos pequeños para los que este tipo de reflexión se mantiene. Ahora esto me parece un poco dudoso, ya que en primer lugar nunca quise conjuntos pequeños, así que ahora los estoy colocando, y también les pido que sigan reflejando el comportamiento completo de todos los conjuntos. Probablemente bien, pero no evidente para mí.)
b) la fuerza de consistencia de este esquema de axioma es considerablemente mayor: es la misma que la consistencia de un cardenal Mahlo. Esto sigue siendo bajo en comparación con los grandes cardenales, pero es mucho más alto que los meros universos de Grothendieck (que son realmente bajos en la parte inferior de la jerarquía).
Con respecto a a), el hecho de que podamos probar la consistencia del teorema del functor adjunto a partir de la consistencia de los universos de Grothendieck apunta en la dirección correcta, pero esto en sí mismo no garantiza que los dos juntos sean consistentes. Puedo imaginarme que podría convencerme de que el esquema del axioma es razonable, pero ciertamente creo que necesita mucha más justificación que los meros universos de Grothendieck. (Pregunta paralela: ¿Qué tan grandes son los grandes cardenales que uno puede justificar usando la idea de "permitir recopilar todo lo que ya teníamos"? No estoy seguro si esta es una pregunta completamente bien definida ... pero para mí, una El cardinal medible definitivamente no es de ese tipo (pero estoy feliz de quedar corregido), ya que parece postular la aparición de nuevas características combinatorias).
Otra razón por la que recientemente me sentí un poco descontento con los universos de Grothendieck es que, si bien en cierto sentido nos gustaría usarlos para poder ignorar las sutilezas de la teoría de conjuntos, de alguna manera vuelven a morderlo, como ahora debe especificar en en qué universo viven ciertas cosas. A veces, es posible que incluso tenga que especificar varios universos diferentes para diferentes tipos de objetos (piense en gavillas en conjuntos profinitos), y encuentro que rápidamente se pone bastante feo. Preferiría que todos los objetos vivieran juntos en un universo.
Entonces, mientras pensaba en gavillas en juegos profinitos, llegué a encontrar la solución con un solo universo mucho más agradable estética y ontológicamente, y esta solución (juegos condensados) se puede formalizar en ZFC sin problemas.
De acuerdo, afirmo que los universos de Grothendieck no resolvieron realmente el problema que se propusieron resolver, ya que
a) todavía no le permiten probar teoremas sobre la categoría de todos los conjuntos / grupos / ... (excepto como resultado de consistencia, o bajo axiomas cardinales grandes más fuertes)
b) trabajando con ellos, todavía tiene que preocuparse por los problemas de tamaño: su categoría de todos los conjuntos ahora viene estratificada en conjuntos de todo tipo de tamaños diferentes (es decir, en diferentes universos).
Además, también aumentan la resistencia de la consistencia.
Ahora, después de esta maravillosa discusión aquí, creo que la propuesta de Feferman es mucho mejor. Sin embargo, como también comentó Mike Shulman, considero que los axiomas de Feferman no describen ningún mundo ontológicamente correcto, sino que considero los "universos" de la teoría de Feferman simplemente como conveniencias, para hablar de categorías grandes como si fueran pequeñas. En otras palabras, la teoría de Feferman te da exactamente una metateoría en la que argumentar sobre categorías tan grandes desde "afuera". Pero es una teoría que solo usaría para dar una prueba de un teorema de ZFC. En comparación con los universos de Grothendieck, la teoría de Feferman
a) le permite probar teoremas sobre la categoría de todos los conjuntos / grupos / ..., porque incluye explícitamente un esquema de axioma en el que todos los teoremas sobre conjuntos pequeños son también teoremas sobre todos los conjuntos.
b) Por supuesto, dentro de una prueba de un teorema de ZFC que invoca algunos problemas de tamaño no triviales, es muy bienvenido que la teoría le permita hablar sobre varios tamaños. Además, lo hace de una manera en la que aún puede aplicar todos los axiomas de ZFC a cada uno de los "universos", y también se ocupa "detrás de escena" de cómo reescribir todo en términos de límites cardinales (potencialmente extremadamente sutiles). en el propio ZFC. Así que es como un lenguaje de programación de alto nivel para argumentos que involucran estimaciones cardinales difíciles en ZFC.
Además, no aumenta la fuerza de la consistencia y, de hecho, cualquier declaración de ZFC probada en este lenguaje son teoremas de ZFC. (Como recordé anteriormente, también podríamos tener a) + b) con universos de Grothendieck, pero luego alcanzaríamos la consistencia de un cardenal Mahlo).
Entonces, el resultado es que creo que los universos de Feferman resuelven el problema de proporcionar una metateoría para "hablar de categorías grandes como si fueran pequeñas" mucho mejor que los universos de Grothendieck.
Permítanme agregar algunas razones finales para hacer la pregunta. Creo que las técnicas de categorías superiores, como las que se presentan en HTT, son de una importancia fundamental, no solo en la topología algebraica donde se originaron, sino en todas las matemáticas. Ciertamente puedo dar fe de ello en lo que respecta a la teoría de números y la geometría algebraica. Entonces, su centralidad es también una razón importante para analizar su fuerza de consistencia.
Leer HTT no es un asunto trivial, es largo y complicado. Sin embargo, algunos colegas de la teoría de números han dicho que una de las principales razones por las que no podían leer HTT es que usa universos . Es decir, están tan acostumbrados a ZFC (¡y a verificar con sumo cuidado!) Que intentarán eliminar automáticamente cualquier uso de universos en una discusión. Ahora, en SGA, al menos si solo estuviera interesado en aplicaciones para etale cohomology de esquemas razonables, esto era algo que podía hacer a mano; por ejemplo, simplemente agregue algunas suposiciones de contabilización para hacer las cosas pequeñas. Sin embargo, en HTT no veo ninguna forma de que alguien pueda poner límites cardinales mientras lee, los argumentos son demasiado complejos para esto.
Así que ahora espero poder decirles que pueden comprobar que todo funciona en ZFC y que todavía pueden leer HTT (esencialmente) como está escrito, si lo leen en la teoría de conjuntos de Feferman. Si lo comprueban con cuidado (lo que harán), es posible que aún deban completar un pequeño lema aquí y un pequeño argumento adicional allá, pero tendrían que hacerlo de todos modos, en cualquier libro de ~ 1000 páginas, y me imagino que menos de la mitad de estos comentarios secundarios tienen que ver con la sustitución de los universos de Grothendieck por los "universos" de Feferman. Si alguien realmente emprende ese proyecto, ¡por supuesto que merece todo el crédito si tiene éxito en este importante trabajo!
Permítanme terminar con una nota muy breve sobre lo que parece ser el punto clave en la traducción a la teoría de Feferman. Llegué a apreciar el punto que Tim Campion planteó en su respuesta, y ahora veo que esto también se mencionó en la segunda respuesta de Jacob Lurie. Aproximadamente, es lo siguiente. Si$C$ es una categoría presentable, entonces hay una pequeña categoría $C_0$ tal que $C=\mathrm{Ind}_\kappa(C_0)$
para algún cardenal regular $\kappa$, colindando libremente todos los pequeños $\kappa$-colimits filtrados. Esto hace$C$ naturalmente una unión de $C_\tau$donde $C_\tau$ solo recoge el $\tau$-pequeña $\kappa$-colimits filtrados. Aquí$\tau$ es un cardenal regular tal que $\tau\gg \kappa$. Esta creciente estructura de$C$ como una unión de $C_\tau$es central en la teoría de categorías presentables, pero los niveles son realmente enumerados por (ciertos) cardenales regulares $\tau$. Si aumentas tu universo, también obtienes una versión más grande.$C'$ de $C$ sí mismo, y en los universos de Grothendieck $C$ es ahora una de las bonitas capas $C'_\tau$ de $C$, dónde $\tau$es el punto cardinal del universo anterior. Pero en los universos de Feferman, este$\tau$no es regular. Esto puede hacer que algunos argumentos sean más sutiles, pero yo esperaría que uno pueda resolver este problema simplemente incrustando$C$ en algunos $C'_\tau$ con $\tau$ algún cardenal regular más grande que el cardenal de corte del universo más pequeño.
En respuesta a la edición que clava las cosas en un sistema formal que involucra a los cardenales $\kappa_{-1} < \kappa_0 < \kappa_{1/2} < \kappa_1$:
Voy a arriesgarme en una rama quizás menos aconsejable y predecir que para encajar los capítulos 1-4 en este sistema formal, no será necesaria ninguna aritmética cardinal real. Más bien, para esta parte del libro, todo lo que tendrá que hacer es revisar y agregar a varios enunciados de teoremas hipótesis de la forma "$X$ es $\kappa_{-1}$-small ". Después de todo, esta parte del libro realmente solo trata con objetos pequeños, con la excepción de algunos objetos grandes particulares como la categoría de pequeños conjuntos simpliciales, la categoría de pequeñas categorías simpliciales, etc., y cosas como Se construyen varias estructuras modelo, pero creo que en cada caso se puede utilizar el caso especial del argumento del objeto pequeño para generar cofibraciones / cofibraciones acíclicas entre objetos finitamente presentables, de modo que no se necesita inducción transfinita. A primera vista, enderezamiento / desalineamiento tienen el aspecto de construcciones que podrían estar usando la teoría de conjuntos de manera seria, pero voy a seguir adelante y predecir que no presentan problemas para el sistema formal propuesto.
El capítulo 5 se vuelve más molesto. Creo que uno tendrá que tomar algunas decisiones cuidadosas sobre los teoremas centrales de presentable ($\infty$) -categorías. Lo que hace que las categorías presentables funcionen es que empaquetan el teorema del functor adjunto de manera muy limpia, pero como usted dice, el teorema del functor adjunto ordinario viene con salvedades en esta configuración. Podría ir tan lejos como para decir que todo el objetivo de pensar en categorías presentables en primer lugar se deshace por completo en este entorno. No podrá probar cosas básicas como "las categorías presentables son precisamente las localizaciones accesibles de las categorías anteriores a la gavilla". Predigo que, sean cuales sean las elecciones que se tomen sobre la formulación de versiones débiles de los teoremas centrales de las categorías presentables en este escenario, habrá alguna aplicación o aplicación potencial que sufrirá.
Los capítulos 5 y 6 también contienen algunos teoremas sobre categorías particulares muy grandes, como $\infty$-categoría de presentable $\infty$-categorías y el $\infty$-categoría de $\infty$-topoi [1]. El sistema parece ser tal que esto realmente no será un problema per se , excepto que los problemas encontrados en la teoría de presentabilidad básica ahora se agravarán. No podrás probar eso$Pr^L$ es dual para $Pr^R$. No podrá probar el teorema de Giraud (bueno, las definiciones van a estar cambiando de todos modos, así que debo aclarar: no podrá probar que las localizaciones accesibles exactas a la izquierda de las categorías de pregajo son las mismas que localmente pequeñas categorías que satisfacen una lista de condiciones de integridad, generación y exactitud). Entonces, cualquier teorema sobre$\infty$-topoi cuya demostración procede comenzando con el caso anterior a la gavilla y luego localizando tendrá que ser completamente repensado.
Quizás estoy fuera de base aquí, pero creo que se requeriría un trabajo adicional significativo e ideas matemáticas genuinamente nuevas para los Capítulos 5 y 6, y el resultado sería una teoría que es sustancialmente más difícil de usar.
Por el contrario, creo que si está dispuesto a restringir la atención a categorías grandes que se pueden definir a partir de parámetros pequeños, entonces, aunque se perderá la hermosa capacidad de decir "probamos esto para categorías pequeñas, pero ahora podemos aplicarlo a grandes one ", terminará con una teoría de la presentabilidad mucho más útil, sin salir de ZFC.
[1] En realidad, en los fundamentos habituales estas categorías son (hasta la equivalencia) solo grandes y no muy grandes (más precisamente, se han $\kappa_0$-muchos objetos y $\kappa_0$homs de tamaño grande), pero se requiere un mínimo de trabajo para mostrar esto. ¿Seguirá siendo así en este sistema formal? No estoy seguro.
EDIT: Un largo comentario en respuesta a Peter Scholze respuesta .
Una cosa de la que me acabo de dar cuenta es que si$\kappa_0$ no es un $\beth$-punto-fijo, entonces no todos los conjuntos en $V_{\kappa_0}$ tiene cardinalidad $<\kappa_0$, de modo que se multiplican las nociones de "pequeñez". Felizmente, creo que su sistema formal demuestra que$V_{\kappa_0}$ posee $\Sigma_1$-remplazo, lo que implica que es un $\beth$-punto fijo. ¡Crisis evitada!
Quizás este enfoque de utilizar sistemáticamente hipótesis de definibilidad dentro de un "entorno universal" sea viable, combinando "lo mejor de ambos mundos". Una cosa buena es que, aunque esté utilizando explícitamente hipótesis metamatemáticas, parecería que aún podrá enunciar y probar estos teoremas como teoremas únicos en lugar de esquemas.
Estoy un poco confundido acerca de la Proposición 5.2.6.3 (la última que discutes y una versión para bebés del teorema del functor adjunto). Supongo que la categoría antes de la gavilla$P(C)$ se definirá para comprender esos functores $C^{op} \to Spaces$ que se encuentran en $Def(V_{\kappa_0})$. Cuando pasamos a un universo más grande, la transición suele ser bastante fluida, porque esperamos$P(C)$ tener todos los colimits indexados por $\kappa_0$-pequeñas categorías - una propiedad perfectamente natural para trabajar en $V_{\kappa_1}$. De hecho, el primer paso de la prueba de Lurie de 5.2.6.3 es mostrar que existe un adjunto izquierdo usando el hecho de que$P(C)$tiene todos los colimits pequeños [2]. Sin embargo, en el contexto actual nunca podemos suponer que$\kappa_0$ es regular y, por lo tanto, nunca podemos suponer que $P(C)$tiene todos los colimits pequeños. Lo mejor que podemos decir es que$V_{\kappa_0}$ piensa $P(C)$tiene todos los colimits pequeños. Mientras estemos trabajando en$V_{\kappa_0}$, esta propiedad es "tan buena" como tener todos los colimits pequeños. Pero cuando pasamos a$V_{\kappa_1}$, de repente tenemos que pensar en ello por lo que es: una propiedad metamatemática. Quizás más tarde me sentaré y trataré de ver si la prueba de Lurie de 5.2.6.3 puede funcionar en este escenario, pero creo que prima facie no está claro.
[2] Sólo después de verificar la existencia de forma abstracta de esta manera, muestra que el adjunto izquierdo debe ser el funtor indicado. Por supuesto, esta maniobra es en realidad una complicación adicional que viene con el$\infty$-configuración categorial: en categorías ordinarias, las fórmulas para los dos functores pueden verificarse directamente como adjuntas, pero en $\infty$-categorías la fórmula para el adjunto izquierdo no es obviamente funcional.