Hypercubical manifolds in homotopy type theory

Resumen Técnico: Variedades Hipercubicales en la Teoría de Tipos Homotópicos

Planteamiento del Problema
La teoría de tipos homotópicos (HoTT) ofrece un marco sintético para la topología donde los tipos representan espacios hasta la equivalencia de homotopía. Si bien muchos espacios clásicos pueden definirse como Tipos Inductivos Superiores (HIT) especificando sus estructuras de celdas (por ejemplo, la variedad hipercubical $K$ como un complejo CW), establecer su relación con las acciones de grupo es no trivial. Específicamente, la variedad hipercubical se define clásicamente como el cociente de la 3-esfera $S^3$ por una acción libre del grupo de cuaterniones $Q$. En HoTT, definir tal acción requiere un mapa coherente $\phi: BQ \to \mathcal{U}$ (donde $BQ$ es el deloop de $Q$) tal que la fibra sea $S^3$. Sin embargo, los principios de eliminación estándar para $BQ$ solo permiten la eliminación hacia grupoides, mientras que $S^3$ no es $n$-truncada para ningún $n$. En consecuencia, no hay una forma directa de definir la acción de $Q$ sobre $S^3$ dentro de la teoría, lo que dificulta probar que la definición de $K$ como HIT es equivalente a la definición de cociente $S^3/Q$.

Metodología
Los autores emplean una estrategia de dos pasos aprovechando la dualidad entre fibraciones y acciones de grupo, y el lema de aplanamiento (flattening lemma) para computar las fibras de los HIT.

1. Dualidad Acción-Fibración: En lugar de intentar definir directamente la acción $\phi: BQ \to \mathcal{U}$, los autores definen un mapa $\phi: K \to BQ$ desde la variedad hacia el deloop. Por la dualidad acción-fibración (Proposición 5), una secuencia de fibra $F \to K \to BQ$ corresponde a una acción coherente de $Q$ sobre $F$, donde $K$ es el cociente homotópico. El objetivo es, por tanto, probar que la fibra de $\phi$ es $S^3$.
2. Computación Iterativa de la Fibra: El mapa $\phi$ se construye utilizando el principio de eliminación de $K$ (definido como un HIT con 2 puntos, 4 caminos, 3 2-celdas y 1 3-celda). Para computar la fibra de $\phi$, los autores proceden por inducción sobre los esqueletos de $K$ ($K_0, K_1, K_2, K_3$).
   • Utilizan el Lema de Aplanamiento (Lema 3) para computar el espacio total de la fibración sobre pushouts y coequivalentes.
   • Para cada esqueleto $K_k$, computan la fibra del mapa restringido $\phi_k: K_k \to BQ$.
   • La computación revela que la fibra del 0-esqueleto es un conjunto discreto de 8 puntos (copias de $Q$), la fibra del 1-esqueleto es el 1-esqueleto de un teseracto (homotópicamente equivalente a $S^3$), y los pasos subsecuentes adjuntan celdas para reconstruir la estructura completa de la 3-esfera.
3. Generalización de Dimensiones Superiores: Los autores generalizan esta construcción utilizando la operación de unión (join) en la teoría de tipos. Definen variedades de dimensiones superiores $K_n$ como la unión iterada de $n$ copias de $K$ sobre $BQ$. Esta construcción se basa en la propiedad de que la unión de secuencias de fibra produce una nueva secuencia de fibra, y que las uniones aumentan la conectividad.

Contribuciones Clave y Resultados

• Definición Sintética de $K$: El artículo proporciona una definición formal de la variedad hipercubical $K$ como un Tipo Inductivo Superior en HoTT.
• Equivalencia de Definiciones: El resultado principal (Teorema 10) establece una secuencia de fibra $S^3 \to K \to BQ$. Esto prueba que la definición de $K$ como HIT es, de hecho, el cociente homotópico de $S^3$ por el grupo de cuaterniones $Q$, validando la construcción sintética frente a la definición topológica clásica.
• Grupo Fundamental: Como consecuencia de la secuencia de fibra, los autores prueban que el grupo fundamental de $K$ es $Q$ (Proposición 12).
• Recubrimiento Universal: El artículo demuestra que $S^3$ es el recubrimiento universal de $K$ (Teorema 14), recuperando la estructura de la fibración de Galois sintéticamente.
• Aproximaciones de Dimensiones Superiores: Los autores introducen una secuencia de tipos $K_n$ (donde $K_1 = K$) definidas mediante uniones iteradas. Prueban que $K_n$ es el cociente de $S^{4n-1}$ por $Q$ y que el mapa canónico $K_n \to BQ$ es $(4n-2)$-conectado (Proposición 19).
• Convergencia al Deloop: En el límite, la secuencia converge a un tipo $K_\infty$ que es equivalente a $BQ$, proporcionando una aproximación celular no recursiva del deloop de $Q$ que evita la truncación formal de grupoide.

Significado
El artículo ilustra el poder constructivo de la teoría de tipos homotópicos al resolver un problema combinatorio sutil: definir una acción de grupo coherente sobre un espacio no truncado sin una definición directa de la acción. Al trabajar hacia atrás desde el espacio cociente hacia la acción mediante el lema de aplanamiento, los autores muestran que los métodos sintéticos pueden recuperar hechos topológicos profundos sobre las acciones de grupo y los recubrimientos universales.

La construcción de $K_n$ ofrece un modelo celular práctico para computar la cohomología de $Q$ en dimensiones bajas, ya que se espera que estos tipos sean celulares y aptos para la computación sintética. Además, la metodología se presenta como un enfoque general para definir tipos correspondientes a espacios obtenidos mediante el pegado de caras de poliedros (como la esfera de Poincaré). Finalmente, el trabajo contribuye al programa más amplio de la construcción de $SU(2)$ y su deloop en HoTT, ya que la acción de $Q$ sobre $S^3$ es un caso específico de la acción de $SU(2)$ sobre sí mismo.