Proof that the Bruhat-Tits graph is a tree

Let R be a discrete valuation ring and K its fraction field.

In this file we show that the Bruhat-Tits graph associated to R is acyclic (i.e. without loops) and conclude that it is a tree. The connectedness was already shown in BruhatTits.Graph.Graph (see BruhatTits.BTGraph_connected).

The strategy for proving acyclicity is as follows:

• Show that every trail (i.e. a walk that has no self-intersections in the interior, but possibly at the ends) can be transformed into a standard walk by the action of GL₂(K). Here a standard walk is a walk that is represented by a standard sequence of lattices (see List.IsBTStandard).
• The length of a standard walk is the distance (in the sense of inv) of the endpoints, so by the first point, this also holds for every trail.
• In particular, the second point holds for a circle at x, but a circle always has length at least 3 > 0 = inv x x, so no circles exist.

theorem SimpleGraph.Walk.exists_repr_isChain {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {x y : BruhatTits.Vertices R} (p : BruhatTits.BTgraph.Walk x y) : ∃ (l : List (BruhatTits.Lattice R)), l.IsBTChain ∧ List.map (fun (L : BruhatTits.Lattice R) => ⟦L⟧) l = p.support

Any walk is representable by a chain of lattices. If the walk is a trail, the chain is simple (see BruhatTits.exists_repr_isSimpleChain_of_isTrail).

noncomputable def BruhatTits.chainToWalk {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (l : List (Lattice R)) (hl : l ≠ []) (hc : l.IsBTChain) : BTgraph.Walk ⟦l.head hl⟧ ⟦l.getLast hl⟧

A non-empty chain of lattices defines a walk on the Bruhat-Tits graph.

Equations

• BruhatTits.chainToWalk [L] hl_2 hc_2 = SimpleGraph.Walk.nil' ⟦L⟧
• BruhatTits.chainToWalk (L₁ :: L₂ :: l_2) hl_2 hc_2 = SimpleGraph.Walk.cons ⋯ (BruhatTits.chainToWalk (L₂ :: l_2) ⋯ ⋯)

theorem BruhatTits.isSimpleChain_of_isTrail_aux {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {x y : Vertices R} (p : BTgraph.Walk x y) (hp : p.IsTrail) (l : List (Lattice R)) (hl : List.map (fun (L : Lattice R) => ⟦L⟧) l = p.support) : List.Forall id (List.zipWith₃ (fun (L₁ x L₃ : Lattice R) => ¬Lattice.IsSimilar R L₁ L₃) l l.tail l.tail.tail)

theorem BruhatTits.exists_repr_isSimpleChain_of_isTrail {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {x y : Vertices R} (p : BTgraph.Walk x y) (hp : p.IsTrail) : ∃ (l : List (Lattice R)), l.IsBTSimpleChain ∧ List.map (fun (L : Lattice R) => ⟦L⟧) l = p.support

If p is a trail in the Bruhat-Tits graph, it is representable by a simple chain of lattices.

def SimpleGraph.Walk.IsStandard {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {x y : BruhatTits.Vertices R} (p : BruhatTits.BTgraph.Walk x y) : Prop

A walk on the Bruhat-Tits graph is a standard walk, if there exists a sequence of representing lattices (Lᵢ) with pᵢ = ⟦Lᵢ⟧ such that the sequence (Lᵢ) is a standard sequence (see List.IsBTStandard).

Equations

• p.IsStandard = ∃ (l : List (BruhatTits.Lattice R)), List.map (fun (L : BruhatTits.Lattice R) => ⟦L⟧) l = p.support ∧ l.IsBTStandard

theorem BruhatTits.isStandard_of_list_isStandard {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {x y : Vertices R} {p : BTgraph.Walk x y} (l : List (Lattice R)) (hleq : List.map (fun (L : Lattice R) => ⟦L⟧) l = p.support) (hl : l.IsBTStandard) : p.IsStandard

theorem BruhatTits.length_eq_inv_of_isStandard {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {x y : Vertices R} {p : BTgraph.Walk x y} (h : p.IsStandard) : p.length = inv x y

If p is a standard walk from x to y, the length of p is the distance inv x y.

theorem BruhatTits.exists_map_isStandard {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {x y : Vertices R} {p : BTgraph.Walk x y} (hp : p.IsTrail) : ∃ (g : GL (Fin 2) K), (SimpleGraph.Walk.map (RelIso.toRelEmbedding g.toGraphIso).toRelHom p).IsStandard

Given two vertices and a trail p from x to y, there exists a g : GL₂(K) such that g • p is a standard walk.

theorem BruhatTits.length_eq_inv {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {x y : Vertices R} {p : BTgraph.Walk x y} (hp : p.IsTrail) : p.length = inv x y

The length of a trail is equal to the distance of the endpoints.

theorem BruhatTits.dist_BTgraph_eq_inv {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] : BTgraph.dist = inv

The graph-theoretic distance agrees with our constructed inv function.

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

The Bruhat-Tits graph has no loops, i.e. it is acyclic.

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

The Bruhat-Tits graph is a tree.