Matrices with fixed determinant

This file defines the type of matrices with fixed determinant m and proves some basic results about them.

We also prove that the subgroup of SL(2,ℤ) generated by S and T is the whole group.

Note: Some of this was done originally in Lean 3 in the kbb (https://github.com/kim-em/kbb/tree/master) repository, so credit to those authors.

def FixedDetMatrix (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] (m : R) : Type (max 0 u_1 u_2)

The subtype of matrices with fixed determinant m

theorem FixedDetMatrices.ext' (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] {m : R} {A B : FixedDetMatrix n R m} (h : ↑A = ↑B) : A = B

Extensionality theorem for FixedDetMatrix with respect to the underlying matrix, not entrywise.

theorem FixedDetMatrices.ext (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] {m : R} {A B : FixedDetMatrix n R m} (h : ∀ (i j : n), ↑A i j = ↑B i j) : A = B

theorem FixedDetMatrices.ext_iff {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommRing R] {m : R} {A B : FixedDetMatrix n R m} : A = B ↔ ∀ (i j : n), ↑A i j = ↑B i j

instance FixedDetMatrices.instSMulSpecialLinearGroupFixedDetMatrix (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] (m : R) : SMul (Matrix.SpecialLinearGroup n R) (FixedDetMatrix n R m)

theorem FixedDetMatrices.smul_def (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] (m : R) (g : Matrix.SpecialLinearGroup n R) (A : FixedDetMatrix n R m) : g • A = ⟨↑g * ↑A, ⋯⟩

instance FixedDetMatrices.instMulActionSpecialLinearGroupFixedDetMatrix (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] (m : R) : MulAction (Matrix.SpecialLinearGroup n R) (FixedDetMatrix n R m)

theorem FixedDetMatrices.smul_coe (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] (m : R) (g : Matrix.SpecialLinearGroup n R) (A : FixedDetMatrix n R m) : ↑(g • A) = ↑g * ↑A

def FixedDetMatrices.reps (m : ℤ) : Set (FixedDetMatrix (Fin 2) ℤ m)

Set of representatives for the orbits under S and T

def FixedDetMatrices.reduceStep {m : ℤ} (A : FixedDetMatrix (Fin 2) ℤ m) : FixedDetMatrix (Fin 2) ℤ m

Reduction step for matrices in Δ m which moves the matrices towards reps

@[irreducible]

def FixedDetMatrices.reduce_rec {m : ℤ} {C : FixedDetMatrix (Fin 2) ℤ m → Sort u_3} (base : (A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 = 0 → C A) (step : (A : FixedDetMatrix (Fin 2) ℤ m) → ↑A 1 0 ≠ 0 → C (reduceStep A) → C A) (A : FixedDetMatrix (Fin 2) ℤ m) : C A

Reduction lemma for integral FixedDetMatrices.

@[irreducible]

def FixedDetMatrices.reduce {m : ℤ} : FixedDetMatrix (Fin 2) ℤ m → FixedDetMatrix (Fin 2) ℤ m

Map from Δ m → Δ m which reduces a FixedDetMatrix towards a representative element in reps

theorem FixedDetMatrices.reduce_of_pos {m : ℤ} {A : FixedDetMatrix (Fin 2) ℤ m} (hc : ↑A 1 0 = 0) (ha : 0 < ↑A 0 0) : reduce A = ModularGroup.T ^ (-(↑A 0 1 / ↑A 1 1)) • A

theorem FixedDetMatrices.reduce_of_not_pos {m : ℤ} {A : FixedDetMatrix (Fin 2) ℤ m} (hc : ↑A 1 0 = 0) (ha : ¬0 < ↑A 0 0) : reduce A = ModularGroup.T ^ (-(-↑A 0 1 / -↑A 1 1)) • ModularGroup.S • ModularGroup.S • A

@[simp]

theorem FixedDetMatrices.reduce_reduceStep {m : ℤ} {A : FixedDetMatrix (Fin 2) ℤ m} (hc : ↑A 1 0 ≠ 0) : reduce (reduceStep A) = reduce A

theorem FixedDetMatrices.reps_entries_le_m' {m : ℤ} {A : FixedDetMatrix (Fin 2) ℤ m} (h : A ∈ reps m) (i j : Fin 2) : ↑A i j ∈ Finset.Icc (-|m|) |m|

An auxiliary result bounding the size of the entries of the representatives in reps

@[simp]

theorem FixedDetMatrices.reps_zero_empty : reps 0 = ∅

noncomputable instance FixedDetMatrices.repsFintype (k : ℤ) : Fintype ↑(reps k)

@[simp]

theorem FixedDetMatrices.S_smul_four {m : ℤ} (A : FixedDetMatrix (Fin 2) ℤ m) : ModularGroup.S • ModularGroup.S • ModularGroup.S • ModularGroup.S • A = A

@[simp]

theorem FixedDetMatrices.T_S_rel_smul {m : ℤ} (A : FixedDetMatrix (Fin 2) ℤ m) : ModularGroup.S • ModularGroup.S • ModularGroup.S • ModularGroup.T • ModularGroup.S • ModularGroup.T • ModularGroup.S • A = ModularGroup.T⁻¹ • A

theorem FixedDetMatrices.reduce_mem_reps {m : ℤ} (hm : m ≠ 0) (A : FixedDetMatrix (Fin 2) ℤ m) : reduce A ∈ reps m

theorem FixedDetMatrices.induction_on {m : ℤ} {C : FixedDetMatrix (Fin 2) ℤ m → Prop} {A : FixedDetMatrix (Fin 2) ℤ m} (hm : m ≠ 0) (h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A) (hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (ModularGroup.S • B)) (hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (ModularGroup.T • B)) : C A

theorem FixedDetMatrices.reps_one_id (A : FixedDetMatrix (Fin 2) ℤ 1) (a1 : ↑A 1 0 = 0) (a4 : 0 < ↑A 0 0) (a6 : |↑A 0 1| < |↑A 1 1|) : A = 1

theorem SpecialLinearGroup.SL2Z_generators : Subgroup.closure {ModularGroup.S, ModularGroup.T} = ⊤

SL(2, ℤ) is generated by S and T.