Boundary Hecke sum at a single cusp
ProvedMTT.Cohomology.boundary_hecke_cusp_sum_at_onegroup-cohomologyhecke-operatorsmodular-forms
Let , let be a -equivariant homogeneous polynomial-valued function of degree on the rational cusps, and let be a prime with . For the standard representatives () and , the sum of the adjugate-normalized transforms of at any cusp is . This is the single-cusp calculation underlying the scalar action on boundary cochains. In primitive-vector terms, one representative produces a vector of content and the other representatives produce primitive vectors; homogeneity accounts for the power .
Preamble
import Definitions.Def_MTT_Cohomology_Boundary import Mathlib.NumberTheory.LSeries.PrimesInAP set_option autoImplicit false noncomputable section open scoped BigOperators open MTT.Cohomology
Formal statement
theorem MTT.Cohomology.boundary_hecke_cusp_sum_at_one
{N n : ℕ} (hN : 0 < N)
(Φ : Cusp → Binary ℂ) (hΦ : IsBoundaryDatum N n Φ)
(l : ℕ) (hl : l.Prime) (hlN : (l : ZMod N) = 1) (x : Cusp) :
(∑ b : Fin l,
act (Matrix.adjugate !![1, (b.val : ℤ); 0, (l : ℤ)])
(Φ (fractional !![1, (b.val : ℤ); 0, (l : ℤ)] x))) +
act (Matrix.adjugate !![(l : ℤ), 0; 0, 1])
(Φ (fractional !![(l : ℤ), 0; 0, 1] x)) =
((1 + l^(n+1) : ℕ) : ℂ) • Φ x := by sorrySource
Classical boundary-Hecke calculation in the modular-symbol model of Ash–Stevens, Modular forms in characteristic l and special values of their L-functions (1986), section 4, Definition 4.1 and Proposition 4.2, pp. 861–863, https://math.bu.edu/people/ghs/papers/Mod_fms_char_ell.pdf. For a primitive cusp vector, exactly one of the l+1 standard Hecke representatives gives content l and the remaining l give content 1.