Formalising the Bruhat-Tits Tree

Resumo Técnico: Formalização da Árvore de Bruhat–Tits

Autores: Judith Ludwig e Christian Merten
Publicação: Annals of Formalized Mathematics, Vol. 2 (2026)
Ferramenta: Lean 4 (Teorema Prover) e biblioteca mathlib4

1. O Problema e o Contexto

A Árvore de Bruhat–Tits é um objeto combinatório fundamental na teoria dos números e na geometria aritmética, servindo como uma ferramenta poderosa para estudar subgrupos de grupos lineares gerais sobre corpos de valores discretos (como $\mathbb{Q}_p$). Ela conecta a estrutura de grupos como $GL_2(K)$ e $SL_2(K)$ à teoria de representações e formas modulares.

Apesar de sua importância teórica, até a publicação deste artigo, a árvore de Bruhat–Tits nunca havia sido formalizada em um assistente de prova. O objetivo do projeto foi preencher essa lacuna, formalizando não apenas a construção da árvore, mas também aplicá-la para verificar um resultado de pesquisa ativa sobre cochain harmônicas (cochains harmônicas), demonstrando a viabilidade de usar ferramentas de prova formal em matemática de nível de pós-graduação e pesquisa de ponta.

2. Metodologia

O trabalho foi realizado utilizando o Lean 4, um provador de teoremas interativo baseado no Cálculo de Construções Indutivas, apoiado pela biblioteca matemática mathlib4.

• Abordagem Geral: Os autores generalizaram o contexto, substituindo o corpo de números $p$-ádicos ($\mathbb{Q}_p$) por um corpo de valor discreto $K$ com anel de valoração discreto $R$.
• Estrutura do Código: O projeto consiste em aproximadamente 8.000 linhas de código, organizadas em cinco pastas, com foco principal na construção da árvore como um grafo simples.
• Desafios de Formalização:
  • Decomposição de Cartan: A base teórica para a construção da árvore é a decomposição de Cartan de $GL_n(K)$. Os autores formalizaram uma prova baseada em um algoritmo do tipo Gaussiano (e não na forma normal de Smith), permitindo que a prova funcionasse sobre anéis de valoração gerais.
  • Representação de Retículos (Lattices): Um desafio central foi a representação de retículos $R$-módulos em $K^2$. Os autores desenvolveram três perspectivas formais para lidar com bases e submódulos, optando por uma abordagem que evita o "casting" (conversão de tipos) constante entre o módulo e o espaço vetorial, utilizando igualdades de retículos diretamente para facilitar a indução.
  • Ação de Grupos: Formalizaram a ação transitiva de $GL_2(K)$ e a ação não transitiva de $SL_2(K)$ (que preserva a paridade dos vértices), definindo a árvore como um grafo com ação de grupo.

3. Principais Contribuições

1. Formalização da Decomposição de Cartan:

   • Prova formal da decomposição $GL_n(K) = \bigsqcup_{t \in T^-} GL_n(R) \cdot t \cdot GL_n(R)$.
   • Estabelecimento da unicidade da decomposição e da independência da escolha do uniformizante.
   • Integração de APIs para manipulação de matrizes e anéis de valoração.

2. Construção da Árvore de Bruhat–Tits:

   • Definição dos vértices como classes de equivalência de retículos sob homotetia.
   • Definição da função de distância entre vértices baseada na decomposição de Cartan.
   • Prova formal de que o grafo resultante é uma árvore (conexo e acíclico). A prova de aciclicidade foi particularmente complexa, envolvendo a transformação de trilhas em "cadeias padrão" via ação do grupo $GL_2(K)$.
   • Demonstração da regularidade da árvore (grau $q+1$, onde $q$ é o tamanho do corpo residual).

3. Verificação de Resultados sobre Cochain Harmônicas:

   • Definição do Laplaciano de Bruhat–Tits em um contexto geral (grafos locais finitos com pesos).
   • Teorema Principal Verificado: Prova da sobrejetividade do Laplaciano para árvores onde o grau de cada vértice é $\ge 2$.
   • Estabelecimento da sequência exata curta de cochain harmônicas:
     $$0 \to \text{Har}(\mathcal{T}, \mathbb{Z}) \to \text{Maps}(E(\mathcal{T}), \mathbb{Z}) \xrightarrow{\Delta} \text{Maps}(V(\mathcal{T}), \mathbb{Z}) \to 0$$
   • Generalização do resultado: O que começou como uma prova para anéis $\mathbb{Z}$ foi generalizado para módulos arbitrários sobre anéis comutativos, graças à flexibilidade do Lean.

4. Resultados Técnicos

• Correção Matemática: O código Lean garante que todas as definições e teoremas (incluindo a decomposição de Cartan, a estrutura de árvore e a sobrejetividade do Laplaciano) são logicamente consistentes e livres de erros humanos.
• Eficiência de Prova: A prova da sobrejetividade do Laplaciano foi notavelmente eficiente em termos de código, com uma razão de menos de 750 linhas de código Lean para 140 linhas de LaTeX, indicando uma tradução direta e limpa da prova matemática para a formal.
• Integração com mathlib: O projeto já começou a contribuir com a biblioteca mathlib4, adicionando definições de retículos ($R$-lattices) e resultados sobre cardinalidade de espaços projetivos finitos.

5. Significância e Impacto

• Avanço na Matemática Formal: Este é o primeiro trabalho a formalizar a Árvore de Bruhat–Tits, um objeto central na teoria de grupos algébricos e geometria aritmética. Isso marca um passo significativo na formalização de conceitos de nível de pós-graduação em teoria dos números.
• Suporte à Pesquisa Ativa: O projeto demonstra que assistentes de prova podem ser usados não apenas para verificar resultados clássicos, mas para apoiar pesquisas em andamento (neste caso, sobre cociclos de theta analíticos rígidos e formas automorfas em corpos de funções).
• Descobertas Induzidas pela Formalização: O processo de formalização forçou os autores a generalizar suas hipóteses iniciais (de $\mathbb{Z}$ para módulos arbitrários), revelando a robustez do teorema subjacente de uma maneira que a escrita tradicional poderia ter deixado passar.
• Futuro da Documentação Matemática: O trabalho sugere que, no futuro, a formalização poderá se tornar uma parte padrão do processo de publicação e verificação de resultados complexos em matemática pura, garantindo precisão e reprodutibilidade.

Em suma, o artigo não apenas fornece uma implementação verificada de uma estrutura matemática complexa, mas também serve como um estudo de caso sobre como a interação entre matemáticos e provadores de teoremas pode enriquecer tanto a teoria formal quanto a pesquisa matemática ativa.