The edges of the Bruhat-Tits graph

In this file we define the edge relation of the Bruhat-Tits graph. Two vertices are connected by an edge if they are neighbours, i.e. if their distance, in the sense of inv, is one.

Main definitions

• BruhatTits.IsNeighbour: vertices x and y are neighbours if inv x y = 1.
• BruhatTits.IsStandardNeighbour: lattices L and M are standard neighbours, if ϖ • L < M < L.
• List.IsBTChain: a non-empty list of lattices is a chain, if adjacent elements are standard neighbours.
• List.IsBTSimpleChain: a chain is simple if it does not backtrack.
• List.IsBTStandard: a simple chain L₀, ..., Lₙ is standard if there exists a basis b = (b₁, b₂) of L₀ such that Lᵢ is the span of (ϖ ^ i • b₁, b₂) for all i.

Main results

• BruhatTits.isNeighbour_iff: vertices are neighbours if and only if there exist standard neighbour representatives.
• BruhatTits.length_eq_dist_add_one_of_isStandard: the length of a standard chain agrees with the distance of its endpoints plus one.
• BruhatTits.exists_trafo_to_isStandard: every simple chain can be transformed into a standard chain by the action of GL₂(K).

noncomputable def BruhatTits.IsNeighbour {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (x y : Vertices R) : Prop

Two vertices x and y in the Bruhat-Tits tree are neighbours if inv L M = 1. For a common alternative definition see BruhatTits.isNeighbour_iff.

Equations

• BruhatTits.IsNeighbour x y = (BruhatTits.inv x y = 1)

theorem BruhatTits.isNeighbour_def {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (x y : Vertices R) : IsNeighbour x y ↔ inv x y = 1

theorem BruhatTits.exists_repr_le_of_isNeighbour {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M : Lattice R) (x : Vertices R) (h : IsNeighbour ⟦M⟧ x) : ∃ (L : Lattice R), ⟦L⟧ = x ∧ L.M ≤ M.M ∧ dist M L = 1

If M is a lattice and x a neighbour of ⟦M⟧, there exists a representative L of x such that L ≤ M and dist M L = 1.

theorem BruhatTits.isNeighbour_symm {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (x y : Vertices R) : IsNeighbour x y ↔ IsNeighbour y x

structure BruhatTits.IsStandardNeighbour {K : Type u_1} [Field K] {R : Subring K} (M L : Lattice R) : Prop

M is a standard neighbour of L if ϖ • L < M < L.

• lt : M.M < L.M
• ϖlt (ϖ : ↥R) : Irreducible ϖ → ϖ • L.M < M.M

theorem BruhatTits.smul_isStandardNeighbour {K : Type u_1} [Field K] {R : Subring K} (g : GL (Fin 2) K) (M L : Lattice R) (h : IsStandardNeighbour M L) : IsStandardNeighbour (g • M) (g • L)

GL₂(K) preserves IsStandardNeighbour.

theorem BruhatTits.ntwist_isStandardNeighbour {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (b : Module.Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) : IsStandardNeighbour (b.ntwist₂ hϖ 1 0).toLattice b.toLattice

If b = (b₁, b₂) is a basis of Fin 2 → K, the span of (ϖ • b₁, b₂) is a standard neighbour of the span of b.

theorem BruhatTits.isNeighbour_of_isStandardNeighbour {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {M L : Lattice R} (h : IsStandardNeighbour M L) : IsNeighbour ⟦M⟧ ⟦L⟧

If M is a standard neighbour of L, the vertices ⟦M⟧ and ⟦L⟧ are neighbours.

theorem BruhatTits.exists_basis_eq_ntwist_of_isNeighbour {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M : Lattice R) (L : Vertices R) (h : IsNeighbour ⟦M⟧ L) : ∃ (b : Module.Basis (Fin 2) K (Fin 2 → K)) (ϖ : ↥R) (hϖ : Irreducible ϖ), b.toLattice = M ∧ ⟦(b.ntwist₂ hϖ 1 0).toLattice⟧ = L

theorem BruhatTits.exists_repr_isStandardNeighbour_of_isNeighbour {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M : Lattice R) (x : Vertices R) (h : IsNeighbour ⟦M⟧ x) : ∃ (L : Lattice R), ⟦L⟧ = x ∧ IsStandardNeighbour L M

If M is a lattice with neighbour x, there exists a representative L of x such that L is a standard neighbour of M.

theorem BruhatTits.isNeighbour_iff {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L M : Vertices R) : IsNeighbour L M ↔ ∃ (ϖ : ↥R) (_ : Irreducible ϖ) (L' : Lattice R) (M' : Lattice R), ⟦L'⟧ = L ∧ ⟦M'⟧ = M ∧ ϖ • L'.M < M'.M ∧ M'.M < L'.M

Two vertices are neighbours if and only if there exist representatives L and M and a uniformizer ϖ such that ϖ • L < M < L, i.e. if L is a standard neighbour of M.

This is a common alternative way of defining BruhatTits.IsNeighbour.

structure List.IsBTChain {K : Type u_1} [Field K] {R : Subring K} (l : List (BruhatTits.Lattice R)) : Prop

A list (Lᵢ) of lattices is a chain, if Lᵢ ≤ Lᵢ₊₁ and dist Lᵢ Lᵢ₊₁ = 1 forall i.

• ne_nil : l ≠ []
• isStandardNeighbour : IsChain BruhatTits.IsStandardNeighbour l

theorem BruhatTits.singleton_isChain {K : Type u_1} [Field K] {R : Subring K} (L : Lattice R) : [L].IsBTChain

theorem BruhatTits.cons_isChain_of {K : Type u_1} [Field K] {R : Subring K} {l : List (Lattice R)} {M L : Lattice R} (hl : (L :: l).IsBTChain) (hML : IsStandardNeighbour M L) : (M :: L :: l).IsBTChain

theorem BruhatTits.isChain_of_cons_isChain {K : Type u_1} [Field K] {R : Subring K} {l : List (Lattice R)} {M : Lattice R} (hl : l ≠ []) (h : (M :: l).IsBTChain) : l.IsBTChain

structure List.IsBTSimpleChain {K : Type u_1} [Field K] {R : Subring K} (l : List (BruhatTits.Lattice R)) extends l.IsBTChain : Prop

A chain is simple if it does not backtrack in the interior (i.e. in principle first and last entry can coincide). We will show that every chain is simple.

• ne_nil : l ≠ []
• isStandardNeighbour : IsChain BruhatTits.IsStandardNeighbour l
• no_backtrack : Forall id (zipWith₃ (fun (L₁ x L₃ : BruhatTits.Lattice R) => ¬BruhatTits.Lattice.IsSimilar R L₁ L₃) l l.tail l.tail.tail)

theorem BruhatTits.singleton_isSimpleChain {K : Type u_1} [Field K] {R : Subring K} (L : Lattice R) : [L].IsBTSimpleChain

theorem BruhatTits.isSimpleChain_of_cons_isSimpleChain {K : Type u_1} [Field K] {R : Subring K} {l : List (Lattice R)} {M : Lattice R} (hl : l ≠ []) (h : (M :: l).IsBTSimpleChain) : l.IsBTSimpleChain

structure List.IsBTStandard {K : Type u_1} [Field K] {R : Subring K} (l : List (BruhatTits.Lattice R)) extends l.IsBTSimpleChain : Prop

A chain (Lᵢ) is a standard chain, if L₀ has a basis b such that each Lᵢ is given by b.ntwist₂ hϖ n 0.

• ne_nil : l ≠ []
• isStandardNeighbour : IsChain BruhatTits.IsStandardNeighbour l
• no_backtrack : Forall id (zipWith₃ (fun (L₁ x L₃ : BruhatTits.Lattice R) => ¬BruhatTits.Lattice.IsSimilar R L₁ L₃) l l.tail l.tail.tail)
• exists_basis : ∃ (b : Module.Basis (Fin 2) K (Fin 2 → K)) (ϖ : ↥R) (hϖ : Irreducible ϖ), Forall (fun (x : BruhatTits.Lattice R × ℕ) => match x with | (L, n) => L = (b.ntwist₂ hϖ (l.length - n - 1) 0).toLattice) l.zipIdx

@[implicit_reducible]

noncomputable instance BruhatTits.instSMulGeneralLinearGroupFinOfNatNatListLattice {K : Type u_1} [Field K] {R : Subring K} : SMul (GL (Fin 2) K) (List (Lattice R))

Equations

• BruhatTits.instSMulGeneralLinearGroupFinOfNatNatListLattice = { smul := fun (g : GL (Fin 2) K) (l : List (BruhatTits.Lattice R)) => List.map (fun (L : BruhatTits.Lattice R) => g • L) l }

theorem List.smul_lattice_def {K : Type u_1} [Field K] {R : Subring K} (g : GL (Fin 2) K) (l : List (BruhatTits.Lattice R)) : g • l = map (fun (L : BruhatTits.Lattice R) => g • L) l

@[simp]

theorem List.smul_lattice_length {K : Type u_1} [Field K] {R : Subring K} (g : GL (Fin 2) K) (l : List (BruhatTits.Lattice R)) : (g • l).length = l.length

theorem BruhatTits.smul_isSimilar_iff {K : Type u_1} [Field K] {R : Subring K} (g : GL (Fin 2) K) (M L : Lattice R) : Lattice.IsSimilar R (g • M) (g • L) ↔ Lattice.IsSimilar R M L

GL₂(K) preserves IsSimilar.

theorem BruhatTits.smul_isChain {K : Type u_1} [Field K] {R : Subring K} (g : GL (Fin 2) K) {l : List (Lattice R)} (hl : l.IsBTSimpleChain) : (g • l).IsBTSimpleChain

GL₂(K) preserves IsBTSimpleChain.

theorem BruhatTits.length_eq_dist_add_one_of_isStandard {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {l : List (Lattice R)} (hl : l.IsBTStandard) : l.length = dist (l.head ⋯) (l.getLast ⋯) + 1

If L₀, ..., Lₙ is a standard chain of length n + 1, dist L₀ Lₙ = n.

Transformation of a simple chain to a standard chain

In this section we show that every simple chain can be transformed under GL₂(K) to a standard chain. This is done by induction on the length of the chain.

theorem BruhatTits.exists_trafo_step_one {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M : Lattice R) (b : Module.Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (h1 : M.M < b.toSubmodule) (h2 : ϖ • b.toSubmodule < M.M) : ∃ (g : GL (Fin 2) K), g • M = (b.ntwist₂ hϖ 1 0).toLattice ∧ g • b.toLattice = b.toLattice

If M is a lattice, b = (b₁, b₂) a basis of K^2 and M is a standard neighbour of b.toLattice, there exists g : GL₂(K) preserving b.toLattice and transforming M into the span of (ϖ • b₁, b₂).

theorem BruhatTits.IsStandardNeighbour.exists_unipotent_smul_eq_ntwist₂ {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {ϖ : ↥R} (hϖ : Irreducible ϖ) (n : ℕ) (M : Lattice R) (b : Module.Basis (Fin 2) K (Fin 2 → K)) (h : IsStandardNeighbour M (b.ntwist₂ hϖ (n + 1) 0).toLattice) (hne : ϖ • (b.ntwist₂ hϖ n 0).toSubmodule ≠ M.M) : ∃ (x : ↥R), b.unipotent (ϖ ^ (n + 1) * x) • M = (b.ntwist₂ hϖ (n + 2) 0).toLattice

Core of induction step in Lattice.exists_GL_smul_eq_ntwist₂_of_isSimpleChain_cons:

If M is a lattice and b a basis of K^2 such that

• M is a standard neighbour of the lattice spanned by (ϖ ^ (n + 1) • b₁, b₂), and
• M is not equal to the lattice spanned by (ϖ ^ n • b₁, b₂), then there exists a unipotent matrix transforming M to (ϖ ^ (n + 2) • b₁, b₂).

In more geometric terms, when we later apply this to a walk in the Bruhat-Tits graph, the second condition requires the walk to not backtrack, i.e. to be a trail.

theorem BruhatTits.Lattice.exists_GL_smul_eq_ntwist₂_of_isSimpleChain_cons {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (l : List (Lattice R)) (hlen : 2 ≤ l.length) (M : Lattice R) (hMl : (M :: l).IsBTSimpleChain) (b : Module.Basis (Fin 2) K (Fin 2 → K)) (ϖ : ↥R) (hϖ : Irreducible ϖ) (hl : List.Forall (fun (x : Lattice R × ℕ) => match x with | (L, n) => L = (b.ntwist₂ hϖ (l.length - n - 1) 0).toLattice) l.zipIdx) : ∃ (x : ↥R), b.unipotent (ϖ ^ (l.length - 1) * x) • M = (b.ntwist₂ hϖ l.length 0).toLattice

Core of lemma 2.2 in Casselman: If M :: l is a simple chain of lattices and b a basis of K^2 such that l is a standard chain defined by b, then there exists x : R such that the upper unipotent matrix defined by x transforms M into the lattice spanned by (ϖ ^ (l.length - 1) • b₁, b₂).

We don't yet show that this transformation does not change the entries in l, see Lattice.exists_forall_GL_smul_eq_ntwist₂_of_isSimpleChain_cons for the full result.

Implementation detail: We require that the n-th entry of l equals the lattice generated by (ϖ ^ (l.length - n - 1) • b₁, b₂) and not (ϖ ^ n • b₁, b₂), because it is easier to work with M :: l than with l ++ [M].

theorem BruhatTits.Lattice.exists_GL_forall_smul_eq_ntwist₂_of_isSimpleChain_cons {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (l : List (Lattice R)) (M : Lattice R) (hMl : (M :: l).IsBTSimpleChain) (b : Module.Basis (Fin 2) K (Fin 2 → K)) (ϖ : ↥R) (hϖ : Irreducible ϖ) (hl : List.Forall (fun (x : Lattice R × ℕ) => match x with | (L, n) => L = (b.ntwist₂ hϖ (l.length - n - 1) 0).toLattice) l.zipIdx) : ∃ (g : GL (Fin 2) K), List.Forall (fun (x : Lattice R × ℕ) => match x with | (L, n) => g • L = (b.ntwist₂ hϖ (l.length - n) 0).toLattice) (M :: l).zipIdx

Lemma 2.2 in Casselman and the induction step of exists_trafo_to_isStandard (used via: IsBTSimpleChain.exists_GL_forall_smul):

If M :: l is a simple chain of lattices and b a basis of K^2 such that l is a standard chain defined by b, then there exists g : GL₂(K) such that g • M :: g • l is a standard chain defined by b.

Implementation detail: We require that the n-th entry of l equals the lattice generated by (ϖ ^ (l.length - n - 1) • b₁, b₂) and not (ϖ ^ n • b₁, b₂), because it is easier to work with M :: l than with l ++ [M].

theorem List.IsBTSimpleChain.exists_GL_forall_smul {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (l : List (BruhatTits.Lattice R)) (hl : l.IsBTSimpleChain) : ∃ (g : GL (Fin 2) K) (b : Module.Basis (Fin 2) K (Fin 2 → K)) (ϖ : ↥R) (hϖ : Irreducible ϖ), Forall (fun (x : BruhatTits.Lattice R × ℕ) => match x with | (L, n) => g • L = (b.ntwist₂ hϖ (l.length - n - 1) 0).toLattice) l.zipIdx

(Implementation detail) Intermediate lemma for exists_trafo_to_isStandard, more adapted to induction.

theorem BruhatTits.exists_trafo_to_isStandard {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (l : List (Lattice R)) (hl : l.IsBTSimpleChain) : ∃ (g : GL (Fin 2) K), (g • l).IsBTStandard

Any simple chain of lattices can be transformed by an element of GL₂(K) to a standard chain, i.e. up to a change of coordinates is every simple chain a standard chain. This is later used to show acyclicity of the Bruhat-Tits graph.

Prop. 2.1 in Casselman.