Simplicity of the projective special linear groups

Let F be a field and ι a finite type with at least two elements. The projective special linear group PSL ι F = SL ι F ⧸ Z(SL ι F) acts faithfully and primitively on the projective space ℙ F (ι → F). For a line p, the subgroup lineStab p of SL ι F of matrices A with A v - v ∈ p for every vector v is commutative, and these subgroups are permuted by conjugation exactly as the lines are permuted by SL ι F. Every elementary transvection xᵢⱼ(c) lies in the subgroup of the coordinate line through eᵢ, and transvections generate SL ι F, so their images form an Iwasawa structure on the action of PSL ι F. Iwasawa's criterion MulAction.IwasawaStructure.isSimpleGroup then shows that PSL ι F is simple as soon as it is perfect, which holds when SL ι F is.

SL ι F is perfect on at least three coordinates over every field, and on two coordinates when F has a nonzero element whose square is not one, in particular when F has at least four elements. This gives the simplicity of PSL_n(F) in all the classical cases: every n ≥ 3, and n = 2 outside F = 𝔽₂, 𝔽₃.

Mathlib proves the case of Fin 2 coordinates (Matrix.ProjectiveSpecialLinearGroup.rank_two_simple, with the Iwasawa structure PSL2.Iwasawa). Its commutativity and conjugation arguments apply verbatim to every coordinate type and are reused here, while the generation step is the general generation of SL ι F by transvections.

Main definitions

• Matrix.ProjectiveSpecialLinearGroup.iwasawaStructure: the Iwasawa structure of the action of PSL ι F on ℙ F (ι → F).

Main results

• Matrix.SpecialLinearGroup.iSup_lineStab_eq_top: the subgroups lineStab p generate SL ι F.
• Matrix.ProjectiveSpecialLinearGroup.isSimpleGroup_of_commutator_eq_top: PSL ι F is simple when SL ι F is perfect.
• Matrix.ProjectiveSpecialLinearGroup.isSimpleGroup_of_three_le_card: PSL ι F is simple on at least three coordinates.
• Matrix.ProjectiveSpecialLinearGroup.isSimpleGroup_of_sq_ne_one and Matrix.ProjectiveSpecialLinearGroup.isSimpleGroup_of_four_le_natCard: PSL ι F is simple on at least two coordinates over a field with a nonzero element whose square is not one, for example a field with at least four elements.

References

• K. Iwasawa, Über die Einfachheit der speziellen projektiven Gruppen, Proc. Imp. Acad. Tokyo 17 (1941), 57–59.
• E. Artin, Geometric Algebra, Interscience (1957), Chapter IV, Theorem 4.10.

theorem Matrix.SpecialLinearGroup.iSup_lineStab_eq_top {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] : ⨆ (p : Projectivization F (ι → F)), lineStab p.submodule = ⊤

The subgroups lineStab p generate the special linear group. Each transvection xᵢⱼ(c) lies in the subgroup of the coordinate line through eᵢ, and transvections generate SL ι F. This extends Mathlib's PSL.iSup_lineStab_eq_top from Fin 2 to every finite coordinate type.

theorem Matrix.ProjectiveSpecialLinearGroup.iSup_iwasawaT_eq_top {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] : iSup PSL.iwasawaT = ⊤

The images in PSL ι F of the subgroups lineStab p generate PSL ι F.

noncomputable def Matrix.ProjectiveSpecialLinearGroup.iwasawaStructure {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] : MulAction.IwasawaStructure (ProjectiveSpecialLinearGroup ι F) (Projectivization F (ι → F))

The Iwasawa structure of PSL ι F acting on ℙ F (ι → F). The subgroup attached to a line p is the image of lineStab p; these subgroups are commutative, permuted by conjugation as the lines are permuted, and generate PSL ι F. This extends Mathlib's PSL2.Iwasawa from Fin 2 to every finite coordinate type.

@[simp]

theorem Matrix.ProjectiveSpecialLinearGroup.iwasawaStructure_T {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] (p : Projectivization F (ι → F)) : iwasawaStructure.T p = PSL.iwasawaT p

The subgroup that iwasawaStructure attaches to a line p is the image of lineStab p.

theorem Matrix.ProjectiveSpecialLinearGroup.isSimpleGroup_of_commutator_eq_top {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Nontrivial ι] (h : commutator (SpecialLinearGroup ι F) = ⊤) : IsSimpleGroup (ProjectiveSpecialLinearGroup ι F)

Iwasawa's theorem for PSL. On at least two coordinates, the projective special linear group is simple as soon as the special linear group is perfect.

theorem Matrix.ProjectiveSpecialLinearGroup.isSimpleGroup_of_three_le_card {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] (h : 3 ≤ Fintype.card ι) : IsSimpleGroup (ProjectiveSpecialLinearGroup ι F)

PSL_n(F) is simple for n ≥ 3, over every field.

theorem Matrix.ProjectiveSpecialLinearGroup.isSimpleGroup_of_sq_ne_one {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Nontrivial ι] {a : F} (ha : a ≠ 0) (hasq : a ^ 2 ≠ 1) : IsSimpleGroup (ProjectiveSpecialLinearGroup ι F)

PSL_n(F) is simple for n ≥ 2 over a field with a nonzero element whose square is not one. This extends Mathlib's Matrix.ProjectiveSpecialLinearGroup.rank_two_simple' from Fin 2 to every finite coordinate type with at least two elements.

theorem Matrix.ProjectiveSpecialLinearGroup.isSimpleGroup_of_four_le_natCard {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Nontrivial ι] (hF : 4 ≤ Nat.card F) : IsSimpleGroup (ProjectiveSpecialLinearGroup ι F)

PSL_n(F) is simple for n ≥ 2 over a field with at least four elements. This extends Mathlib's Matrix.ProjectiveSpecialLinearGroup.rank_two_simple from Fin 2 to every finite coordinate type with at least two elements.