Special linear groups generated by transvections

Every element of SL_n(ℤ) is a product of elementary transvection matrices I + c·e_{ij}. The proof is the Euclidean algorithm on the first column: transvection row operations shrink the column to a single unit entry, two or three further transvections move that unit to the (0, 0) corner as +1, row operations clear the first row, and the lower-right block is handled by induction on the dimension.

Mathlib's Mathlib.LinearAlgebra.Transvection.Generation proves the Dieudonné generation theorem over division rings; ℤ is not covered there, and the argument here is the integer-specific one. Transvections are carried as Matrix.TransvectionStruct data, the vocabulary of Mathlib's transvection theory; all of the Euclidean machinery is private.

Over a field, Mathlib's diagonal--transvection induction and the arbitrary-index form of its diag2_decompose factorization give the parallel generation theorem.

The file also records the type-A relations for bare Matrix.transvection matrices and their determinant-one counterparts over an arbitrary commutative ring.

Main results

• Matrix.SpecialLinearGroup.exists_list_transvec_prod: every σ ∈ SL_n(ℤ) is the product of a list of transvections.
• Matrix.SpecialLinearGroup.closure_range_toSpecialLinearGroup_eq_top: SL_n(ℤ) is generated by its transvections.
• Matrix.SpecialLinearGroup.closure_range_toSpecialLinearGroup_eq_top_of_field: over a field, SL_n is generated by its transvections.
• Matrix.SpecialLinearGroup.transvectionHom, transvection_injective, and map_transvection: the one-parameter subgroup over a commutative ring, its injectivity, and its naturality under ring homomorphisms.
• TauCeti.commute_transvection and TauCeti.transvection_mul_transvection_eq_mul_mul: the type-A relations for bare transvection matrices.
• Matrix.SpecialLinearGroup.commute_transvection and Matrix.SpecialLinearGroup.commutatorElement_transvection: the type-A commutator relations for determinant-one transvections.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GLn/SLnTransvection.lean, Chris Birkbeck), toward the multiplicativity theory of the GL_n Hecke ring.

theorem Matrix.SpecialLinearGroup.exists_list_transvec_prod {ι : Type u_1} [Fintype ι] [DecidableEq ι] (σ : SpecialLinearGroup ι ℤ) : ∃ (T : List (TransvectionStruct ι ℤ)), σ = (List.map TransvectionStruct.toSpecialLinearGroup T).prod

Every element of SL_n(ℤ) is a product of elementary transvections.

theorem Matrix.SpecialLinearGroup.closure_range_toSpecialLinearGroup_eq_top {ι : Type u_1} [Fintype ι] [DecidableEq ι] : Subgroup.closure (Set.range TransvectionStruct.toSpecialLinearGroup) = ⊤

SL_n(ℤ) is generated by its transvections.

theorem Matrix.SpecialLinearGroup.closure_range_toSpecialLinearGroup_eq_top_of_field {ι : Type u_1} [Fintype ι] [DecidableEq ι] {K : Type u_2} [Field K] : Subgroup.closure (Set.range TransvectionStruct.toSpecialLinearGroup) = ⊤

Over a field, the special linear group is generated by its elementary transvections.

def Matrix.SpecialLinearGroup.transvectionHom {n : Type u_1} [DecidableEq n] [Fintype n] {A : Type u} [CommRing A] {i j : n} (hij : i ≠ j) : Multiplicative A →* SpecialLinearGroup n A

The transvections at a fixed pair of distinct indices form a one-parameter subgroup of Matrix.SpecialLinearGroup n A, isomorphic to the additive group of A.

Equations

• Matrix.SpecialLinearGroup.transvectionHom hij = { toFun := fun (c : Multiplicative A) => Matrix.SpecialLinearGroup.transvection hij (Multiplicative.toAdd c), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Matrix.SpecialLinearGroup.transvectionHom_apply {n : Type u_1} [DecidableEq n] [Fintype n] {A : Type u} [CommRing A] {i j : n} (hij : i ≠ j) (c : Multiplicative A) : (transvectionHom hij) c = transvection hij (Multiplicative.toAdd c)

The value of the determinant-one root subgroup homomorphism is the transvection of the parameter.

theorem Matrix.SpecialLinearGroup.transvection_injective {n : Type u_1} [DecidableEq n] [Fintype n] {A : Type u} [CommRing A] {i j : n} (hij : i ≠ j) : Function.Injective (transvection hij)

Distinct parameters give distinct determinant-one transvections.

@[simp]

theorem Matrix.SpecialLinearGroup.map_transvection {n : Type u_1} [DecidableEq n] [Fintype n] {A : Type u} [CommRing A] {i j : n} {B : Type v} [CommRing B] (f : A →+* B) (hij : i ≠ j) (c : A) : (map f) (transvection hij c) = transvection hij (f c)

A determinant-one transvection is natural in the base ring: applying a ring homomorphism entrywise to Matrix.SpecialLinearGroup.transvection hij c gives Matrix.SpecialLinearGroup.transvection hij (f c).

The commutator relations between transvections

theorem TauCeti.commute_transvection {n : Type u_1} [Fintype n] [DecidableEq n] {A : Type w} [CommRing A] {i j k l : n} (hjk : j ≠ k) (hli : l ≠ i) (c d : A) : Commute (Matrix.transvection i j c) (Matrix.transvection k l d)

Two matrices of the form Matrix.transvection commute when the corresponding matrix-unit products vanish in both orders. When both index pairs are distinct, these are root-subgroup elements and the sum of the two roots εᵢ - εⱼ and εₖ - εₗ is not a root.

theorem TauCeti.transvection_mul_transvection_eq_mul_mul {n : Type u_1} [Fintype n] [DecidableEq n] {A : Type w} [CommRing A] {i j l : n} (hij : i ≠ j) (hil : i ≠ l) (c d : A) : Matrix.transvection i j c * Matrix.transvection j l d = Matrix.transvection j l d * Matrix.transvection i j c * Matrix.transvection i l (c * d)

A product identity for two chaining matrices of the form Matrix.transvection: reversing their order produces the extra factor at (i, l). When j ≠ l as well, all three index pairs are distinct and this is the type A Chevalley commutator relation before it is written as a commutator.

theorem Matrix.SpecialLinearGroup.commute_transvection {n : Type u_1} [Fintype n] [DecidableEq n] {A : Type w} [CommRing A] {i j k l : n} (hij : i ≠ j) (hkl : k ≠ l) (hjk : j ≠ k) (hli : l ≠ i) (c d : A) : Commute (transvection hij c) (transvection hkl d)

Two determinant-one transvections at index pairs that do not chain commute in SL n A.

theorem Matrix.SpecialLinearGroup.transvection_mul_transvection_eq_mul_mul {n : Type u_1} [Fintype n] [DecidableEq n] {A : Type w} [CommRing A] {i j l : n} (hij : i ≠ j) (hjl : j ≠ l) (hil : i ≠ l) (c d : A) : transvection hij c * transvection hjl d = transvection hjl d * transvection hij c * transvection hil (c * d)

A product identity for two chaining determinant-one transvections: reversing their order produces the extra transvection at (i, l).

theorem Matrix.SpecialLinearGroup.commutatorElement_transvection {n : Type u_1} [Fintype n] [DecidableEq n] {A : Type w} [CommRing A] {i j l : n} (hij : i ≠ j) (hjl : j ≠ l) (hil : i ≠ l) (c d : A) : ⁅transvection hij c, transvection hjl d⁆ = transvection hil (c * d)

The Chevalley commutator relation of type A in SL n A. The commutator of the determinant-one transvections xᵢⱼ(c) and xⱼₗ(d), for distinct i, j and l, is xᵢₗ(cd).