Upper-triangular representatives of integral matrices of fixed determinant

Mathlib's FixedDetMatrices.reps n is the set of integral matrices (a b; 0 d) with ad = n, 0 < a and 0 ≤ b < |d|, and Mathlib proves (FixedDetMatrices.reduce_mem_reps) that, for n ≠ 0, the reduction algorithm carries every determinant-n matrix into it. This file completes that to the statement that FixedDetMatrices.reps n is a set of representatives for the action of SL(2, ℤ) by left multiplication on the determinant-n matrices, n ≠ 0, and counts it. It also records that only finitely many integral matrices of a given determinant have entries bounded by a given constant. Restricted to the primitive matrices, those whose entries have greatest common divisor one, the representatives FixedDetMatrices.primitiveReps n are the (a b; 0 d) with gcd(a, b, d) = 1.

Main results

• FixedDetMatrices.exists_smul_mem_reps: for n ≠ 0, every determinant-n matrix can be moved into FixedDetMatrices.reps n by SL(2, ℤ).
• FixedDetMatrices.eq_one_of_smul_mem_reps: the only g ∈ SL(2, ℤ) moving a matrix of FixedDetMatrices.reps n into FixedDetMatrices.reps n is g = 1; hence (FixedDetMatrices.eq_of_smul_eq_of_mem_reps) two matrices of FixedDetMatrices.reps n in the same SL(2, ℤ)-orbit are equal.
• FixedDetMatrices.repsEquiv: the representatives are parametrized by positive factor pairs (a, d) of |n| and residues 0 ≤ b < d.
• FixedDetMatrices.ncard_reps: FixedDetMatrices.reps n has σ₁(|n|) elements.
• FixedDetMatrices.sum_reps_pow: for even w, the sum of dʷ over the representatives (a b; 0 d) is σ_{w+1}(|n|).
• FixedDetMatrices.finite_setOf_abs_le: there are only finitely many integral matrices of determinant n whose entries are at most B in absolute value.
• FixedDetMatrices.toGL: for n ≠ 0, an integral matrix of determinant n as an element of GL(m, ℚ), on which left multiplication by SL(m, ℤ) is multiplication by its image (FixedDetMatrices.toGL_smul), and FixedDetMatrices.toGLReal, its image in GL(m, ℝ).
• FixedDetMatrices.isPrimitive_smul_iff: left multiplication by SL(m, ℤ) preserves primitivity.
• FixedDetMatrices.primitiveReps: the primitive matrices of FixedDetMatrices.reps n, and FixedDetMatrices.exists_smul_mem_primitiveReps: for n ≠ 0 every primitive matrix of determinant n can be moved into them by SL(2, ℤ).

References

• A. Popa and D. Zagier, An elementary proof of the Eichler--Selberg trace formula, J. Reine Angew. Math. 762 (2020), 105--122, arXiv:1711.00327, Sections 1–2: these are the representatives ℳₙ^∞ of Γ \ ℳₙ fixing ∞.

theorem FixedDetMatrices.exists_smul_mem_reps {n : ℤ} (hn : n ≠ 0) (A : FixedDetMatrix (Fin 2) ℤ n) : ∃ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ), g • A ∈ reps n

Every determinant-n matrix can be moved into reps n by left multiplication by SL(2, ℤ), when n ≠ 0.

theorem FixedDetMatrices.smul_coe_apply {R : Type u_1} [CommRing R] {m : R} (g : Matrix.SpecialLinearGroup (Fin 2) R) (A : FixedDetMatrix (Fin 2) R m) (i j : Fin 2) : ↑(g • A) i j = ↑g i 0 * ↑A 0 j + ↑g i 1 * ↑A 1 j

The entries of g • A for g ∈ SL(2, R) and a 2 × 2 matrix A of fixed determinant.

theorem FixedDetMatrices.eq_one_of_smul_mem_reps {n : ℤ} {A : FixedDetMatrix (Fin 2) ℤ n} {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hA : A ∈ reps n) (hgA : g • A ∈ reps n) : g = 1

No nontrivial element of SL(2, ℤ) moves a representative to a representative: if A and g • A both lie in reps n, then g = 1.

theorem FixedDetMatrices.eq_of_smul_eq_of_mem_reps {n : ℤ} {A B : FixedDetMatrix (Fin 2) ℤ n} {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hA : A ∈ reps n) (hB : B ∈ reps n) (h : g • A = B) : A = B

Two matrices of reps n in the same SL(2, ℤ)-orbit are equal.

theorem FixedDetMatrices.apply_zero_zero_mul_apply_one_one {R : Type u_1} [CommRing R] {m : R} {A : FixedDetMatrix (Fin 2) R m} (h : ↑A 1 0 = 0) : ↑A 0 0 * ↑A 1 1 = m

The diagonal entries of an upper-triangular 2 × 2 matrix of determinant m multiply to m.

def FixedDetMatrices.repsEquiv {n : ℤ} (hn : n ≠ 0) : ↑(reps n) ≃ (p : ↥n.natAbs.divisorsAntidiagonal) × Fin (↑p).2

The upper-triangular representatives, explicitly parametrized. For n ≠ 0, a representative (a b; 0 d) is recorded by the positive factor pair (|a|, |d|) of |n| and the residue b ∈ Fin |d|. The inverse gives d the sign of n.

This is the summation interface for the representatives: an invariant may be summed first over factor pairs and then over the upper-right entry.

@[simp]

theorem FixedDetMatrices.coe_repsEquiv_apply_fst {n : ℤ} (hn : n ≠ 0) (A : ↑(reps n)) : ↑((repsEquiv hn) A).fst = ((↑↑A 0 0).natAbs, (↑↑A 1 1).natAbs)

The factor pair recording a representative (a b; 0 d) is (|a|, |d|).

@[simp]

theorem FixedDetMatrices.coe_repsEquiv_apply_snd {n : ℤ} (hn : n ≠ 0) (A : ↑(reps n)) : ↑((repsEquiv hn) A).snd = (↑↑A 0 1).natAbs

The residue recording a representative (a b; 0 d) is |b|.

@[simp]

theorem FixedDetMatrices.coe_repsEquiv_symm_apply {n : ℤ} (hn : n ≠ 0) (x : (p : ↥n.natAbs.divisorsAntidiagonal) × Fin (↑p).2) : ↑↑((repsEquiv hn).symm x) = !![↑(↑x.fst).1, ↑↑x.snd; 0, n.sign * ↑(↑x.fst).2]

The matrix represented by a factor pair (a, d) and a residue b is (a b; 0, sign(n)d).

@[simp]

theorem FixedDetMatrices.ncard_reps (n : ℤ) : (reps n).ncard = (ArithmeticFunction.sigma 1) n.natAbs

The number of upper-triangular representatives: the set reps n has σ₁(|n|) elements, one for each divisor d of |n| and each 0 ≤ b < d.

theorem FixedDetMatrices.sum_reps_pow {n : ℤ} {R : Type u_1} [CommRing R] {w : ℕ} (hw : Even w) : ∑ A : ↑(reps n), ↑(↑↑A 1 1) ^ w = ↑((ArithmeticFunction.sigma (w + 1)) n.natAbs)

The divisor sum over the upper-triangular representatives: for even w, the sum of dʷ over the representatives (a b; 0 d) in reps n is σ_{w+1}(|n|), since each factor pair (a, d) of |n| carries |d| representatives.

theorem FixedDetMatrices.finite_setOf_abs_le {m : Type u_1} [Fintype m] [DecidableEq m] (n B : ℤ) : {A : FixedDetMatrix m ℤ n | ∀ (i j : m), |↑A i j| ≤ B}.Finite

Finiteness of bounded matrices: there are only finitely many integral matrices of determinant n whose entries are at most B in absolute value.

Integral matrices of nonzero determinant as rational invertible matrices

noncomputable def FixedDetMatrices.toGL {n : ℤ} {m : Type u_1} [Fintype m] [DecidableEq m] (hn : n ≠ 0) (A : FixedDetMatrix m ℤ n) : GL m ℚ

For n ≠ 0, an integral matrix of determinant n as an invertible rational matrix, the form in which it acts on the upper half-plane and on the cusps ℙ¹(ℚ).

@[simp]

theorem FixedDetMatrices.coe_toGL {n : ℤ} {m : Type u_1} [Fintype m] [DecidableEq m] (hn : n ≠ 0) (A : FixedDetMatrix m ℤ n) : ↑(toGL hn A) = (↑A).map Int.cast

The underlying matrix of toGL hn A is the entrywise cast of A.

theorem FixedDetMatrices.det_toGL {n : ℤ} {m : Type u_1} [Fintype m] [DecidableEq m] (hn : n ≠ 0) (A : FixedDetMatrix m ℤ n) : (↑(toGL hn A)).det = ↑n

The determinant of toGL hn A is n.

theorem FixedDetMatrices.toGL_injective {n : ℤ} {m : Type u_1} [Fintype m] [DecidableEq m] (hn : n ≠ 0) : Function.Injective (toGL hn)

toGL hn is injective: the cast ℤ → ℚ is.

theorem FixedDetMatrices.toGL_smul {n : ℤ} {m : Type u_1} [Fintype m] [DecidableEq m] (hn : n ≠ 0) (g : Matrix.SpecialLinearGroup m ℤ) (A : FixedDetMatrix m ℤ n) : toGL hn (g • A) = (Matrix.SpecialLinearGroup.mapGL ℚ) g * toGL hn A

Left multiplication by g ∈ SL(m, ℤ) becomes multiplication by its image in GL(m, ℚ).

Integral matrices of nonzero determinant as real invertible matrices

noncomputable def FixedDetMatrices.toGLReal {n : ℤ} {m : Type u_1} [Fintype m] [DecidableEq m] (hn : n ≠ 0) (A : FixedDetMatrix m ℤ n) : GL m ℝ

For n ≠ 0, an integral matrix of determinant n as an invertible real matrix. For 2 × 2 matrices and 0 < n this is the form in which it acts on the upper half-plane, by the Möbius transformation τ ↦ (a τ + b) / (c τ + d).

theorem FixedDetMatrices.toGLReal_eq_map_toGL {n : ℤ} {m : Type u_1} [Fintype m] [DecidableEq m] (hn : n ≠ 0) (A : FixedDetMatrix m ℤ n) : toGLReal hn A = (Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) (toGL hn A)

toGLReal hn A is the image of toGL hn A under ℚ → ℝ.

@[simp]

theorem FixedDetMatrices.coe_toGLReal {n : ℤ} {m : Type u_1} [Fintype m] [DecidableEq m] (hn : n ≠ 0) (A : FixedDetMatrix m ℤ n) : ↑(toGLReal hn A) = (↑A).map Int.cast

The underlying matrix of toGLReal hn A is the entrywise cast of A.

theorem FixedDetMatrices.toGLReal_apply {n : ℤ} {m : Type u_1} [Fintype m] [DecidableEq m] (hn : n ≠ 0) (A : FixedDetMatrix m ℤ n) (i j : m) : ↑(toGLReal hn A) i j = ↑(↑A i j)

The entries of toGLReal hn A are the casts of the entries of A.

theorem FixedDetMatrices.det_toGLReal {n : ℤ} {m : Type u_1} [Fintype m] [DecidableEq m] (hn : n ≠ 0) (A : FixedDetMatrix m ℤ n) : ↑(Matrix.GeneralLinearGroup.det (toGLReal hn A)) = ↑n

The determinant of toGLReal hn A is n.

theorem FixedDetMatrices.toGLReal_smul {n : ℤ} {m : Type u_1} [Fintype m] [DecidableEq m] (hn : n ≠ 0) (g : Matrix.SpecialLinearGroup m ℤ) (A : FixedDetMatrix m ℤ n) : toGLReal hn (g • A) = (Matrix.SpecialLinearGroup.mapGL ℝ) g * toGLReal hn A

Left multiplication by g ∈ SL(m, ℤ) becomes multiplication by its image in GL(m, ℝ).

@[simp]

theorem FixedDetMatrices.isPrimitive_smul_iff {n : ℤ} {m : Type u_1} [Fintype m] [DecidableEq m] (g : Matrix.SpecialLinearGroup m ℤ) (A : FixedDetMatrix m ℤ n) : TauCeti.IsPrimitive ↑(g • A) ↔ TauCeti.IsPrimitive ↑A

Left multiplication by SL(m, ℤ) preserves and reflects primitivity: the greatest common divisor of the entries is unchanged.

Primitive representatives

noncomputable def FixedDetMatrices.primitiveReps (n : ℤ) : Finset (FixedDetMatrix (Fin 2) ℤ n)

The primitive matrices among the upper-triangular representatives reps n: the matrices (a b; 0 d) with ad = n, 0 < a, 0 ≤ b < |d| and gcd(a, b, d) = 1. For n ≠ 0 they represent the orbits of SL(2, ℤ) on the primitive integral matrices of determinant n.

@[simp]

theorem FixedDetMatrices.mem_primitiveReps {n : ℤ} {A : FixedDetMatrix (Fin 2) ℤ n} : A ∈ primitiveReps n ↔ A ∈ reps n ∧ TauCeti.IsPrimitive ↑A

A matrix lies in primitiveReps n exactly when it is a primitive matrix of reps n.

theorem FixedDetMatrices.exists_smul_mem_primitiveReps {n : ℤ} (hn : n ≠ 0) {A : FixedDetMatrix (Fin 2) ℤ n} (hA : TauCeti.IsPrimitive ↑A) : ∃ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ), g • A ∈ primitiveReps n

For n ≠ 0, every primitive matrix of determinant n can be moved into primitiveReps n by left multiplication by SL(2, ℤ).