Chinese-remainder splitting of SL(ι, ℤ)

For coprime moduli d, d', every τ ∈ SL(ι, ℤ) — ι any finite index type — factors as τ₁ * τ₂ with τ₁ ≡ 1 (mod d) and τ₂ ≡ 1 (mod d'). The proof is by generators: τ is a product of transvections (exists_list_transvec_prod), a single transvection splits by Bézout, and splittings multiply.

Main results

• Matrix.SpecialLinearGroup.exists_mul_modEq_one_of_coprime: the factorization.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GLn/CoprimeMul.lean, Chris Birkbeck), where it is the group-theoretic input to the coprime multiplication rule of the Hecke ring.

Chinese-remainder splitting of SL(ι, ℤ)

Every τ ∈ SL(ι, ℤ) factors as τ₁ * τ₂ with τ₁ ≡ 1 mod d and τ₂ ≡ 1 mod d' for coprime d, d': transvections split by Bézout, and splittings multiply.

theorem Matrix.SpecialLinearGroup.exists_mul_modEq_one_of_coprime {ι : Type u_1} [Fintype ι] [DecidableEq ι] (d d' : ℕ) (hcop : d.Coprime d') (τ : SpecialLinearGroup ι ℤ) : ∃ (τ₁ : SpecialLinearGroup ι ℤ) (τ₂ : SpecialLinearGroup ι ℤ), τ = τ₁ * τ₂ ∧ (∀ (i j : ι), ↑d ∣ ↑τ₁ i j - if i = j then 1 else 0) ∧ ∀ (i j : ι), ↑d' ∣ ↑τ₂ i j - if i = j then 1 else 0

Chinese remainder decomposition of SL(ι, ℤ): for coprime d, d', every element factors as τ₁ * τ₂ with τ₁ ≡ 1 mod d and τ₂ ≡ 1 mod d'.