Double cosets of PSL(2, ℤ) in ℳₙ

Let Γ = PSL(2, ℤ) act on the projective determinant-n matrix module ℳₙ by left and by right multiplication. For n > 0 the elementary divisor theorem puts every M ∈ ℳₙ into the double coset of a diagonal matrix: M = g · diag(d₀, d₁) · g' with g ∈ SL(2, ℤ), g' ∈ Γ, 0 < d₀, d₀ ∣ d₁ and d₀ d₁ = n. Writing d₀ = a and d₁ = am, the double cosets Γ (a 0; 0 am) Γ with a, m ≥ 1 therefore cover ℳ = ⋃_{n ≥ 1} ℳₙ, as in Popa and Zagier's decomposition of ℳ into double cosets.

The right coset diag(d₀, d₁) · Γ and the orbit of diag(d₀, d₁) under left multiplication by Γ_∞ = ⟨T⟩ are described explicitly below; for diag(1, m) the former is Popa and Zagier's coset K₀ = (1 0; 0 m) Γ.

Main results

• TauCeti.TraceFormulaMatrixModule.exists_eq_smul_op_smul_mk_diagonal: for n > 0, every element of ℳₙ lies in the double coset of some diag(d₀, d₁) with 0 < d₀, d₀ ∣ d₁.
• TauCeti.TraceFormulaMatrixModule.mk_mem_orbit_op_mk_diagonal_iff: for n ≠ 0, the class of A lies in the right coset diag(d₀, d₁) · Γ if and only if d₀ divides the first row of A and d₁ its second row.
• TauCeti.TraceFormulaMatrixModule.mk_mem_orbit_zpowers_T_mk_diagonal_iff: the Γ_∞-orbit of diag(d₀, d₁) consists of the classes of (d₀, j d₁; 0, d₁).

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. The decomposition into double cosets and the description of K₀ are in §4, proof of Theorem 4(b); the Γ_∞-orbits of the matrices (1 b; 0 n) are used in §3, proof of Theorem 2(b).

theorem TauCeti.TraceFormulaMatrixModule.exists_eq_smul_op_smul_mk_diagonal {n : ℤ} (hn : 0 < n) (x : TraceFormulaMatrixModule n) : ∃ (d₀ : ℤ) (d₁ : ℤ) (h : d₀ * d₁ = n), 0 < d₀ ∧ d₀ ∣ d₁ ∧ ∃ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (γ : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ), x = g • MulOpposite.op γ • mk (TraceFormulaMatrix.diagonal d₀ d₁ h)

Diagonal representatives of the double cosets (Popa–Zagier, §4, proof of Theorem 4(b)): for n > 0, every x ∈ ℳₙ is g · diag(d₀, d₁) · γ for some g ∈ SL(2, ℤ), γ ∈ PSL(2, ℤ) and d₀ d₁ = n with 0 < d₀ and d₀ ∣ d₁.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.mk_mem_orbit_op_mk_diagonal_iff {n d₀ d₁ : ℤ} (h : d₀ * d₁ = n) (hn : n ≠ 0) {A : TraceFormulaMatrix n} : mk A ∈ MulAction.orbit (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ)ᵐᵒᵖ (mk (TraceFormulaMatrix.diagonal d₀ d₁ h)) ↔ d₀ ∣ ↑A 0 0 ∧ d₀ ∣ ↑A 0 1 ∧ d₁ ∣ ↑A 1 0 ∧ d₁ ∣ ↑A 1 1

The right coset of a diagonal matrix (Popa–Zagier, §4, proof of Theorem 4(b)): for n = d₀ d₁ ≠ 0, the class of a determinant-n matrix A lies in the right coset diag(d₀, d₁) · Γ if and only if d₀ divides the first row of A and d₁ its second row.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.mk_mem_orbit_zpowers_T_mk_diagonal_iff {n d₀ d₁ : ℤ} (h : d₀ * d₁ = n) {A : TraceFormulaMatrix n} : mk A ∈ MulAction.orbit (↥(Subgroup.zpowers ModularGroup.T)) (mk (TraceFormulaMatrix.diagonal d₀ d₁ h)) ↔ ∃ (j : ℤ), ↑A = !![d₀, j * d₁; 0, d₁] ∨ ↑A = -!![d₀, j * d₁; 0, d₁]

The Γ_∞-orbit of a diagonal matrix: the class of A lies in the orbit of diag(d₀, d₁) under left multiplication by Γ_∞ = ⟨T⟩ if and only if A = ±(d₀, j d₁; 0, d₁) for some j ∈ ℤ.