The right coset sums of Popa–Zagier's explicit element

For ξ = ∑ c_M M ∈ k[ℳₙ] and a right coset K = M Γ of Γ = PSL(2, ℤ) in ℳₙ, write ⟨ξ, K⟩ = ∑_{M ∈ K} c_M. Popa and Zagier's explicit Hecke element Tₙ (written with a tilde in their paper, their eq. (15)) has ⟨Tₙ, K⟩ = -1 for every right coset K and every n > 0 (their Theorem 4(b), first part). Together with the exchange relations (B), this coset identity is the input from which they deduce that Tₙ satisfies the period relation (A).

The proof reduces to a single coset in each double coset. Since Tₙ satisfies (B), its coset sums are constant on double cosets (Popa–Zagier, Theorem 2(a)), and every double coset contains a coset diag(d₀, d₁) Γ with 0 < d₀ ∣ d₁. On such a coset, write Tₙ = T₁ - T₂ - T₃ - T₄ as in eq. (15).

• T₂ = T₁ U with U = T S, and right multiplication by U permutes each right coset, so the contributions of T₁ and T₂ cancel.
• The coefficients of eq. (15) only depend on which of its linear inequalities hold, so they are invariant under scaling the matrix by a positive integer (PopaZagier.weight_smul), and the coset of diag(d₀, d₀ m) is the scaled coset of diag(1, m).
• In the coset of diag(1, m), the matrices occurring in T₃ or T₄ are (0 -1; m 0) and (1 -1; m 0) and, for m = 1, also (0 -1; 1 -1). Their coefficients in T₃ + T₄ add up to 1.

Main results

• TauCeti.TraceFormulaMatrixModule.mapDomain_orbitRel_mk_coeff_popaZagierElement: ⟨Tₙ, K⟩ = -1 for every right coset K of ℳₙ, n > 0.

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, §3 Theorem 2 and §4, eq. (15) and Theorem 4(b).

The sums T₃ and T₄ on the coset of diag(1, m)

The coset sum of the weight

theorem TauCeti.TraceFormulaMatrixModule.mapDomain_orbitRel_mk_coeff_popaZagierElement {k : Type u_1} {n : ℤ} [DivisionRing k] (h12 : 12 ≠ 0) (hn : 0 < n) (x : TraceFormulaMatrixModule n) : (Finsupp.mapDomain (Quotient.mk (MulAction.orbitRel (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ)ᵐᵒᵖ (TraceFormulaMatrixModule n))) (popaZagierElement k n).coeff) ⟦x⟧ = -1

Popa–Zagier, Theorem 4(b), the coset identity: for n > 0, the coefficients of Popa–Zagier's explicit element Tₙ sum to -1 over every right coset K of PSL(2, ℤ) in ℳₙ, that is, ⟨Tₙ, K⟩ = -1. This needs 12 ≠ 0 in k, as Tₙ is defined with denominators dividing 12.