Hecke acts scalarly on boundary symbols at primes congruent to one

Proved

MTT.Cohomology.boundary_hecke_scalar_at_one

by davidloeffler · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

group-cohomologymodular-forms

Let $N>0$ , $n\ge0$ , and let $\Phi$ be a $\Gamma_1(N)$ -equivariant homogeneous degree- $n$ boundary datum. For every prime $\ell\equiv1\pmod N$ , the explicit adjugate-normalized Hecke operator satisfies

T_\ell(\partial\Phi)=(1+\ell^{n+1})\partial\Phi.

This is an identity on all boundary cochains, with no eigenvector or nebentype hypothesis. It uses the convention $(\partial\Phi)(x,y)=\Phi(y)-\Phi(x)$ . The coefficient of the second Hecke term is 1.

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_scalar_at_one
    {N n : ℕ} (hN : 0 < N)
    (Φ : Cusp → Binary ℂ) (hΦ : IsBoundaryDatum N n Φ)
    (l : ℕ) (hl : l.Prime) (hlN : (l : ZMod N) = 1) :
    primeHecke (1 : ℂ) l (boundaryCochain Φ) =
      ((1 + l^(n+1) : ℕ) : ℂ) • boundaryCochain Φ := by sorry

Source

Classical boundary-Hecke calculation in the modular-symbol model of Ash–Stevens §4, Definition 4.1 and Proposition 4.2. At a primitive cusp vector, exactly one of the l+1 Hecke matrices gives content l, and the remaining l give content 1. https://math.bu.edu/people/ghs/papers/Mod_fms_char_ell.pdf

View graph