Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalising the Bruhat-Tits Tree

Judith Ludwig, Christian Merten

TL;DR

The work presents a formalisation of the Bruhat--Tits tree for $\mathrm{GL}_2(K)$ in Lean 4, generalising from $\mathbb{Q}_p$ to arbitrary discrete valuation fields and linking lattice theory, Cartan decomposition, and harmonic cochains. It develops a constructive framework for lattices, a distance function yielding a tree structure, and a surjective Laplacian on edge-valued cochains, with a concrete Lean verification. A key contribution is the integration pathway into mathlib4, including a reusable lattice API and formalised group actions, paving the way for deeper formal study of $p$-adic groups and function field analogues. The work also documents an application to harmonic cochains and outlines ongoing research directions in rigid analytic theta cocycles and Drinfeld’s upper half plane, highlighting both the potential and current limitations of formalising advanced number-theoretic constructions.

Abstract

In this article we describe the formalisation of the Bruhat-Tits tree - an important tool in modern number theory - in the Lean Theorem Prover. Motivated by the goal of connecting to ongoing research, we apply our formalisation to verify a result about harmonic cochains on the tree.

Formalising the Bruhat-Tits Tree

TL;DR

The work presents a formalisation of the Bruhat--Tits tree for in Lean 4, generalising from to arbitrary discrete valuation fields and linking lattice theory, Cartan decomposition, and harmonic cochains. It develops a constructive framework for lattices, a distance function yielding a tree structure, and a surjective Laplacian on edge-valued cochains, with a concrete Lean verification. A key contribution is the integration pathway into mathlib4, including a reusable lattice API and formalised group actions, paving the way for deeper formal study of -adic groups and function field analogues. The work also documents an application to harmonic cochains and outlines ongoing research directions in rigid analytic theta cocycles and Drinfeld’s upper half plane, highlighting both the potential and current limitations of formalising advanced number-theoretic constructions.

Abstract

In this article we describe the formalisation of the Bruhat-Tits tree - an important tool in modern number theory - in the Lean Theorem Prover. Motivated by the goal of connecting to ongoing research, we apply our formalisation to verify a result about harmonic cochains on the tree.
Paper Structure (17 sections, 5 theorems, 15 equations, 1 figure)

This paper contains 17 sections, 5 theorems, 15 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Lean and mathlib
  3. The Cartan decomposition of $\mathrm{GL}_n(K)$
  4. The Bruhat--Tits Tree
  5. Lattices
  6. Distance function
  7. Perspectives on lattices
  8. Acyclicity
  9. Regularity
  10. Group actions
  11. Subrings or algebras
  12. Harmonic cochains
  13. Surjectivity of the Laplacian
  14. Verification of surjectivity proof
  15. Concluding remarks
  16. ...and 2 more sections

Key Result

Theorem 2.1

There is a decomposition of $\mathrm{GL}_n(K)$ into a disjoint union of double cosets

Figures (1)

  • Figure 1: The Bruhat-Tits tree for $\mathbb{Q}_2$

Theorems & Definitions (11)

  • Theorem 2.1: Cartan decomposition
  • Proposition 3.1: https://github.com/chrisflav/bruhat-tits/blob/b8d0ceceb5cd243b4a4c20be816d591c319e77e9/BruhatTits/Lattice/Distance.lean#L113
  • proof : Proof of Proposition \ref{['prop:inv-factor']}
  • Lemma 3.2
  • Lemma 3.3: https://github.com/chrisflav/bruhat-tits/blob/b8d0ceceb5cd243b4a4c20be816d591c319e77e9/BruhatTits/Graph/Tree.lean#L163
  • Definition 4.1
  • Definition 4.2
  • Definition 4.3
  • Proposition 4.4: https://github.com/chrisflav/bruhat-tits/blob/b8d0ceceb5cd243b4a4c20be816d591c319e77e9/BruhatTits/Harmonic/Basic.lean#L730
  • proof
  • ...and 1 more