The Synthetic Sierpinski Cone

Aquí se presenta un resumen técnico detallado del artículo "The Synthetic Sierpi´nski Cone" de Bakke, Sterling, Williams y Ye.

1. Enunciado del Problema

El artículo aborda una tensión fundamental en las matemáticas sintéticas (específicamente dentro de la Teoría de Tipos de Homotopía, o HoTT) respecto a la relación entre las construcciones geométricas y la clasificación lógica de los mapas parciales.

• La Coincidencia Clásica: En la teoría de categorías clásica y la teoría de dominios, el cono de Sierpi´nski ($X_\perp$), construido pegando un punto cerrado universal por debajo de un espacio $X$, es equivalente al clasificador de mapas parciales ($L^\circ(X)$). Este último clasifica los mapas parciales definidos en subespacios abiertos. Esta equivalencia es una piedra angular de la dualidad entre lógica y geometría en estos campos.
• El Obstáculo Sintético: En contextos sintéticos basados en HoTT con un intervalo genérico $I$, afirmar que $X_\perp \simeq L^\circ(X)$ para todos los tipos $X$ conduce a una degeneración de la teoría. Específicamente, si esta equivalencia se cumple universalmente, fuerza al intervalo $I$ a ser "codiscreto" (trivial), colapsando la distinción entre subespacios abiertos y cerrados y volviendo triviales todos los espacios sintéticos.
• La Pregunta Central: ¿Se puede identificar un subuniverso no trivial de tipos donde el cono de Sierpi´nski sí clasifique mapas parciales, y cómo se relaciona esto con las nociones existentes de completitud en la teoría sintética de categorías superiores (específicamente la completitud de Segal)?

2. Metodología

Los autores trabajan dentro de los Fundamentos Univalentes (HoTT) sin asumir axiomas fuertes sobre el intervalo $I$ (como que sea un orden lineal estricto) ni utilizar modalidades globalmente, excepto donde sea necesario para argumentos específicos. Utilizan:

• Retículos Distributivos: Parametrizan su teoría sobre un retículo distributivo acotado $\Sigma$ (que representa el "intervalo" $I$) en lugar de fijar un modelo específico.
• Teoría de Localización: Emplean la teoría de localizaciones reflejas accesibles (siguiendo a Rijke et al.) para definir subuniversos de tipos "completos".
• Ortogonalidad: Definen la completitud mediante la ortogonalidad a clases específicas de mapas (inclusiones de cuernos, conos, etc.).
• Cilindros de Mapeo: Generalizan el cono de Sierpi´nski a cilindros de mapeo abiertos (o cilindros de visualización abiertos) para manejar familias dependientes de tipos.
• Modalidades (Limitadas): Utilizan brevemente una modalidad de "puntos globales" ($\flat$) para analizar la exponenciabilidad de puntos globales sin colapsar la lógica interna.

3. Contribuciones y Definiciones Clave

A. Jerarquía de Completitud

El artículo establece una jerarquía estricta de condiciones de completitud para los tipos, refinando el trabajo de Pugh y Sterling:

1. Completitud de Segal: Ortogonal a la inclusión del cuerno interior $\Lambda^2_1 \hookrightarrow \Delta^2$. Esta es la condición estándar para las $\infty$-categorías sintéticas.
2. Completitud de Segal Basada: Ortogonal a la familia de inclusiones $\{(i=1)_\perp \hookrightarrow I/i \mid i:I\}$. Esta es una condición más fuerte.
3. Completitud de Sierpi´nski Pequeña: Ortogonal a los mapas de comparación "pequeños" $\sigma_{(i=1)}: (i=1)_\perp \to L^\circ(i=1)$.
4. Completitud de Sierpi´nski: Ortogonal a la familia completa de mapas de comparación $\sigma_X: X_\perp \to L^\circ(X)$ para todo $X$.

B. La Equivalencia Principal

Los autores demuestran que la Completitud de Sierpi´nski Pequeña es equivalente a la Completitud de Sierpi´nski.

• Significado: Pugh y Sterling habían demostrado previamente esta equivalencia solo para tipos 0-truncados (conjuntos). Este artículo la extiende a tipos no truncados (grupos superiores/$\infty$-categorías), demostrando que verificar la ortogonalidad contra los mapas "pequeños" es suficiente para garantizar la ortogonalidad contra todos los mapas.

C. Separación de la Completitud de Segal y la Completitud de Segal Basada

El artículo resuelve una conjetura de Ulrik Buchholtz, demostrando que la completitud de Segal no implica la completitud de Segal basada en contextos no triviales.

• Muestran que si cada tipo con completitud de Segal también tuviera completitud de Segal basada, el intervalo $I$ se volvería inicial-quotient (colapsando a un conjunto de dos elementos), lo cual contradice las propiedades de modelos estándar como los espacios simpliciales.
• Esto establece que la condición "Segal basada" es estrictamente más fuerte y necesaria para que el cono de Sierpi´nski funcione como un clasificador de mapas parciales.

D. Cilindros de Mapeo y Clasificadores de Mapas Parciales

Los autores extienden los resultados del cono de Sierpi´nski a los cilindros de mapeo abiertos ($M^\circ_Y(f)$).

• Demuestran que para tipos con completitud de Sierpi´nski, el cilindro de mapeo abierto de una función $f: X \to Y$ es equivalente al clasificador de mapas parciales relativo $L^\circ_Y(f)$.
• Esto proporciona una nueva propiedad universal "derecha" para los cilindros de mapeo dentro del subuniverso de tipos con completitud de Sierpi´nski.

4. Resultados Clave

1. Teorema 64 y Corolario 66: Un tipo es con completitud de Sierpi´nski si y solo si es con completitud de Sierpi´nski pequeña. En consecuencia, los tipos con completitud de Sierpi´nski forman un subuniverso reflejo accesible.
2. Corolario 48/49/50: En modelos estándar (espacios simpliciales, espacios cúbicos de Dedekind), la completitud de Segal basada es estrictamente más fuerte que la completitud de Segal.
3. Teorema 75 y Corolario 77: El subuniverso de tipos con completitud de Sierpi´nski es cerrado bajo la formación de clasificadores de mapas parciales abiertos relativos. Dentro de este subuniverso, el cilindro de mapeo abierto $M^\circ_Y(f)$ clasifica puntos $y:Y$ equipados con elementos parciales abiertos de la fibra $\text{fib}_f(y)$.
4. Exponenciabilidad: El artículo analiza la exponenciabilidad de los puntos globales. Muestra que, aunque las inclusiones de puntos globales son exponenciables en el sentido clásico, no son $L_{Segal}$-exponenciables internamente a menos que el intervalo sea trivial. Esto resalta la distinción entre propiedades internas y externas en las matemáticas sintéticas.

5. Significado y Aplicaciones

• Semántica Denotacional: En la teoría sintética de dominios, la parcialidad se modela a menudo mediante el mónada del clasificador de mapas parciales $L^\circ$. Los resultados aclaran que para definir funciones perezosas (que dependen de si una entrada está definida) por casos, el codominio debe ser con completitud de Sierpi´nski. Esto implica que cualquier dominio sintético que admita tales funciones perezosas debe satisfacer la condición de Segal (transitividad de caminos) y, más fuertemente, la condición de Segal basada.
• Teoría Sintética de Categorías Superiores: El trabajo clarifica la estructura de la cocompletación libre por un objeto inicial. En las $\infty$-categorías sintéticas, el cono de Sierpi´nski $C_\perp$ no es automáticamente una $\infty$-categoría. Sin embargo, dentro del subuniverso reflejo de $\infty$-categorías con completitud de Sierpi´nski, la reflexión $R(C_\perp)$ es equivalente al clasificador de mapas parciales $L^\circ(C)$. Esto proporciona una descripción computacionalmente manejable de la cocompletación libre en estos contextos específicos.
• Unificación de Campos: El artículo unifica con éxito conceptos de topología sintética, teoría de dominios y teoría de categorías superiores. Demuestra que la "coincidencia" entre el cono geométrico de Sierpi´nski y el clasificador lógico de mapas parciales no es una ley universal, sino una propiedad de un subuniverso específico y bien comportado de tipos.
• Mecanización: Los autores señalan que sus resultados principales han sido mecanizados en el asistente de pruebas Agda, asegurando la corrección rigurosa de los argumentos de teoría de tipos.

En resumen, el artículo resuelve una ambigüedad crítica en las matemáticas sintéticas al identificar las condiciones precisas (completitud de Sierpi´nski) bajo las cuales las construcciones geométricas (conos/cilindros) se alinean con la clasificación lógica (mapas parciales), demostrando simultáneamente que estas condiciones son estrictamente más fuertes que los requisitos estándar para las $\infty$-categorías sintéticas.