Formalisation of the Bruhat-Tits Tree

This repository contains a formalisation of the Bruhat-Tits tree of the general linear group over a discretely valued field and a proof that it is a regular tree of degree where is the cardinality of the finite residue field.

Layout of the repository

The code is organized into the five folders Cartan, Graph, Harmonic, Lattice and Utils.

The folder Graphcontains the main constructions:

• The vertices of the Bruhat-Tits tree are defined in the file Graph/Vertices.lean, and the edges in Graph/Edges.lean.
• The Bruhat-Tits tree is defined as a graph BTgraph in Graph/Graph.lean.
• The main theorem theorem BTtree which shows that the Bruhat-Tits graph is indeed a tree can be found at the end of the file Graph/Tree.lean.
• The file Graph/Regular.lean contains the theorem btgraph_regular, showing that the tree is regular.
• In Graph/GroupAction.lean the action of on the tree is defined.

Vertices of the Bruhat-Tits tree are defined as homothety classes of -lattices in , where is a DVR with fraction field . The folder Lattice contains the formalisation of the notion of lattices as well as various constructions needed to define the tree. Notably, the file Lattice/Distance.lean contains the definition dist of the distance of lattices and various results about it.

An important result needed for the concept of distance of lattices and to define the edges of the tree is the Cartan decomposition. This result for the group is formalised in the folder Cartan with the file Cartan/Existence.lean containing the decomposition result on the matrices and Cartan/Uniqueness.lean containing the result theorem cartan_decomposition_unique, that the diagonal matrix occurring in the decomposition is unique.

As an application, in the folder Harmonic, we verify a result in the context of harmonic cochains on the Bruhat--Tits tree. The main result there, in Harmonic/Application.lean, is theorem BTlaplace_surjective, which shows surjectivity of a Laplacian. In Harmonic/Basic.lean we develop this in a more general setup; we define a Laplacian for simple graphs and show surjectivity for certain trees.

The folder Utils contains auxiliary results, e.g., from linear algebra, that are needed in the main files, but are not directly related to the concepts we formalise.

For a visualisation of the dependencies, have a look at the import graph.

Paper

For a short exposition of this formalisation, we refer to this article.