Assembling the trace of Popa–Zagier's explicit element

The trace of the explicit element on positive even-degree period polynomials is a finite sum of fixed-trace weight sums. Writing Tₙ for this element, for determinant n ≠ 0 the formula is

tr(Tₙ | W_w) = (1/12) ∑_{-4n ≤ t ≤ 4n} (∑_{det M = n, tr M = t} weight M) P_{w+2}(t,n).

Here weight is twelve times the coefficient in Popa–Zagier's equation (15), and P is the Dickson polynomial already used for binary-form traces. The inner sums have finite support: every matrix of nonzero weight has all entries bounded by 2n. No elliptic, hyperbolic or parabolic weight identity is assumed. Substituting those identities into this formula is what converts it to the class-number and divisor-sum expression for the trace.

The sum is over integral matrices, not projective classes. Each projective coefficient is (weight A + weight (-A)) / 12, so no additional factor of two occurs. This is distinct from the factor of two in the later transfer from W_w to cusp forms.

Main results

• TauCeti.TraceFormulaMatrixModule.trace_periodAction_popaZagierElement_eq_finsum: the ambient trace as a weight sum over determinant-n matrices.
• TauCeti.TraceFormulaMatrixModule.trace_periodAction_popaZagierElement_eq_sum_trace_fibres: the ambient trace grouped by integral trace.

The analogous theorem trace_periodActionRestrict_popaZagierElement_eq_sum_trace_fibres gives this formula on period polynomials of positive even degree.

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, §§2, 4, equation (15).

theorem TauCeti.TraceFormulaMatrixModule.trace_periodAction_popaZagierElement_eq_finsum {K : Type u_1} [Field K] {n : ℤ} (hn : n ≠ 0) (w : ℕ) (hw : Even w) : (LinearMap.trace K ↥(MvPolynomial.homogeneousSubmodule (Fin 2) K w)) ((periodAction hw) (popaZagierElement K n)) = 12⁻¹ * ∑ᶠ (A : TraceFormulaMatrix n), ↑(PopaZagier.weight ↑A) * Polynomial.eval (↑(↑A).trace) (Polynomial.dickson 2 (↑n) w)

The trace of Popa–Zagier's explicit element on degree-w binary forms is the sum of its integer matrix weights times the Dickson trace polynomial, divided by twelve.

theorem TauCeti.TraceFormulaMatrixModule.trace_periodAction_popaZagierElement_eq_sum_trace_fibres {K : Type u_1} [Field K] {n : ℤ} (hn : n ≠ 0) (w : ℕ) (hw : Even w) : (LinearMap.trace K ↥(MvPolynomial.homogeneousSubmodule (Fin 2) K w)) ((periodAction hw) (popaZagierElement K n)) = 12⁻¹ * ∑ t ∈ Finset.Icc (-4 * n) (4 * n), ↑(∑ᶠ (A : ↥(traceDetFiber (Fin 2) t n)), PopaZagier.weight ↑A) * Polynomial.eval (↑t) (Polynomial.dickson 2 (↑n) w)

Grouping by integral trace reduces the ambient trace to finitely many fixed-trace weight sums. The interval [-4n,4n] contains the trace of every matrix of nonzero weight.

theorem TauCeti.TraceFormulaMatrixModule.trace_periodActionRestrict_popaZagierElement_eq_sum_trace_fibres {K : Type u_1} [Field K] {n : ℤ} [CharZero K] (hn : n ≠ 0) (w : ℕ) (hw : Even w) (hw₀ : w ≠ 0) : (LinearMap.trace K ↥(periodPolynomials K w)) (ExchangeRelations.periodActionRestrict hw ⋯) = 12⁻¹ * ∑ t ∈ Finset.Icc (-4 * n) (4 * n), ↑(∑ᶠ (A : ↥(traceDetFiber (Fin 2) t n)), PopaZagier.weight ↑A) * Polynomial.eval (↑t) (Polynomial.dickson 2 (↑n) w)

The trace of Popa–Zagier's explicit element on period polynomials of positive even degree is the fixed-trace weight sum. The exchange relations identify this trace with the ambient binary-form trace.