Proof that the Bruhat-Tits tree is regular

Let R be a discrete valuation ring. Assume that the residue field k = R ⧸ 𝓂 R of R is finite.

In this file we show that the Bruhat-Tits tree associated to R is regular, i.e. that every vertex has the same finite number of neighbours. Furthermore we show that this number is #k+1.

Main result

• BruhatTits.btgraph_regular : The Bruhat-Tits Tree is q + 1-regular, where q is the cardinality of R ⧸ 𝓂 R.

noncomputable def BruhatTits.standardNeighbourBasis {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {L : Lattice R} {y : Vertices R} (h : IsNeighbour y ⟦L⟧) : Module.Basis (Fin 2) K (Fin 2 → K)

A basis putting a neighbour of L into standard form.

Equations

• BruhatTits.standardNeighbourBasis h = ⋯.choose

@[simp]

theorem BruhatTits.standardNeighbourBasis_toLattice_Eq {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {L : Lattice R} {y : Vertices R} (h : IsNeighbour y ⟦L⟧) : (standardNeighbourBasis h).toLattice = L

noncomputable def BruhatTits.standardNeighbourϖ {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {L : Lattice R} {y : Vertices R} (h : IsNeighbour y ⟦L⟧) : ↥R

The uniformizer used in the standard representative of a neighbour.

Equations

• BruhatTits.standardNeighbourϖ h = ⋯.choose

theorem BruhatTits.standardNeighbourϖ_irreducible {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {L : Lattice R} {y : Vertices R} (h : IsNeighbour y ⟦L⟧) : Irreducible (standardNeighbourϖ h)

noncomputable def BruhatTits.standardNeighbour {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {L : Lattice R} {y : Vertices R} (h : IsNeighbour y ⟦L⟧) : Lattice R

The standard lattice representative of a neighbour of L.

Equations

• BruhatTits.standardNeighbour h = ((BruhatTits.standardNeighbourBasis h).ntwist₂ ⋯ 1 0).toLattice

@[simp]

theorem BruhatTits.standardNeighbourBasis_ntwist_eq {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {L : Lattice R} {y : Vertices R} (h : IsNeighbour y ⟦L⟧) : ((standardNeighbourBasis h).ntwist₂ ⋯ 1 0).toLattice = standardNeighbour h

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

@[simp]

theorem BruhatTits.standardNeighbour_mk_eq {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {L : Lattice R} {y : Vertices R} (h : IsNeighbour y ⟦L⟧) : ⟦standardNeighbour h⟧ = y

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

theorem BruhatTits.eq_standardNeighbour_of_isStandardNeighbour {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {L : Lattice R} {y : Vertices R} (h : IsNeighbour y ⟦L⟧) (M : Lattice R) (hM : ⟦M⟧ = y) (hML : IsStandardNeighbour M L) : M = standardNeighbour h

noncomputable def BruhatTits.neighborsEquivStandardNeighbors {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L : Lattice R) : ↑{y : Vertices R | IsNeighbour y ⟦L⟧} ≃ ↑{M : Lattice R | IsStandardNeighbour M L}

The neighbours of ⟦L⟧ are in one to one correspondence to standard neighbours of L.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BruhatTits.Lattice.quotientRestrictScalarsEquiv {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L : Lattice R) : Submodule (IsLocalRing.ResidueField ↥R) L.quotient ≃o Submodule (↥R) L.quotient

Restrict scalars from the residue field quotient to an R-submodule.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible, instance 99999]

noncomputable instance BruhatTits.instSMulIdealSubtypeMemSubringSubmoduleForallFinOfNatNatM {K : Type u_1} [Field K] {R : Subring K} (L : Lattice R) : SMul (Ideal ↥R) (Submodule ↥R ↥L.M)

Equations

• BruhatTits.instSMulIdealSubtypeMemSubringSubmoduleForallFinOfNatNatM L = Submodule.instSMul

noncomputable def BruhatTits.Lattice.submoduleRestrictQuotientEquiv {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L : Lattice R) : Submodule (↥R) L.quotient ≃o { M : Submodule ↥R ↥L.M // IsLocalRing.maximalIdeal ↥R • ⊤ ≤ M }

Relate quotient submodules to submodules of the lattice containing the maximal ideal multiple.

Equations

• L.submoduleRestrictQuotientEquiv = (IsLocalRing.maximalIdeal ↥R • ⊤).comapMkQRelIso

noncomputable def BruhatTits.Lattice.submoduleQuotientEquiv {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L : Lattice R) : Submodule (IsLocalRing.ResidueField ↥R) L.quotient ≃o { M : Submodule ↥R ↥L.M // IsLocalRing.maximalIdeal ↥R • ⊤ ≤ M }

Relate residue-field subspaces of the quotient to intermediate R-submodules of the lattice.

Equations

• L.submoduleQuotientEquiv = L.quotientRestrictScalarsEquiv.trans L.submoduleRestrictQuotientEquiv

theorem BruhatTits.submodule_ne_top_of_finrank {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {L : Lattice R} {M : Submodule (IsLocalRing.ResidueField ↥R) L.quotient} (h : Module.finrank (IsLocalRing.ResidueField ↥R) ↥M = 1) : M ≠ ⊤

theorem BruhatTits.submodule_ne_bot_of_finrank {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] {L : Lattice R} {M : Submodule (IsLocalRing.ResidueField ↥R) L.quotient} (h : Module.finrank (IsLocalRing.ResidueField ↥R) ↥M = 1) : M ≠ ⊥

theorem BruhatTits.submodule_finrank_eq_one_of_ne_bot_of_ne_top {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {L : Lattice R} {M : Submodule (IsLocalRing.ResidueField ↥R) L.quotient} (h₁ : M ≠ ⊥) (h₂ : M ≠ ⊤) : Module.finrank (IsLocalRing.ResidueField ↥R) ↥M = 1

theorem BruhatTits.submodule_finrank_eq_one_iff {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {L : Lattice R} {M : Submodule (IsLocalRing.ResidueField ↥R) L.quotient} : Module.finrank (IsLocalRing.ResidueField ↥R) ↥M = 1 ↔ M ≠ ⊥ ∧ M ≠ ⊤

noncomputable def BruhatTits.linesQuotientEquiv {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L : Lattice R) : { M : Submodule (IsLocalRing.ResidueField ↥R) L.quotient // Module.finrank (IsLocalRing.ResidueField ↥R) ↥M = 1 } ≃ { M : { M : Submodule ↥R ↥L.M // IsLocalRing.maximalIdeal ↥R • ⊤ ≤ M } // M ≠ ⊥ ∧ M ≠ ⊤ }

Lines in the residue quotient correspond to proper nonzero intermediate submodules.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BruhatTits.Lattice.standardNeighboursEquivLinesAux {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L : Lattice R) : { M : Submodule (↥R) (Fin 2 → K) // IsLocalRing.maximalIdeal ↥R • L.M < M ∧ M < L.M } ≃ { M : Lattice R // IsStandardNeighbour M L }

R-submodules of K^2 that are strictly between ϖ L and L are in one-to-one correspondence to standard neighbours of L.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BruhatTits.standardNeighboursEquivLines {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L : Lattice R) : { M : Lattice R // IsStandardNeighbour M L } ≃ { M : Submodule (IsLocalRing.ResidueField ↥R) L.quotient // Module.finrank (IsLocalRing.ResidueField ↥R) ↥M = 1 }

The standard neighbours of ⟦L⟧ are in one-to-one correspondence to one-dimensional subspaces of L ⧸ ϖ L, i.e. lines.

Equations

• BruhatTits.standardNeighboursEquivLines L = L.standardNeighboursEquivLinesAux.symm.trans ((BruhatTits.Lattice.submoduleNeAndNeEquivLtAndLt✝ L).symm.trans (BruhatTits.linesQuotientEquiv L).symm)

noncomputable def BruhatTits.neighborsEquivLines {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L : Lattice R) : { y : Vertices R // IsNeighbour y ⟦L⟧ } ≃ { M : Submodule (IsLocalRing.ResidueField ↥R) L.quotient // Module.finrank (IsLocalRing.ResidueField ↥R) ↥M = 1 }

Neighbors of a vertex ⟦L⟧ correspond to lines in L ⧸ ϖ L.

Equations

• BruhatTits.neighborsEquivLines L = (BruhatTits.neighborsEquivStandardNeighbors L).trans (BruhatTits.standardNeighboursEquivLines L)

noncomputable def BruhatTits.neighborSetEquivProjectivization {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L : Lattice R) : ↑(BTgraph.neighborSet ⟦L⟧) ≃ Projectivization (IsLocalRing.ResidueField ↥R) L.quotient

Neighbors of a vertex ⟦L⟧ correspond the projectivization of L ⧸ ϖ L.

Equations

• One or more equations did not get rendered due to their size.

instance BruhatTits.instFiniteElemVerticesNeighborSetBTgraph {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] [Finite (IsLocalRing.ResidueField ↥R)] (x : Vertices R) : Finite ↑(BTgraph.neighborSet x)

If the residue field of R is finite, every vertex has finitely many neighbors.

@[implicit_reducible]

noncomputable instance BruhatTits.instFintypeElemVerticesNeighborSetBTgraph {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] [Finite (IsLocalRing.ResidueField ↥R)] (x : Vertices R) : Fintype ↑(BTgraph.neighborSet x)

Equations

• BruhatTits.instFintypeElemVerticesNeighborSetBTgraph x = Fintype.ofFinite ↑(BruhatTits.BTgraph.neighborSet x)

theorem BruhatTits.btgraph_degree {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] [Finite (IsLocalRing.ResidueField ↥R)] (x : Vertices R) : BTgraph.degree x = Nat.card (IsLocalRing.ResidueField ↥R) + 1

The degree of the Bruhat-Tits tree is q + 1 where q is the cardinality of R ⧸ 𝓂 R.

theorem BruhatTits.btgraph_regular {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] [Finite (IsLocalRing.ResidueField ↥R)] : BTgraph.IsRegularOfDegree (Nat.card (IsLocalRing.ResidueField ↥R) + 1)

If R ⧸ 𝓂 R is finite, the Bruhat-Tits Tree is q + 1-regular, where q is the cardinality of R ⧸ 𝓂 R.