Hypercubical manifolds in homotopy type theory

Resumo Técnico: Variedades Hipercubicais em Teoria do Tipo de Homotopia

Enunciado do Problema
A teoria do tipo de homotopia (HoTT) oferece um arcabouço sintético para a topologia onde tipos representam espaços até a equivalência de homotopia. Embora muitos espaços clássicos possam ser definidos como Tipos Indutivos Superiores (HITs) ao especificar suas estruturas de células (por exemplo, a variedade hipercubica $K$ como um complexo CW), estabelecer sua relação com ações de grupos é não trivial. Especificamente, a variedade hipercubica é classicamente definida como o quociente da 3-esfera $S^3$ por uma ação livre do grupo quatérnio $Q$. Em HoTT, definir tal ação requer um mapa coerente $\phi: BQ \to \mathcal{U}$ (onde $BQ$ é o delooping de $Q$) tal que a fibra seja $S^3$. Consequentemente, as eliminações padrão para $BQ$ apenas permitem a eliminação para grupoides, enquanto $S^3$ não é $n$-truncada para qualquer $n$. Assim, não há uma maneira direta de definir a ação de $Q$ sobre $S^3$ dentro da teoria, tornando difícil provar que a definição de $K$ como HIT é equivalente à definição de quociente $S^3/Q$.

Metodologia
Os autores empregam uma estratégia de dois passos aproveitando a dualidade entre fibrações e ações de grupos, e o lema de achatamento (flattening lemma) para computar fibras de HITs.

1. Dualidade Ação-Fibração: Em vez de tentar definir diretamente a ação $\phi: BQ \to \mathcal{U}$, os autores definem um mapa $\phi: K \to BQ$ do manifold para o delooping. Pela dualidade ação-fibração (Proposição 5), uma sequência de fibra $F \to K \to BQ$ corresponde a uma ação coerente de $Q$ sobre $F$, onde $K$ é o quociente de homotopia. O objetivo é, portanto, provar que a fibra de $\phi$ é $S^3$.
2. Computação Iterativa de Fibra: O mapa $\phi$ é construído usando o princípio de eliminação de $K$ (definido como um HIT com 2 pontos, 4 caminhos, 3 2-células e 1 3-célula). Para computar a fibra de $\phi$, os autores procedem por indução nos esqueletos de $K$ ($K_0, K_1, K_2, K_3$).
   • Eles utilizam o Lema de Achatamento (Lema 3) para computar o espaço total da fibração sobre pushouts e coequalizadores.
   • Para cada esqueleto $K_k$, eles computam a fibra do mapa restrito $\phi_k: K_k \to BQ$.
   • A computação revela que a fibra do 0-esqueleto é um conjunto discreto de 8 pontos (cópias de $Q$), a fibra do 1-esqueleto é o 1-esqueleto de um tesserato (homotopicamente equivalente a $S^3$) e os passos subsequentes anexam células para reconstruir a estrutura completa da 3-esfera.
3. Generalização para Dimensões Superiores: Os autores generalizam esta construção usando a operação de junção (join) em teoria de tipos. Eles definem variedades de dimensões superiores $K_n$ como a junção iterada de $n$ cópias de $K$ sobre $BQ$. Esta construção baseia-se na propriedade de que a junção de sequências de fibra resulta em uma nova sequência de fibra, e que as junções aumentam a conectividade.

Principais Contribuições e Resultados

• Definição Sintética de $K$: O artigo fornece uma definição formal da variedade hipercubica $K$ como um Tipo Indutivo Superior em HoTT.
• Equivalência de Definições: O resultado principal (Teorema 10) estabelece uma sequência de fibra $S^3 \to K \to BQ$. Isso prova que a definição de $K$ como HIT é, de fato, o quociente de homotopia de $S^3$ pelo grupo quatérnio $Q$, validando a construção sintética contra a definição topológica clássica.
• Grupo Fundamental: Como consequência da sequência de fibra, os autores provam que o grupo fundamental de $K$ é $Q$ (Proposição 12).
• Cobertura Universal: O artigo demonstra que $S^3$ é a cobertura universal de $K$ (Teorema 14), recuperando a estrutura de fibração de Galois sinteticamente.
• Aproximações de Dimensões Superiores: Os autores introduzem uma sequência de tipos $K_n$ (onde $K_1 = K$) definidos via junções iteradas. Eles provam que $K_n$ é o quociente de $S^{4n-1}$ por $Q$ e que o mapa canônico $K_n \to BQ$ é $(4n-2)$-conectado (Proposição 19).
• Convergência para o Delooping: No limite, a sequência converge para um tipo $K_\infty$ que é equivalente a $BQ$, fornecendo uma aproximação celular e não recursiva do delooping de $Q$ que evita a truncagem formal de grupoides.

Significância
O artigo ilustra o poder construtivo da teoria do tipo de homotopia ao resolver um problema combinatório sutil: definir uma ação de grupo coerente em um espaço não truncado sem uma definição direta da ação. Ao trabalhar de trás para frente, do espaço quociente para a ação via o lema de achatamento, os autores mostram que métodos sintéticos podem recuperar fatos topológicos profundos sobre ações de grupos e coberturas universais.

A construção de $K_n$ oferece um modelo celular prático para computar a cohomologia de $Q$ em baixas dimensões, pois espera-se que esses tipos sejam celulares e passíveis de computação sintética. Além disso, a metodologia é apresentada como uma abordagem geral para definir tipos correspondentes a espaços obtidos pelo colamento de faces de poliedros (como a esfera de Homologia de Poincaré). Finalmente, o trabalho contribui para o programa mais amplo de construção de $SU(2)$ e seu delooping em HoTT, uma vez que a ação de $Q$ sobre $S^3$ é um caso específico da ação de $SU(2)$ sobre si mesmo.