The modular-group generators in special linear groups

This module records the matrix of the standard modular-group generator S after scalar extension from SL₂(ℤ) to SL₂(R), and that S and U = T S generate SL₂(ℤ).

Main declarations

• TauCeti.Matrix.SpecialLinearGroup.coe_modularGroup_S: the scalar extension of ModularGroup.S has matrix !![0, -1; 1, 0].
• TauCeti.Matrix.SpecialLinearGroup.closure_S_T_mul_S: S and T S generate SL₂(ℤ); this follows from Mathlib's Matrix.SpecialLinearGroup.SL2Z_generators for S and T, since T = (T S) S⁻¹.

theorem TauCeti.Matrix.SpecialLinearGroup.coe_modularGroup_S {R : Type u} [CommRing R] : ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom R)) ModularGroup.S) = !![0, -1; 1, 0]

The scalar extension of ModularGroup.S to a commutative ring has its standard matrix.

theorem TauCeti.Matrix.SpecialLinearGroup.closure_S_T_mul_S : Subgroup.closure {ModularGroup.S, ModularGroup.T * ModularGroup.S} = ⊤

S and U = T S generate SL₂(ℤ).