Definition of the Bruhat-Tits graph

In this file we define the Bruhat-Tits graph as a simple graph and show it is connected.

@[implicit_reducible]

noncomputable instance BruhatTits.instInhabitedVertices {K : Type u_1} [Field K] {R : Subring K} : Inhabited (Vertices R)

Equations

• BruhatTits.instInhabitedVertices = { default := ⟦Lattice.standard R⟧ }

noncomputable def BruhatTits.BTgraph {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] : SimpleGraph (Vertices R)

The Bruhat-Tits graph defined as a simple graph. The vertices are given by the homothety classes of lattices. Two vertices are connected by an edge if they are neighbours, i.e. if their distance is equal to 1.

Equations

• BruhatTits.BTgraph = { Adj := fun (L M : BruhatTits.Vertices R) => BruhatTits.IsNeighbour L M, symm := ⋯, loopless := ⋯ }

theorem BruhatTits.BTgraph_adj {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L M : Vertices R) : BTgraph.Adj L M = IsNeighbour L M

theorem BruhatTits.reachable {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Vertices R) {n : ℕ} (h : inv M L = n) : BTgraph.Reachable M L

There is a path between any two vertices.

theorem BruhatTits.BTgraph_connected {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] : BTgraph.Connected

The Bruhat-Tits graph is connected.