Formalising the Bruhat-Tits Tree

A continuación presento un resumen técnico detallado del artículo "Formalising the Bruhat–Tits Tree" (Formalización del Árbol de Bruhat–Tits), publicado en Annals of Formalized Mathematics (2026) por Judith Ludwig y Christian Merten.

1. Problema y Contexto

El artículo aborda la formalización de una herramienta fundamental en la teoría de números y la geometría aritmética: el Árbol de Bruhat–Tits. Este objeto combinatorio, construido a partir de retículos en $K^2$ (donde $K$ es un campo de valoración discreta), es esencial para estudiar subgrupos de $GL_2(K)$, homología, formas modulares y la teoría de representaciones de grupos reductivos sobre campos locales no arquimedianos.

El problema central es la ausencia de una formalización previa de este concepto en asistentes de prueba (proof assistants). Los autores buscan llenar este vacío utilizando Lean 4 y su biblioteca matemática mathlib4, con el objetivo específico de verificar un resultado de investigación en curso sobre co-cadenas armónicas (harmonic cochains) y su relación con formas automorfas sobre campos de funciones.

2. Metodología

La metodología se basa en la implementación rigurosa de conceptos algebraicos y combinatorios dentro del ecosistema de Lean 4, aprovechando la biblioteca mathlib.

• Entorno y Herramientas: Se utilizó Lean 4 (versión estable v4.19.0) y mathlib4. El código, de aproximadamente 8.000 líneas, está organizado en cinco carpetas, siendo la principal Graph/Tree.lean.
• Generalización: En lugar de trabajar únicamente con el campo de los números p-ádicos ($\mathbb{Q}_p$), la formalización se realiza en un contexto más general: $K$ es un campo con un anillo de valoración discreta $R$ (no necesariamente completo ni con cuerpo residual finito, aunque estas propiedades se asumen para aplicaciones específicas).
• Enfoque de Diseño:
  • Se definieron clases de tipos (typeclasses) para retículos (IsLattice) y se estructuraron como módulos finitamente generados sobre $R$ que generan $K^2$.
  • Se abordaron desafíos de tipado al trabajar con bases de retículos, comparando diferentes perspectivas (submódulos de $K^2$ vs. span de bases de $K^2$) para facilitar el uso del principio de inducción de igualdad.
  • Se implementó una acción de grupo transita de $GL_2(K)$ sobre el árbol.

3. Contribuciones Clave

A. Descomposición de Cartan para $GL_n(K)$

Antes de construir el árbol, los autores formalizaron la Descomposición de Cartan para $GL_n(K)$.

• Teorema: $GL_n(K) = \bigsqcup_{t \in T^-} GL_n(R) \cdot t \cdot GL_n(R)$, donde $T^-$ son matrices diagonales con entradas potencias del uniformizador $\varpi$ ordenadas decrecientemente.
• Implementación: La prueba sigue un algoritmo tipo Gaussiano, demostrando la existencia (mediante manipulación de filas/columnas y normalización de entradas) y la unicidad de la tupla de enteros que define la clase de doble coset.
• Significado: Esta descomposición es crucial para definir la distancia entre retículos y establecer la estructura del árbol.

B. Construcción del Árbol de Bruhat–Tits

Se formalizó la construcción del árbol como un grafo simple infinito y regular:

• Vértices: Clases de equivalencia de retículos bajo homotecia ($L \sim \alpha L$).
• Aristas: Dos vértices son adyacentes si sus representantes de retículos $L, L'$ satisfacen $\varpi L \subsetneq L' \subsetneq L$.
• Distancia: Se definió una función de distancia $d(L, L')$ basada en la diferencia de los exponentes en la descomposición de Cartan de una base de un retículo respecto al otro.
• Propiedades Verificadas:
  • Conexidad: Probada por inducción sobre la distancia.
  • Aciclicidad: Demostrada transformando cualquier camino (trail) en una "cadena estándar" mediante la acción de $GL_2(K)$, probando que la distancia gráfica coincide con la distancia algebraica.
  • Regularidad: Se verificó que si el cuerpo residual es finito de cardinalidad $q$, el árbol es regular de grado $q+1$.

C. Co-cadenas Armónicas y Suryectividad del Laplaciano

La aplicación principal de la formalización fue verificar un teorema sobre co-cadenas armónicas.

• Definición: Se definió el Laplaciano de Bruhat–Tits $\Delta: \text{Maps}(E(T), M) \to \text{Maps}(V(T), M)$, donde $M$ es un módulo sobre un anillo conmutativo $A$.
• Resultado Formalizado: Se demostró que $\Delta$ es sobre (surjective) bajo condiciones generales (árbol localmente finito con grado mínimo 2).
• Secuencia Exacta: Se verificó la secuencia corta exacta de $SL_2(K)$-módulos:
  $$0 \to \text{Har}(T, \mathbb{Z}) \to \text{Maps}(E(T), \mathbb{Z}) \xrightarrow{\Delta} \text{Maps}(V(T), \mathbb{Z}) \to 0$$
• Generalización: Un hallazgo notable fue que, gracias a la flexibilidad de Lean, los autores pudieron generalizar la prueba de la suryectividad desde el caso de valores en $\mathbb{Z}$ a valores en un módulo arbitrario $M$ sobre un anillo $A$, sin esfuerzo adicional significativo en el código.

4. Resultados Técnicos

• Código: Se produjeron aproximadamente 8.000 líneas de código Lean, integrando definiciones de retículos, la descomposición de Cartan, la estructura del árbol y la teoría de co-cadenas.
• Eficiencia de Verificación: La verificación de la prueba de suryectividad del Laplaciano fue notablemente eficiente, con una relación de menos de 750 líneas de código Lean por 140 líneas de LaTeX, lo que indica una alta correspondencia entre la demostración matemática informal y la formal.
• Integración: Se han comenzado a integrar componentes clave (definición de retículos, cardinalidad de proyecciones de espacios vectoriales finitos) en mathlib.

5. Significado e Impacto

• Avance en Matemáticas Formales: Este trabajo marca la primera formalización completa del árbol de Bruhat–Tits en un asistente de prueba, sentando las bases para la formalización de la teoría de edificios de Bruhat–Tits para grupos reductivos generales.
• Apoyo a la Investigación Activa: El proyecto demuestra la viabilidad de utilizar asistentes de prueba para verificar resultados de investigación de nivel de posgrado en teoría de números, específicamente en el contexto de formas automorfas sobre campos de funciones y cociclos theta analíticos rígidos.
• Herramienta para la Teoría de Representaciones: Al formalizar la acción de $GL_2(K)$ y $SL_2(K)$ y la estructura de las co-cadenas armónicas, se proporciona una base verificada para futuros trabajos sobre cohomología de grupos y la correspondencia de Langlands en contextos de campos de funciones.
• Mejora de la Documentación Matemática: El proceso de formalización obligó a los autores a clarificar definiciones y probar resultados de manera no ambigua, mejorando la calidad de su propia investigación y documentación.

En resumen, el artículo no solo proporciona una implementación técnica robusta de un objeto matemático complejo, sino que también valida el uso de herramientas formales como un componente integral en el ciclo de investigación matemática moderna.