Boundary Hecke sum at the cusp $\infty$ equals $1+\ell^{n+1}$

Proved

MTT.Cohomology.boundary_hecke_cusp_sum_at_one_infty

by carlok · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

group-cohomologyhecke-operatorsmodular-forms

Let $\Phi$ be a boundary datum of level $N$ and weight $n$ — a $\Gamma_1(N)$ -equivariant map from the rational cusps to binary forms of degree $n$ over $\mathbf C$ — and let $\ell\ge 0$ be an integer. Consider the $\ell+1$ standard Hecke representatives

g_b=\begin{pmatrix}1&b\\0&\ell\end{pmatrix}\ (0\le b<\ell),\qquad g_\infty=\begin{pmatrix}\ell&0\\0&1\end{pmatrix},

each acting on cusps by fractional linear transformations and on coefficients through its adjugate. Then the boundary Hecke sum, evaluated at the cusp $\infty$ , is the scalar $1+\ell^{\,n+1}$ :

\sum_{b=0}^{\ell-1}\operatorname{adj}(g_b)\cdot\Phi(g_b\infty)\;+\;\operatorname{adj}(g_\infty)\cdot\Phi(g_\infty\infty)\;=\;\bigl(1+\ell^{\,n+1}\bigr)\,\Phi(\infty).

This is the cusp- $\infty$ case of the single-cusp boundary Hecke calculation. In primitive-vector language: the vector $(1,0)$ representing $\infty$ is fixed by all $\ell+1$ representatives, one of them ( $g_\infty$ ) produces a vector of content $\ell$ and the other $\ell$ produce primitive vectors, and homogeneity of degree $n$ converts the content into the factor $\ell^{\,n}$ , giving $\ell\cdot\ell^{\,n}+1$ .

Two hypotheses that appear in the general single-cusp statement are deliberately absent, because this branch does not need them: $\ell$ need not be prime, and no congruence $\ell\equiv 1\pmod N$ is required. Every one of the $\ell+1$ matrices has vanishing lower-left entry, so it fixes $\infty$ without any appeal to the level structure, and the whole computation takes place inside the stabiliser of a single cusp.

Preamble

import Definitions.Def_MTT_Cohomology_Boundary
set_option autoImplicit false
noncomputable section
open scoped BigOperators
open MTT.Cohomology

Formal statement

theorem MTT.Cohomology.boundary_hecke_cusp_sum_at_one_infty
    {N n : ℕ} (Φ : Cusp → Binary ℂ) (hΦ : IsBoundaryDatum N n Φ) (l : ℕ) :
    (∑ b : Fin l,
      act (Matrix.adjugate !![1, (b.val : ℤ); 0, (l : ℤ)])
        (Φ (fractional !![1, (b.val : ℤ); 0, (l : ℤ)] OnePoint.infty))) +
      act (Matrix.adjugate !![(l : ℤ), 0; 0, 1])
        (Φ (fractional !![(l : ℤ), 0; 0, 1] OnePoint.infty)) =
      ((1 + l^(n+1) : ℕ) : ℂ) • Φ OnePoint.infty := by sorry

Source

Ash-Stevens, Modular forms in characteristic l and special values of their L-functions, Duke Math. J. 53 (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; the cusp at infinity branch of the single-cusp computation

View graph

Boundary Hecke sum at the cusp ∞\infty∞ equals 1+ℓn+11+\ell^{n+1}1+ℓn+1

Boundary Hecke sum at the cusp $\infty$ equals $1+\ell^{n+1}$