Stabilizer of a line in PSL(n, F)

This file contains key constructions to prove that PSL(n, F) is simple via showing it has an Iwasawa structure.

Main definitions

• Matrix.SpecialLinearGroup.lineStab : the unipotent radical attached to a subspace L ⊆ ι → F defined as the subgroup of SL ι F consisting of matrices A such that A - 1 sends every vector into L.

• PSL.iwasawaT : the candidate family of subgroups for the Iwasawa structure on PSL ι F acting on the projective space ℙ F (ι → F) from Matrix.SpecialLinearGroup.lineStab.

def Matrix.SpecialLinearGroup.lineStab {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (L : Submodule F (ι → F)) : Subgroup (SpecialLinearGroup ι F)

The "unipotent radical" attached to a subspace L ⊆ ι → F: the subgroup of SL ι F consisting of matrices A such that A - 1 sends every vector into L. When L is one-dimensional this is an abelian subgroup of the stabilizer of L in SL.

Equations

• Matrix.SpecialLinearGroup.lineStab L = { carrier := {A : Matrix.SpecialLinearGroup ι F | ∀ (w : ι → F), A • w - w ∈ L}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem Matrix.SpecialLinearGroup.mem_lineStab_iff {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (A : SpecialLinearGroup ι F) (L : Submodule F (ι → F)) : A ∈ lineStab L ↔ ∀ (w : ι → F), A • w - w ∈ L

@[reducible, inline]

noncomputable abbrev PSL.iwasawaT {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (p : Projectivization F (ι → F)) : Subgroup (Matrix.ProjectiveSpecialLinearGroup ι F)

The candidate family of subgroups for the Iwasawa structure on PSL ι F acting on the projective space ℙ F (ι → F): the unipotent radical attached to the line through p.

Equations

• PSL.iwasawaT p = Subgroup.map (QuotientGroup.mk' (Subgroup.center (Matrix.SpecialLinearGroup ι F))) (Matrix.SpecialLinearGroup.lineStab p.submodule)

theorem PSL.smul_submodule {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (g : Matrix.SpecialLinearGroup ι F) (p : Projectivization F (ι → F)) : (g • p).submodule = g • p.submodule

theorem Matrix.SpecialLinearGroup.lineStab_smul {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (g : SpecialLinearGroup ι F) (L : Submodule F (ι → F)) : lineStab (g • L) = MulAut.conj g • lineStab L

Equivariance of lineStab under conjugation by elements of SL.

theorem PSL.iwasawaT_map_conj {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (g : Matrix.SpecialLinearGroup ι F) (H : Subgroup (Matrix.SpecialLinearGroup ι F)) : Subgroup.map (QuotientGroup.mk' (Subgroup.center (Matrix.SpecialLinearGroup ι F))) (MulAut.conj g • H) = MulAut.conj ↑g • Subgroup.map (QuotientGroup.mk' (Subgroup.center (Matrix.SpecialLinearGroup ι F))) H

The SL-level equivariance pushed through the quotient: the image in PSL of the conjugate MulAut.conj g_SL • H equals MulAut.conj (mk g_SL) • (image of H).

theorem Matrix.SpecialLinearGroup.lineStab_fix_of_span {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (v : ι → F) (hv : v ≠ 0) (A : SpecialLinearGroup ι F) (hA : A ∈ lineStab (F ∙ v)) : A • v = v

theorem Matrix.SpecialLinearGroup.lineStab_isMulCommutative_of_span' {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (v : ι → F) (hv : v ≠ 0) (A B : SpecialLinearGroup ι F) (hA : A ∈ lineStab (F ∙ v)) (hB : B ∈ lineStab (F ∙ v)) : A * B = B * A

The subgroup lineStab (span F {v}) is commutative when v ≠ 0.

theorem Matrix.SpecialLinearGroup.lineStab_isMulCommutative_of_span {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (v : ι → F) (hv : v ≠ 0) : IsMulCommutative ↥(lineStab (F ∙ v))