Resumo Técnico: Formalização de Complexos Simpliciais Abstratos e Subdivisões Estelares em Lean

Declaração do Problema

A teoria dos complexos simpliciais é fundamental para a topologia algébrica e combinatória, servindo como uma ferramenta primária para computar invariantes como homologia e gênero, e para estudar tipos de homotopia via teoria de Morse discreta e algoritmos de colapso. Embora as definições clássicas frequentemente dependam de imersões geométricas no espaço Euclidiano (usando coordenadas baricêntricas e independência afim), tais abordagens introduzem dados extrínsecos que complicam a computação formal.

Os autores identificam uma lacuna no ecossistema de assistentes de prova Lean: embora a mathlib contenha várias formalizações relacionadas a complexos simpliciais, elas carecem de interconexão, e não existe uma formalização existente de subdivisões estelares. Além disso, as formalizações existentes em outros assistentes (Rocq, ACL2) são fortemente orientadas a aplicações computacionais específicas (por exemplo, homologia persistente, dual de Alexander) em vez de fornecerem um fundamento combinatório coeso para teoremas estruturais como os de Alexander e Pachner sobre triangulações de variedades. O artigo aborda a necessidade de um framework puramente combinatório no Lean 4 que suporte a verificação rigorosa de identidades envolvendo subdivisões estelares, links e joins, mantendo a compatibilidade com o conteúdo existente da biblioteca e a computabilidade.

Metodologia

Os autores adotam um framework puramente combinatório, definindo Complexos Simpliciais Abstratos como coleções de conjuntos finitos (faces) fechados sob a relação de subconjunto, independentemente de qualquer espaço geométrico ambiente. Esta abordagem remove condições geométricas (independência afim, interseções de envelopes convexos) encontradas na estrutura SimplicialComplex da mathlib, reduzindo assim o overhead e simplificando as assinaturas de tipos.

As principais escolhas metodológicas incluem:

• Type-Casting e Coerções: Para lidar com operações que alteram o tipo de vértice subjacente (ex: joins, subdivisões), os autores definem SimplicialCoe, uma estrutura que representa mapas injetivos em conjuntos de vértices. Isso permite um reetiquetamento "sem perdas" sem exigir bijeções globais nos tipos ambientes.
• União Disjunta para Joins: Para definir o join de dois complexos ($K \star L$) sem assumir conjuntos de vértices disjuntos, os autores utilizam um tipo produto $E \times k$ (onde $k$ é um semiring não trivial) para indexar as faces, criando efetivamente cópias disjuntas dos conjuntos de vértices.
• Subdivisões Estelares: A subdivisão $\sigma_s K$ de uma face $s$ é definida combinatoriamente removendo o interior do star de $s$ e substituindo-o pelo join do link de $s$, a fronteira de $s$ e um novo vértice baricentro $x$.
• Verificação Formal: Todas as definições e teoremas são implementados em Lean 4. Os autores priorizam a preservação da computabilidade e a minimização de suposições para facilitar a futura integração com a mathlib.

Principais Contribuições

O artigo apresenta a primeira formalização de subdivisões estelares em qualquer assistente de prova. As contribuições específicas são:

1. Formalização de Complexos Simpliciais Abstratos:

   • Definição da estrutura central AbstractSimplicialComplex e sua conversão de/para instâncias de SimplicialComplex geométricas.
   • Formalização de morfismos (SimplicialMap), isomorfismos (SimplicialIso) e coerções (SimplicialCoe).
   • Implementação de operações padrão: uniões, interseções, subcomplexos e cálculos de dimensão.

2. Formalização de Subcomplexos e Operações:

   • Definições rigorosas e provas de propriedades para links ($Lk(K, s)$), fronteiras de faces ($\partial s$), stars ($St(K, s)$), complementos de star, cones e joins ($K \star L$).
   • Prova de leis distributivas, associatividade e comutatividade (até isomorfismo/coerção) para joins.
   • Estabelecimento de identidades mostrando como essas operações interagem com isomorfismos e coerções.

3. Formalização de Subdivisões Estelares:

   • Definição da subdivisão estelar $\sigma_s K$ e da soldagem estelar (a operação inversa).
   • Definição de equivalência estelar ($K \cong_{st} L$) como o fechamento transitivo de movimentos estelares.
   • Prova de que a equivalência estelar é preservada sob type-casting injetivo (Teorema 3.2), garantindo que a relação de equivalência seja robusta contra mudanças no etiquetamento de vértices.

4. Novos Teoremas e Identidades:

   • Derivação de identidades descrevendo a interação entre subdivisões estelares e links. Notavelmente, o Teorema 3.9 estabelece que, para uma face $t$ no link da face subdividida, o link de $t$ no complexo subdividido é a subdivisão estelar do link original: $Lk(\sigma_s K, t) = \sigma_{s \setminus t}(Lk(K, t))$.
   • Os autores observam que esta identidade específica, juntamente com outras relativas à "anticomutatividade" de links e subdivisões, não possui referência padrão na literatura e foi derivada durante o processo de formalização.

Resultados

A formalização verifica com sucesso um conjunto de identidades comumente usadas no estudo de variedades trianguladas:

• Preservação de Link: Se uma face $t$ está fora do star subdividido, seu link permanece inalterado ($Lk(\sigma_s K, t) = Lk(K, t)$).
• Compatibilidade de Join: Subdivisões estelares distribuem-se sobre joins de formas específicas, ex: $(\sigma_s K) \star L = \sigma_{s \sqcup \emptyset}(K \star L)$.
• Preservação de Equivalência: A equivalência estelar é preservada sob isomorfismos simpliciais e type-casting injetivo, desde que o tipo alvo tenha "espaço" suficiente para novos rótulos de baricentro.
• Volume de Código: O projeto compreende atualmente aproximadamente 14.000 linhas de código Lean, cobrindo definições, lemas utilitários e provas.

Significância e Alegações

Os autores posicionam este trabalho como um passo fundamental em direção à formalização dos teoremas de Alexander e Pachner, que afirmam que triangulações de variedades são homeomorfas se, e somente se, estão relacionadas por uma sequência de movimentos estelares (ou bistelares).

• Primeiro de seu Tipo: O artigo afirma ser a primeira formalização de subdivisões estelares em qualquer assistente de prova.
• Unindo Teoria e Computação: Ao adotar um framework combinatório, o trabalho visa tornar a teoria dos complexos simpliciais mais adequada a técnicas computacionais e aplicações algorítmicas (ex: em Análise de Dados Topológicos e softwares como o Regina).
• Catalogação de Folclore: Os autores argumentam que muitas identidades técnicas na topologia combinatória tornaram-se "folclore" devido à natureza tediosa de suas provas. Esta formalização serve para catalogar e verificar esses resultados, garantindo que suas lacunas lógicas sejam preenchidas.
• Escopo Modesto: Os autores declaram explicitamente que este é um "trabalho inicial". Eles não pretendem ter formalizado os teoremas de Pachner ainda, mas forneceram a infraestrutura necessária (subdivisões, links, joins e relações de equivalência) para fazê-lo. Eles também reconhecem que, embora tenham isolado os aspectos combinatórios, o trabalho futuro será necessário para integrar totalmente estes resultados com as definições geométricas de SimplicialComplex na mathlib e para lidar com as complexidades de complexos totais (onde cada singleton é uma face).

O trabalho enfatiza uma filosofia de design que prioriza a computabilidade e a compatibilidade com a mathlib, visando criar uma base simplificada para desenvolvimentos futuros em topologia combinatória dentro do ecossistema Lean.