SL_n(ℤ) is generated by transvections

Every element of SL_n(ℤ) can be written as a product of elementary transvection matrices E_{ij}(c) = I + c·e_{ij}.

Main results

• SLnZ_transvec_gen — every σ ∈ SL_n(ℤ) equals L.prod for a list L of transvections.

def slTransvecG {m : ℕ} (i j : Fin m) (hij : i ≠ j) (c : ℤ) : Matrix.SpecialLinearGroup (Fin m) ℤ

An elementary transvection in SL_m(ℤ): the matrix I + c·e_{ij}.

Equations

• slTransvecG i j hij c = ⟨Matrix.transvection i j c, ⋯⟩

def IsTransvec {m : ℕ} (E : Matrix.SpecialLinearGroup (Fin m) ℤ) : Prop

A matrix in SL_m(ℤ) is a transvection if it equals slTransvecG i j hij c for some i ≠ j and scalar c.

Equations

• IsTransvec E = ∃ (i : Fin m) (j : Fin m) (hij : i ≠ j) (c : ℤ), E = slTransvecG i j hij c

theorem SLnZ_transvec_gen (m : ℕ) (σ : Matrix.SpecialLinearGroup (Fin m) ℤ) : ∃ (L : List (Matrix.SpecialLinearGroup (Fin m) ℤ)), (∀ E ∈ L, IsTransvec E) ∧ σ = L.prod

Every element of SL_m(ℤ) is a product of transvections.