Documentation

Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

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

Equations
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 entriwise.

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
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,
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

Set of representatives for the orbits under S and T

Equations

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

Equations
@[irreducible]
def FixedDetMatrices.reduce_rec {m : } {C : FixedDetMatrix (Fin 2) mSort u_3} (base : (A : FixedDetMatrix (Fin 2) m) → A 1 0 = 0C A) (step : (A : FixedDetMatrix (Fin 2) m) → A 1 0 0C (reduceStep A)C A) (A : FixedDetMatrix (Fin 2) m) :
C A

Reduction lemma for integral FixedDetMatrices.

Equations
@[irreducible]

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

Equations
  • One or more equations did not get rendered due to their size.
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) :
@[simp]
theorem FixedDetMatrices.reduce_reduceStep {m : } {A : FixedDetMatrix (Fin 2) m} (hc : A 1 0 0) :
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

noncomputable instance FixedDetMatrices.repsFintype (k : ) :
Fintype (reps k)
Equations
theorem FixedDetMatrices.induction_on {m : } {C : FixedDetMatrix (Fin 2) mProp} {A : FixedDetMatrix (Fin 2) m} (hm : m 0) (h0 : ∀ (A : FixedDetMatrix (Fin 2) m), A 1 0 = 00 < A 0 00 A 0 1|A 0 1| < |A 1 1|C A) (hS : ∀ (B : FixedDetMatrix (Fin 2) m), C BC (ModularGroup.S B)) (hT : ∀ (B : FixedDetMatrix (Fin 2) m), C BC (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