Group actions on the Bruhat-Tits graph

In this file we equip the Bruhat-Tits graph with group actions of GL₂(K) and compute stabilizers.

Main results

• MulAction.IsPretransitive (GL (Fin 2) K) (Vertices R) : We show that GL₂(K) acts transitively on the vertices.
• GraphAction (GL (Fin 2) K) (BTgraph (R:= R)) : The group GL₂(K) acts on BTgraph.
• stabilizer_mk_standard_eq_sup : The stabilizer of the standard vertex of the GL₂(K)-action is Kˣ * GL₂(R).
• stabilizer_fun_mk_ntwist₂_eq_sup_comap_upperTriangularSubgroup: The pointwise stabilizer of GL₂(K) of the segment ⟦v₀⟧ - ⟦v₁⟧ - ... - ⟦vₙ⟧ is the subgroup Kˣ * Iₙ where Iₙ is the subgroup of GL₂(R) that is upper triangular modulo ϖ ^ n.

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

def BruhatTits.smulGL {K : Type u_1} [Field K] {R : Subring K} (g : GL (Fin 2) K) : Vertices R → Vertices R

The action of GL₂(K) on vertices induced by its action on lattices.

Equations

• BruhatTits.smulGL g = Quotient.lift (fun (L : BruhatTits.Lattice R) => ⟦g • L⟧) ⋯

theorem BruhatTits.smulGL_mk {K : Type u_1} [Field K] {R : Subring K} (g : GL (Fin 2) K) (L : Lattice R) : smulGL g ⟦L⟧ = ⟦g • L⟧

@[implicit_reducible]

instance BruhatTits.instSMulGeneralLinearGroupFinOfNatNatVertices {K : Type u_1} [Field K] {R : Subring K} : SMul (GL (Fin 2) K) (Vertices R)

Equations

• BruhatTits.instSMulGeneralLinearGroupFinOfNatNatVertices = { smul := BruhatTits.smulGL }

theorem BruhatTits.Vertices.smul_def {K : Type u_1} [Field K] {R : Subring K} (g : GL (Fin 2) K) (x : Vertices R) : g • x = smulGL g x

@[implicit_reducible]

instance BruhatTits.instMulActionGeneralLinearGroupFinOfNatNatVertices {K : Type u_1} [Field K] {R : Subring K} : MulAction (GL (Fin 2) K) (Vertices R)

The action of GL₂(K) on vertices.

Equations

• BruhatTits.instMulActionGeneralLinearGroupFinOfNatNatVertices = { toSMul := BruhatTits.instSMulGeneralLinearGroupFinOfNatNatVertices, mul_smul := ⋯, one_smul := ⋯ }

instance BruhatTits.instIsPretransitiveGeneralLinearGroupFinOfNatNatVertices {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] : MulAction.IsPretransitive (GL (Fin 2) K) (Vertices R)

GL₂(K) acts transitively on the vertices.

@[simp]

theorem BruhatTits.inv_smul_smul_eq_inv {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (g : GL (Fin 2) K) (x y : Vertices R) : inv (g • x) (g • y) = inv x y

theorem BruhatTits.adj_smul_smul_iff_adj {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (g : GL (Fin 2) K) (x y : Vertices R) : BTgraph.Adj (g • x) (g • y) ↔ BTgraph.Adj x y

def Matrix.GeneralLinearGroup.toGraphIso {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (g : GL (Fin 2) K) : BruhatTits.BTgraph ≃g BruhatTits.BTgraph

GL₂(K) acts by graph isomorphisms on the Bruhat-Tits tree.

Equations

• g.toGraphIso = { toEquiv := MulAction.toPerm g, map_rel_iff' := ⋯ }

instance BruhatTits.instGraphActionVerticesGeneralLinearGroupFinOfNatNatBTgraph {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] : GraphAction (GL (Fin 2) K) BTgraph

The action of GL₂(K) on the Bruhat-Tits graph.

theorem BruhatTits.cartanDiag_smul_standard {K : Type u_1} [Field K] {R : Subring K} (ϖ : ↥R) (hϖ : Irreducible ϖ) (f : Fin 2 → ℤ) : cartanDiag ϖ hϖ f • Lattice.standard R = ((Pi.basisFun K (Fin 2)).twist hϖ f).toLattice

theorem BruhatTits.pow_smul_range_eq_range_iff {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {ι : Type u_2} [Finite ι] [Nonempty ι] {ϖ : ↥R} (hϖ : Irreducible ϖ) (n : ℤ) : ↑ϖ ^ n • Set.range ⇑((Algebra.linearMap (↥R) K).compLeft ι) = Set.range ⇑((Algebra.linearMap (↥R) K).compLeft ι) ↔ n = 0

theorem BruhatTits.stabilizer_standard_eq_range_map_subtype {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] : MulAction.stabilizer (GL (Fin 2) K) (Lattice.standard R) = (Matrix.GeneralLinearGroup.map R.subtype).range

The stabilizer of the standard lattice of the GL₂(K)-action on lattices is GL₂(R).

theorem BruhatTits.stabilizer_smul_standard_eq_map_conj_subtype_range {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (g : GL (Fin 2) K) : MulAction.stabilizer (GL (Fin 2) K) (g • Lattice.standard R) = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (Matrix.GeneralLinearGroup.map R.subtype).range

The stabilizer of any lattice g • Lattice.standard R is the conjugate g GL₂(R) g⁻¹.

theorem BruhatTits.Lattice.valuation_det_eq_one_of_mem_stabilizer {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L : Lattice R) (g : GL (Fin 2) K) (hg : g ∈ MulAction.stabilizer (GL (Fin 2) K) L) : (ValuationRing.valuation (↥R) K) ↑(Matrix.GeneralLinearGroup.det g) = 1

theorem Matrix.GL.mem_range_map_iff {R : Type u_2} {K : Type u_3} [CommRing R] [CommRing K] (f : R →+* K) (hf : Function.Injective ⇑f) {ι : Type u_4} [Fintype ι] [DecidableEq ι] (g : GL ι K) : g ∈ Set.range ⇑(GeneralLinearGroup.map f) ↔ (∀ (i j : ι), ↑g i j ∈ Set.range ⇑f) ∧ ↑(GeneralLinearGroup.det g)⁻¹ ∈ Set.range ⇑f

theorem BruhatTits.mem_stabilizer_twist_iff_mem {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {ϖ : ↥R} (hϖ : Irreducible ϖ) (g : GL (Fin 2) ↥R) (f : Fin 2 → ℤ) : «GL».map R.subtype g ∈ MulAction.stabilizer (GL (Fin 2) K) ((Pi.basisFun K (Fin 2)).twist hϖ f).toLattice ↔ ↑ϖ ^ (f 1 - f 0) * ↑(↑g 0 1) ∈ R ∧ ↑ϖ ^ (f 0 - f 1) * ↑(↑g 1 0) ∈ R

theorem BruhatTits.mem_stabilizer_twist_iff_exists {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {ϖ : ↥R} (hϖ : Irreducible ϖ) (g : GL (Fin 2) K) (f : Fin 2 → ℤ) : g ∈ MulAction.stabilizer (GL (Fin 2) K) ((Pi.basisFun K (Fin 2)).twist hϖ f).toLattice ↔ ∃ (k : GL (Fin 2) ↥R), ↑g 0 0 = ↑(↑k 0 0) ∧ ↑g 1 1 = ↑(↑k 1 1) ∧ ↑g 1 0 = ↑ϖ ^ (f 1 - f 0) * ↑(↑k 1 0) ∧ ↑g 0 1 = ↑ϖ ^ (f 0 - f 1) * ↑(↑k 0 1)

g in GL₂(K) stabilizes (ϖ ^ n • e₀, ϖ ^ m • e₁) if and only if g is of the form

      a           ϖ ^ (n - m) * b
ϖ ^ (m - n) * c         d

for some (a b, c d) in GL₂(R).

theorem BruhatTits.mem_stabilizer_ntwist₂_iff_mem_span {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {ϖ : ↥R} (hϖ : Irreducible ϖ) (n : ℕ) (g : GL (Fin 2) ↥R) : «GL».map R.subtype g ∈ MulAction.stabilizer (GL (Fin 2) K) ((Pi.basisFun K (Fin 2)).ntwist₂ hϖ 0 n).toLattice ↔ ↑g 1 0 ∈ Ideal.span {ϖ ^ n}

g in GL₂(R) is in the stabilizer of (e₀, ϖ ^ n • e₁) if and only if g 1 0 ≡ 0 (mod ϖ ^ n).

theorem BruhatTits.stabilizer_fun_ntwist₂_eq_sup_comap_upperTriangularSubgroup {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {ϖ : ↥R} (hϖ : Irreducible ϖ) (n : ℕ) : (MulAction.stabilizer (GL (Fin 2) K) fun (k : Fin (n + 1)) => ((Pi.basisFun K (Fin 2)).ntwist₂ hϖ 0 ↑k).toLattice) = Subgroup.map (Matrix.GeneralLinearGroup.map R.subtype) (Subgroup.comap (Matrix.GeneralLinearGroup.map (Ideal.Quotient.mk (Ideal.span {ϖ ^ n}))) (Matrix.GeneralLinearGroup.upperTriangularSubgroup (↥R ⧸ Ideal.span {ϖ ^ n}) (Fin 2)))

The pointwise stabilizer of the chain of lattices L₀ - L₁ - ... - Lₙ where Lᵢ = (e₀, ϖ ^ n • eᵢ) is the subgroup of matrices in GL₂(R) that are upper triangular modulo ϖ ^ n. We express the stabilizer of the chain as the stabilizer of the function i ↦ Lᵢ. Here GL₂(K) acts pointwise on pi types.

theorem BruhatTits.stabilizer_fun_mk_eq_sup {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {ι : Type u_2} (L : ι → Lattice R) : (MulAction.stabilizer (GL (Fin 2) K) fun (i : ι) => Vertices.mk (L i)) = (Matrix.GeneralLinearGroup.embDiagonal K (Fin 2)).range ⊔ MulAction.stabilizer (GL (Fin 2) K) L

The pointwise stabilizer of the GL₂(K)-action on a family of vertices {⟦Lᵢ⟧}ᵢ is Kˣ * Stab({Lᵢ}). We express the stabilizer of {⟦Lᵢ⟧}ᵢ as the stabilizer of the function i ↦ ⟦Lᵢ⟧. Here GL₂(K) acts pointwise on pi types.

theorem BruhatTits.stabilizer_mk_eq_sup {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L : Lattice R) : MulAction.stabilizer (GL (Fin 2) K) (Vertices.mk L) = (Matrix.GeneralLinearGroup.embDiagonal K (Fin 2)).range ⊔ MulAction.stabilizer (GL (Fin 2) K) L

The stabilizer of the GL₂(K)-action on a vertex ⟦L⟧ is Kˣ * Stab(L).

theorem BruhatTits.stabilizer_mk_standard_eq_sup {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] : MulAction.stabilizer (GL (Fin 2) K) (Vertices.mk (Lattice.standard R)) = (Matrix.GeneralLinearGroup.embDiagonal K (Fin 2)).range ⊔ (Matrix.GeneralLinearGroup.map R.subtype).range

The stabilizer of the GL₂(K)-action on the standard vertex is Kˣ * GL₂(R).

theorem BruhatTits.stabilizer_fun_mk_ntwist₂_eq_sup_comap_upperTriangularSubgroup {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {ϖ : ↥R} (hϖ : Irreducible ϖ) (n : ℕ) : (MulAction.stabilizer (GL (Fin 2) K) fun (k : Fin (n + 1)) => Vertices.mk ((Pi.basisFun K (Fin 2)).ntwist₂ hϖ 0 ↑k).toLattice) = (Matrix.GeneralLinearGroup.embDiagonal K (Fin 2)).range ⊔ Subgroup.map (Matrix.GeneralLinearGroup.map R.subtype) (Subgroup.comap (Matrix.GeneralLinearGroup.map (Ideal.Quotient.mk (Ideal.span {ϖ ^ n}))) (Matrix.GeneralLinearGroup.upperTriangularSubgroup (↥R ⧸ Ideal.span {ϖ ^ n}) (Fin 2)))

The pointwise stabilizer of GL₂(K) of the segment v₀ - v₁ - ... - vₙ is the subgroup Kˣ * Iₙ where Iₙ is the subgroup of GL₂(R) that is upper triangular modulo ϖ ^ n. Here the vertex vᵢ is the image of the lattice (e₀, ϖ ^ i • e₁). In particular, this shows that the stabilizer of the edge v₀ - v₁ is Kˣ * I₁.