Estudio de caso: ¿qué se necesita para formular y probar el argumento del objeto pequeño de Quillen en ZFC?
Me estoy perdiendo un poco con la interesante pregunta de Peter Scholze sobre eliminar la dependencia de los universos de los teoremas en la teoría de categorías. En particular, me veo obligado a admitir que realmente no sé cuándo se invoca el reemplazo, no importa cuándo se invoca "de manera esencial". Así que me gustaría trabajar con un ejemplo razonablemente concreto del fenómeno. Entiendo que el reemplazo debería "realmente" considerarse como el axioma que permite la recursividad transfinita. Mi sensación es que la teoría de categorías tiende a no usar la recursividad de manera rigurosa (aunque, más que otras ramas de las matemáticas, tiene muchas definiciones que al menos prima facie tienen una complejidad de Levy no trivial. Por ejemplo, creo que el fórmula$\phi(x,y,z,p,q)$ diciendo que el set $z$ y funciones $p: z \to x$ y $q: z \to y$ son un producto categórico de los conjuntos $x,y$ es sintácticamente $\Pi_1$, y la afirmación de que existen productos binarios en la categoría de conjuntos es sintácticamente $\Pi_3$ (ignorando los cuantificadores acotados, por supuesto)).
El siguiente teorema es, creo, una de las excepciones notables a la categoría-teórico-no-uso-de-recursividad:
Teorema [Quillen] "El argumento del objeto pequeño": Sea$\mathcal C$ ser una categoría presentable localmente, y dejar $I \subseteq Mor \mathcal C$ser un pequeño conjunto de morfismos. Dejar$\mathcal L \subseteq Mor \mathcal C$ ser la clase de retracciones de compuestos transfinitos de cambios de cobase de coproductos de morfismos en $I$, y deja $\mathcal R \subseteq Mor \mathcal C$ comprenden aquellos morfismos débilmente ortogonales a la derecha de los morfismos de $I$. Luego$(\mathcal L, \mathcal R)$es un sistema de factorización débil en$\mathcal C$.
Para la prueba, consulte el nlab . Básicamente, las factorizaciones se construyen mediante recursividad transfinita. La recursividad me parece "esencial" porque se introducen nuevos datos en cada etapa de la construcción.
Formalización:
Creo que este teorema y su demostración son directamente formalizables en MK, donde la distinción "pequeño / grande" teórico de categorías se interpreta como la distinción "conjunto / clase" de MK. No me siento calificado para comentar si la prueba funciona en NBG, pero la declaración al menos tiene sentido directamente.
Cuando se trata de formalizar en ZFC, tenemos opciones que hacer con respecto a la distinción pequeña / grande:
Una opción es introducir un "universo" $V_\kappa$(que, si realmente estamos tratando de trabajar en ZFC, será un tipo de universo más débil de lo habitual). Interpretaremos "pequeño" como "en$V_\kappa$". No consideraremos" objetos verdaderamente grandes "- todo de lo que hablamos será un conjunto - en particular, cada categoría de la que hablamos tendrá el tamaño de un conjunto, incluso si no es" pequeño "per se. interpretar "categoría presentable localmente" en el sentido de "$\kappa$-cocompleto, localmente $\kappa$-categoría pequeña con un fuerte $\kappa$-pequeña, $\lambda$-generador presentable para algunos regulares $\lambda < \kappa$"(No sé si hay alguna diferencia en decir que $V_\kappa$ piensa $\lambda$ es un cardenal regular).
Otra opción es no introducir ningún universo y simplemente interpretar "pequeño" en el sentido de "tamaño de conjunto". En este caso, cualquier objeto "grande" del que hablamos debe ser definible a partir de pequeños parámetros. Así que definimos una categoría para que comprenda una clase de objetos definibles por parámetros, una clase de morfismos definibles por parámetros, etc. Esto puede parecer restrictivo, pero funcionará bien en el caso presentable localmente, ya que podemos definir una categoría presentable localmente$\mathcal C$ por definir, relativo a los parámetros $(\lambda, \mathcal C_\lambda)$ (dónde $\lambda$ es un cardenal regular y $\mathcal C_\lambda$ es una pequeña $\lambda$-categoría cocompleta), como la categoría de $\lambda$-Ind objetos en $\mathcal C_\lambda$.
Ahora, para el teorema que nos ocupa, el enfoque (2) parece más limpio porque la "traducción" necesaria es sencilla, y una vez hecha, la demostración original debería funcionar sin modificaciones. Creo que los principales inconvenientes de (2) vienen de otra parte. Por ejemplo, probablemente será un asunto delicado formular teoremas sobre la categoría de categorías presentables localmente. En general, habrá varios teoremas sobre categorías que tienen formulaciones y demostraciones conceptuales limpias cuando las categorías involucradas son pequeñas, pero que requieren modificaciones técnicas molestas cuando las categorías involucradas son grandes. Es por estas razones que los enfoques más como (1) tienden a ser favorecidos para proyectos de teoría de categorías a gran escala.
Así que supongamos que estamos siguiendo el enfoque (1). La pregunta entonces es:
Pregunta 1: ¿Exactamente qué tipo de universo necesitamos para formular y probar el teorema anterior siguiendo el enfoque (1)?
Pregunta 2: ¿Cuántos universos de este tipo están garantizados por ZFC?
Presumiblemente, la respuesta a la Pregunta 2 será que hay muchos de esos universos, lo suficiente para que podamos hacer cosas como, dada una categoría, pasar a un universo lo suficientemente grande como para hacer que esa categoría sea pequeña e invocar el teorema de ese universo. .
Pregunta 3: ¿Hasta dónde debemos llegar entre las malas hierbas para responder las preguntas 1 y 2?
¿Tenemos que analizar la demostración del Teorema en profundidad? ¿Existe una rúbrica de criterios fácil que nos permita echar un vistazo a la demostración y, para el 99% de los teoremas como este, decir fácilmente que "pasa" sin profundizar demasiado en las cosas? ¿O hay algún metateorema formal al que podamos apelar de modo que incluso una computadora pueda comprobar que todo está bien?
Respuestas
El comentario de Jacob Lurie da una respuesta a la pregunta 1. Es decir, suponiendo que las estimaciones que di en mi comentario son correctas, para formular y demostrar el teorema será suficiente suponer que
- $\kappa$ es regular
y eso
- para cada $\mu < \kappa$, existe $\rho < \kappa$ tal que $\mu \ll \rho$ (significa que $\mu' < \mu, \rho' < \rho \Rightarrow (\rho')^{\mu'} < \rho$).
Quizás esta propiedad de $\kappa$podría verse como una "forma" de reemplazo. Pero realmente, lo que tenemos son dos condiciones en$\kappa$ que son puramente teóricos de conjuntos en lugar de metamatemáticos, de modo que la respuesta a la Pregunta 1 es algo mucho más limpio de lo que había supuesto.
Esto nos permite abordar la Pregunta 2. Presumiblemente, el resultado es que ZFC demuestra que hay muchísimas $\kappa$ satisfaciendo las dos condiciones anteriores.
Cuando se trata de la Pregunta 3, parecería que en este enfoque, de hecho, necesitamos profundizar bastante en la prueba. De hecho, parece que para llevar a cabo este enfoque, debemos agregar algún contenido matemático genuino a la demostración y, de hecho, demostrar una afirmación más sólida. Las preguntas posteriores se vuelven
¿Será posible en general "construir" "la mayoría" de los teoremas de la teoría de categorías de esta manera, o aparecerán otras cuestiones en el curso del proyecto "Teoría de categorías de ZFC-ify"?
Si la respuesta a (1) es "sí" (o si generalmente es "no" y restringimos nuestra atención a los casos en los que es "sí"), entonces "¿cuánto trabajo extra" sería realmente un proyecto de este tipo?
Supongo que la respuesta a (1) es que cuando se trata del uso de la recursividad transfinita en la teoría de categorías, de hecho será típicamente el caso de que el uso del reemplazo pueda eliminarse de una manera similar a esto, pero Lo más importante es que me he perdido el punto: como argumenta Jacob Lurie en respuesta a la pregunta de Peter Scholze, los problemas más espinosos con la teoría de categorías de ZFC-ifying no tienen que ver con la recursividad transfinita, sino con la posibilidad de ir y venir libremente entre "grandes categorías "y" pequeñas categorías "de diversas formas.
Supongo que la respuesta a (2) es que para "la mayoría" de los usos teóricos de categorías de la recursividad transfinita, debería ser bastante sencillo "construirlos" para que encajen en un "universo bebé" con las propiedades anteriores o algo similar, y que con solo un poco de práctica, uno podría desarrollar la capacidad de verificar casi de un vistazo que es posible, aunque todavía teorema por teorema. ¡Pero me encantaría que me demuestren que estoy equivocado y que me muestren un teorema en la teoría de categorías donde este tipo de enfoque falla!
Finalmente, esto deja como una pregunta abierta si existe una forma "más automática" de hacer todo esto, quizás con una conclusión más débil que "nuestro universo no necesita satisfacer ninguna forma de reemplazo".