Definition of vertices

In this file we define the type of vertices of the Bruhat-Tits tree. A vertex is an equivalence class of R-lattices with respect to homothety.

The distance of lattices is invariant under homothety (see BruhatTits.dist_inv_isSimilar), hence the distance function descends to vertices which is called BruhatTits.inv. This is later used to define the edge relations on the Bruhat-Tits graph (see BruhatTits.Graph.Edges).

Main definitions and results

• BruhatTits.inv: the distance between vertices defined as the distance between lattice representatives.
• BruhatTits.exists_repr_inv': given two vertices x and y, there exists a basis b of Fin 2 → K such that x = ⟦b.toLattice⟧ and y = ⟦(b.ntwist₂ (inv x y) 0).toLattice⟧`.
• BruhatTits.exists_intermediate_vertex: Given two vertices x and y of distance n + 1, there exists a vertex z such that inv x z = n and inv z y = 1. This will later be used to deduce that the Bruhat-Tits graph is connected.

def BruhatTits.Vertices {K : Type u_1} [Field K] (R : Subring K) : Type u_1

The vertices of the Bruhat-Tits tree are R-lattices modulo the equivalence relation IsSimilar.

Equations

• BruhatTits.Vertices R = Quotient (BruhatTits.Lattice.IsSimilar.setoid R)

@[reducible, inline]

abbrev BruhatTits.Vertices.mk {K : Type u_1} [Field K] {R : Subring K} (L : Lattice R) : Vertices R

An abbreviation for Quotient.mk for vertices. We only use this it the additional type information is needed.

Equations

• BruhatTits.Vertices.mk L = ⟦L⟧

noncomputable def BruhatTits.inv {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L M : Vertices R) : ℕ

The distance of vertices defined as the distance of representatives. This is well-defined by BruhatTits.dist_inv_isSimilar.

Equations

• BruhatTits.inv L M = Quotient.lift₂ BruhatTits.dist ⋯ L M

@[simp]

theorem BruhatTits.inv_mk {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L M : Lattice R) : inv (Quotient.mk'' L) (Quotient.mk'' M) = dist L M

theorem BruhatTits.inv_symm {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L M : Vertices R) : inv L M = inv M L

theorem BruhatTits.inv_self {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L : Vertices R) : inv L L = 0

theorem BruhatTits.exists_repr_inv_of_fixed {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M : Lattice R) (y : Vertices R) : ∃ (ϖ : ↥R) (_ : Irreducible ϖ) (L : Lattice R) (bM : Module.Basis (Fin 2) ↥R ↥M.M) (bL : Module.Basis (Fin 2) ↥R ↥L.M), ⟦L⟧ = y ∧ ↑(bL 0) = ϖ ^ inv ⟦M⟧ y • ↑(bM 0) ∧ ↑(bL 1) = ↑(bM 1)

Variant of exists_repr_inv where the first vertex has a fixed representative.

theorem BruhatTits.exists_repr_inv {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (x y : Vertices R) : ∃ (ϖ : ↥R) (_ : Irreducible ϖ) (M : Lattice R) (L : Lattice R) (bM : Module.Basis (Fin 2) ↥R ↥M.M) (bL : Module.Basis (Fin 2) ↥R ↥L.M), ⟦M⟧ = x ∧ ⟦L⟧ = y ∧ ↑(bL 0) = ϖ ^ inv x y • ↑(bM 0) ∧ ↑(bL 1) = ↑(bM 1)

Given vertices x and y, there exist representatives M and L and a basis bM of M such that (ϖ ^ (inv x y) • (bM 0), bM 1) is a basis of L.

theorem BruhatTits.exists_repr_dist' {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Lattice R) : ∃ (ϖ : ↥R) (hϖ : Irreducible ϖ) (b : Module.Basis (Fin 2) K (Fin 2 → K)) (f : Fin 2 → ℤ) (_ : Antitone f), M = b.toLattice ∧ L = (b.twist hϖ f).toLattice ∧ f 0 - f 1 = ↑(dist M L)

Variant of exists_repr_dist in terms of Basis.twist.

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

Variant of exists_repr_inv_of_fixed in terms of Basis.ntwist₂.

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

Variant of exists_repr_inv in terms of Basis.ntwist₂.

theorem BruhatTits.dist_twist {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Module.Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) {f : Fin 2 → ℤ} (hf : Antitone f) : ↑(dist b.toLattice (b.twist hϖ f).toLattice) = f 0 - f 1

If b is a basis of Fin 2 → K and f₀ ≥ f₁, the distance of b.toLattice and (b.twist hϖ f).toLattice is f₀ - f₁.

theorem BruhatTits.dist_twist_monotone {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Module.Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) {f : Fin 2 → ℤ} (hf : Monotone f) : ↑(dist b.toLattice (b.twist hϖ f).toLattice) = f 1 - f 0

If b is a basis of Fin 2 → K and f₀ ≤ f₁, the distance of b.toLattice and (b.twist hϖ f).toLattice is f₁ - f₀.

@[simp]

theorem BruhatTits.dist_smul_GL_eq_dist {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Lattice R) (g : GL (Fin 2) K) : dist (g • M) (g • L) = dist M L

theorem BruhatTits.dist_twist₂ {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Module.Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (n m : ℤ) : ↑(dist b.toLattice (b.twist₂ hϖ n m).toLattice) = |n - m|

theorem BruhatTits.dist_ntwist₂ {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Module.Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (n : ℕ) : dist b.toLattice (b.ntwist₂ hϖ n 0).toLattice = n

theorem BruhatTits.exists_intermediate_vertex {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (n : ℕ) (x y : Vertices R) (h : inv x y = n + 1) : ∃ (o : Vertices R), inv y o = n ∧ inv o x = 1

If vertices x and y have distance n + 1, there exists a vertex o with inv o x = 1 and inv y o = n. This is the inductive step for showing that the Bruhat-Tits graph is connected (see BruhatTits.reachable).

theorem BruhatTits.isSimilar_of_dist_eq_zero {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {M L : Lattice R} (h : dist M L = 0) : Lattice.IsSimilar R M L

If two lattices have distance zero, they are equal up to a unit.

theorem BruhatTits.eq_iff {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Vertices R) : M = L ↔ inv M L = 0

Two vertices are equal if and only if their distance is zero.