The upper-triangular representatives of Γ \ ℳₙ

For a nonzero integer n, every orbit of SL(2, ℤ) on the projective determinant-n matrix module ℳₙ contains exactly one class of an upper-triangular matrix (a b; 0 d) with ad = n, 0 < a and 0 ≤ b < |d|. Popa and Zagier write ℳₙ^∞ for this set of representatives and Tₙ^∞ for its formal sum. The matrices themselves are Mathlib's FixedDetMatrices.reps n, which TauCeti.LinearAlgebra.Matrix.FixedDetMatrices shows to be a transversal of the SL(2, ℤ)-orbits of determinant-n matrices and counts (FixedDetMatrices.ncard_reps). This file takes their projective classes, proves that they form a transversal of the orbits of ℳₙ, and deduces |Γ \ ℳₙ| = σ₁(|n|).

Popa and Zagier take Γ = PSL(2, ℤ). Since -1 acts trivially on ℳₙ, the PSL(2, ℤ)-orbits are the SL(2, ℤ)-orbits, and this file works with the latter throughout: Γ \ ℳₙ denotes MulAction.orbitRel.Quotient SL(2, ℤ) ℳₙ.

Main definitions

• TauCeti.TraceFormulaMatrixModule.upperTriangularReps n: the set ℳₙ^∞ of projective classes of the matrices in FixedDetMatrices.reps n.
• TauCeti.TraceFormulaMatrixModule.upperTriangularRepsEquiv: for n ≠ 0, ℳₙ^∞ is in bijection with the orbit space Γ \ ℳₙ.

Main results

• TauCeti.TraceFormulaMatrixModule.exists_smul_mem_upperTriangularReps: for n ≠ 0, every SL(2, ℤ)-orbit of ℳₙ meets ℳₙ^∞.
• TauCeti.TraceFormulaMatrixModule.exists_T_zpow_smul_mk_mem_upperTriangularReps: for n ≠ 0, the class of an upper-triangular matrix can be moved into ℳₙ^∞ by a power of T.
• TauCeti.TraceFormulaMatrixModule.smul_eq_self_of_mem_upperTriangularReps: an element of SL(2, ℤ) that moves one element of ℳₙ^∞ into ℳₙ^∞ fixes it.
• TauCeti.TraceFormulaMatrixModule.ncard_upperTriangularReps: |ℳₙ^∞| = σ₁(|n|).
• TauCeti.TraceFormulaMatrixModule.card_orbitRel_quotient: |Γ \ ℳₙ| = σ₁(|n|).

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, Section 2.

The representative set ℳₙ^∞

def TauCeti.TraceFormulaMatrixModule.upperTriangularReps (n : ℤ) : Set (TraceFormulaMatrixModule n)

Popa--Zagier's set ℳₙ^∞ of upper-triangular representatives of Γ \ ℳₙ: the projective classes of the matrices (a b; 0 d) with ad = n, 0 < a and 0 ≤ b < |d|.

theorem TauCeti.TraceFormulaMatrixModule.mem_upperTriangularReps {n : ℤ} {x : TraceFormulaMatrixModule n} : x ∈ upperTriangularReps n ↔ ∃ A ∈ FixedDetMatrices.reps n, mk A = x

The elements of ℳₙ^∞ are exactly the classes of the matrices in FixedDetMatrices.reps n.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.mk_mem_upperTriangularReps {n : ℤ} {A : TraceFormulaMatrix n} : mk A ∈ upperTriangularReps n ↔ A ∈ FixedDetMatrices.reps n ∨ -A ∈ FixedDetMatrices.reps n

The class of A lies in ℳₙ^∞ exactly when A or -A is an upper-triangular representative.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.upperTriangularReps_zero : upperTriangularReps 0 = ∅

ℳ₀^∞ is empty: there are no upper-triangular representatives of determinant 0.

theorem TauCeti.TraceFormulaMatrixModule.mk_injOn_reps {n : ℤ} : Set.InjOn mk (FixedDetMatrices.reps n)

Distinct upper-triangular representatives have distinct projective classes.

instance TauCeti.TraceFormulaMatrixModule.instFiniteElemUpperTriangularReps (n : ℤ) : Finite ↑(upperTriangularReps n)

ℳₙ^∞ is finite.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.ncard_upperTriangularReps (n : ℤ) : (upperTriangularReps n).ncard = (ArithmeticFunction.sigma 1) n.natAbs

ℳₙ^∞ has σ₁(|n|) elements, as many as FixedDetMatrices.reps n.

theorem TauCeti.TraceFormulaMatrixModule.exists_smul_mem_upperTriangularReps {n : ℤ} (hn : n ≠ 0) (x : TraceFormulaMatrixModule n) : ∃ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ), g • x ∈ upperTriangularReps n

Existence of upper-triangular representatives: for n ≠ 0, every element of ℳₙ can be moved into ℳₙ^∞ by SL(2, ℤ).

theorem TauCeti.TraceFormulaMatrixModule.exists_T_zpow_smul_mk_mem_upperTriangularReps {n : ℤ} (hn : n ≠ 0) {A : TraceFormulaMatrix n} (hA : ↑A 1 0 = 0) : ∃ (m : ℤ), ModularGroup.T ^ m • mk A ∈ upperTriangularReps n

For n ≠ 0, the class of an upper-triangular matrix of determinant n can be moved into ℳₙ^∞ by a power of T.

theorem TauCeti.TraceFormulaMatrixModule.smul_eq_self_of_mem_upperTriangularReps {n : ℤ} {x : TraceFormulaMatrixModule n} {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hx : x ∈ upperTriangularReps n) (hgx : g • x ∈ upperTriangularReps n) : g • x = x

Uniqueness of upper-triangular representatives: if g : SL(2, ℤ) moves an element of ℳₙ^∞ into ℳₙ^∞, then it fixes that element.

noncomputable def TauCeti.TraceFormulaMatrixModule.upperTriangularRepsEquiv {n : ℤ} (hn : n ≠ 0) : ↑(upperTriangularReps n) ≃ MulAction.orbitRel.Quotient (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)

For n ≠ 0, ℳₙ^∞ is a transversal of the SL(2, ℤ)-orbits of ℳₙ (Popa--Zagier, Section 2): sending a representative to its orbit is a bijection onto Γ \ ℳₙ.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.upperTriangularRepsEquiv_apply {n : ℤ} (hn : n ≠ 0) (x : ↑(upperTriangularReps n)) : (upperTriangularRepsEquiv hn) x = Quotient.mk'' ↑x

The transversal bijection sends a representative to its orbit.

theorem TauCeti.TraceFormulaMatrixModule.upperTriangularRepsEquiv_symm_mk_mem_orbit {n : ℤ} (hn : n ≠ 0) (x : TraceFormulaMatrixModule n) : ↑((upperTriangularRepsEquiv hn).symm (Quotient.mk'' x)) ∈ MulAction.orbit (Matrix.SpecialLinearGroup (Fin 2) ℤ) x

The inverse of the transversal bijection picks the representative in the given orbit.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.upperTriangularRepsEquiv_symm_mk {n : ℤ} (hn : n ≠ 0) (x : ↑(upperTriangularReps n)) : (upperTriangularRepsEquiv hn).symm (Quotient.mk'' ↑x) = x

The inverse of the transversal bijection sends the orbit of a representative back to it.

theorem TauCeti.TraceFormulaMatrixModule.finite_orbitRel_quotient {n : ℤ} (hn : n ≠ 0) : Finite (MulAction.orbitRel.Quotient (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n))

For n ≠ 0, the orbit space Γ \ ℳₙ is finite.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.card_orbitRel_quotient {n : ℤ} (hn : n ≠ 0) : Nat.card (MulAction.orbitRel.Quotient (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)) = (ArithmeticFunction.sigma 1) n.natAbs

The number of orbits (Popa--Zagier, Section 2): for n ≠ 0, Γ \ ℳₙ has σ₁(|n|) elements.