Perfectness of special linear groups

Over a field containing a nonzero element whose square is not one, the special linear group on any finite coordinate type is perfect. Conjugation by the determinant-one diagonal matrix with entries a and a⁻¹ rescales a transvection by a². Every transvection is consequently a commutator, and transvections generate the special linear group. The hypothesis holds over every infinite field and every finite field with at least four elements; it excludes the small-field exceptions in rank two.

On three or more coordinates no hypothesis on the field is needed: for distinct i, k, j the type-A commutator relation ⁅xᵢₖ(c), xₖⱼ(1)⁆ = xᵢⱼ(c) exhibits every transvection as a commutator, so the special linear group is perfect over every field.

The commutator calculation generalizes Mathlib's Matrix.commutator_diag2_transvection and the perfectness statement generalizes Matrix.SL2.commutator_eq_top to arbitrary finite coordinate types. Generation is reused from Matrix.SpecialLinearGroup.closure_range_toSpecialLinearGroup_eq_top_of_field.

Main results

• Matrix.SpecialLinearGroup.commutator_eq_top: perfectness over a field containing a nonzero element whose square is not one.
• Matrix.SpecialLinearGroup.commutator_eq_top_of_four_le_natCard: perfectness over a field with at least four elements.
• Matrix.SpecialLinearGroup.commutator_eq_top_of_three_le_card: perfectness on at least three coordinates over every field.

References

• J. S. Milne, Algebraic Groups (2017), §6d.

theorem Matrix.SpecialLinearGroup.commutatorElement_diag2n_transvection {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {i j : ι} (hij : i ≠ j) (a : F) (ha : a ≠ 0) (b : F) : ⁅diag2n hij a ha, transvection hij b⁆ = transvection hij (b * (a ^ 2 - 1))

Conjugation by the determinant-one two-coordinate diagonal matrix rescales a transvection by a², so its commutator has parameter b * (a² - 1).

theorem Matrix.SpecialLinearGroup.transvection_mem_commutator {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {i j : ι} (hij : i ≠ j) {a : F} (ha : a ≠ 0) (hasq : a ^ 2 ≠ 1) (c : F) : transvection hij c ∈ commutator (SpecialLinearGroup ι F)

Every transvection is in the commutator subgroup if the field contains a nonzero element whose square is not one.

theorem Matrix.SpecialLinearGroup.commutator_eq_top {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {a : F} (ha : a ≠ 0) (hasq : a ^ 2 ≠ 1) : commutator (SpecialLinearGroup ι F) = ⊤

The special linear group over a field with a nonzero element whose square is not one is perfect, in every finite rank, including ranks zero and one.

theorem Matrix.SpecialLinearGroup.commutator_eq_top_of_four_le_natCard {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] (hF : 4 ≤ Nat.card F) : commutator (SpecialLinearGroup ι F) = ⊤

The special linear group over a field with at least four elements is perfect, in every finite rank.

theorem Matrix.SpecialLinearGroup.transvection_mem_commutator_of_ne {ι : Type u_2} [Fintype ι] [DecidableEq ι] {i j : ι} {A : Type u_3} [CommRing A] {k : ι} (hij : i ≠ j) (hik : i ≠ k) (hkj : k ≠ j) (c : A) : transvection hij c ∈ commutator (SpecialLinearGroup ι A)

A transvection xᵢⱼ(c) is a commutator as soon as a third index k is available: it is ⁅xᵢₖ(c), xₖⱼ(1)⁆.

theorem Matrix.SpecialLinearGroup.commutator_eq_top_of_three_le_card {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] (h : 3 ≤ Fintype.card ι) : commutator (SpecialLinearGroup ι F) = ⊤

The special linear group on at least three coordinates is perfect over every field.