Delooping presented groups in homotopy type theory

1. Formulação do Problema

Na Teoria dos Tipos Homotópicos (HoTT), os grupos podem ser representados de duas maneiras:

1. Externa: Como conjuntos equipados com operações de multiplicação, unidade e inverso que satisfazem os axiomas.
2. Interna: Como o espaço de laços ($\Omega A$) de um grupóide pontuado e conexo $A$. O tipo $A$ é chamado de delooping do grupo ($BG$).

Embora a existência de um delooping para qualquer grupo seja conhecida, as construções padrão para um grupo arbitrário $G$ frequentemente resultam em tipos complexos que são difíceis de computar ou sobre os quais é difícil raciocinar indutivamente. Especificamente:

• A construção de torção (usando conjuntos-$G$) exige considerar a ação de todo o grupo, levando a tipos grandes.
• A construção via Tipos Indutivos Superiores (HIT) (espaços de Eilenberg-MacLane) tipicamente requer um laço para cada elemento de $G$ e um caminho para cada par de elementos (tabela de multiplicação), resultando em um número massivo de construtores.

Os autores visam desenvolver construções mais simples e computacionalmente eficientes para deloopings quando o grupo é apresentado (ou seja, definido por um conjunto de geradores e relações). Eles buscam reduzir o tamanho dos tipos resultantes para corresponder à complexidade combinatória da apresentação, em vez da estrutura completa do grupo.

2. Metodologia

O artigo emprega a geometria sintética da HoTT, utilizando:

• Tipos Indutivos Superiores (HITs): Para definir espaços com pontos, caminhos e caminhos superiores.
• Truncamento: Para impor propriedades de grupóide (truncando grupos de homotopia superiores).
• Polígrafos: Uma estrutura da teoria da reescrita adaptada à HoTT para gerenciar sistematicamente geradores e relações.
• Dualidade de Grothendieck e Lema de Achamento (Flattening Lemma): Para relacionar sequências de fibras e espaços totais, permitindo o cálculo de núcleos e componentes conexos.
• Formalização: Todos os resultados são formalizados no assistente de prova cubical Agda.

3. Contribuições e Resultados Chave

A. Delooping Simplificado via Conjuntos-Torção Gerados (Seções 3 e 4)

Os autores refinam a construção clássica de torção. Em vez de usar o tipo de todos os conjuntos-$G$ (conjuntos com uma ação de todo o grupo $G$), eles introduzem conjuntos-$X$ (conjuntos com uma ação de um conjunto gerador $X$).

• Teorema 15: Se $G$ é gerado por um conjunto $X$, o componente conexo do conjunto-$X$ principal (derivado do torção-$G$ principal) é um delooping de $G$.
• Significado: Esta construção requer apenas a ação dos geradores, não de todo o grupo.
  • Exemplo: Para o grupo cíclico $\mathbb{Z}$, o delooping padrão é o círculo $S^1$. Os autores mostram que o componente conexo da função sucessor no tipo de endomorfismos ($\Sigma (A:U). (A \to A)$) é um delooping de $\mathbb{Z}$. Isso evita a necessidade de HITs em alguns contextos (como UniMath) e simplifica o raciocínio.

B. Delooping Simplificado via Tipos Indutivos Superiores (Seção 5)

Os autores propõem uma nova construção HIT para um grupo $G$ apresentado por $\langle X \mid R \rangle$.

• Construção ($BP$): Em vez de um laço por elemento do grupo, o tipo $BP$ possui:
  • Um ponto $\star$.
  • Um laço gen para cada gerador $x \in X$.
  • Um 2-caminho rel para cada relação $r \in R$.
  • Um truncamento de grupóide.
• Teorema 24: $BP$ é um delooping do grupo apresentado $[P]$.
• Vantagem: Isso reduz drasticamente o número de construtores em comparação com o $K(G, 1)$ padrão (que requer laços para todos os $|G|$ elementos). Alinha a definição na teoria dos tipos com a teoria combinatória de grupos padrão, facilitando provas por indução que espelham argumentos algébricos tradicionais (por exemplo, transformações de Tietze).

C. 2-Polígrafos e Raciocínio Interno (Seção 6)

Para formalizar a manipulação desses HITs, os autores introduzem 2-polígrafos dentro da HoTT.

• Definição: Uma estrutura consistindo em 0-células (pontos), 1-células (geradores) e 2-células (relações).
• Tipos Apresentados: Eles definem o tipo gerado por um 2-polígrafo como um HIT específico.
• Transformações de Tietze: Eles definem operações (T0, T1, T2) que modificam um polígrafo (adicionando/removendo geradores ou relações) enquanto preservam o tipo apresentado.
• Teorema 29: 2-polígrafos equivalentes por Tietze apresentam o mesmo tipo.
• Significado: Isso permite a manipulação interna de apresentações de grupos dentro da HoTT, possibilitando a conversão de apresentações em formas computacionalmente convenientes (por exemplo, apresentações convergentes via conclusão de Knuth-Bendix) sem alterar o tipo homotópico subjacente.

D. Grafos de Cayley e Complexos (Seção 7)

Os autores fornecem uma interpretação homotópica novel de grafos e complexos de Cayley.

• Grafo de Cayley como Núcleo: Eles provam (Teorema 35) que o grafo de Cayley $C(X, G)$ é o núcleo do mapa $B\gamma^*: BX^* \to BG$ induzido pela apresentação.
  • $BX^*$ é o delooping do grupo livre sobre os geradores.
  • A sequência de fibras $C(X, G) \to BX^* \to BG$ codifica as relações do grupo.
• Complexo de Cayley: Eles estendem isso para duas dimensões, definindo o complexo de Cayley $CP$ como o núcleo do mapa $B_2P \to BG$ (onde $B_2P$ é o 2-esqueleto do delooping).
• Teorema 40 e 43: O complexo de Cayley é o recobrimento universal do tipo $B_2P$.
• Significado: Isso estabelece um link direto entre objetos geométricos clássicos da teoria de grupos (grafos/complexos de Cayley) e a estrutura homotópica dos deloopings, medindo o "defeito" entre o grupo livre e o grupo apresentado.

4. Significado e Impacto

• Eficiência Computacional: As construções propostas produzem tipos com significativamente menos construtores, tornando-os mais adequados para computação e raciocínio automatizado em assistentes de prova como o Agda.
• Ponte entre Álgebra e Topologia: O artigo traduz com sucesso conceitos clássicos da teoria de grupos (geradores, relações, transformações de Tietze, grafos de Cayley) para a linguagem sintética da HoTT, permitindo provas "internas" que se assemelham a provas algébricas tradicionais.
• Raciocínio Metateórico: Ao usar 2-polígrafos, os autores fornecem um arcabouço para raciocinar sobre a estrutura dos próprios HITs, permitindo transformações que preservam o tipo homotópico.
• Fundação para Trabalhos Futuros: O artigo estabelece as bases para a definição de polígrafos de dimensão superior ($n$-polígrafos) e complexos de Cayley superiores, o que poderia levar a provas de coerência automatizadas e computações cohomológicas eficientes para grupos na HoTT.

Em resumo, este trabalho fornece um conjunto de ferramentas para construir modelos "pequenos" e "combinatórios" de deloopings de grupos na Teoria dos Tipos Homotópicos, aproveitando a estrutura específica das apresentações de grupos para simplificar tanto a definição de tipos quanto o raciocínio sobre eles.