Hecke operators Tp, Up on modular and cusp forms #
Definition: ModularForm_HeckeOperatorForms (fade376f-2288-591a-bdb5-cbe38983f3ce), by Claude,
2026-09-05.
For a weight $k \in \mathbb{Z}$ and level $\Gamma_0(N)$, this module packages the raw Hecke
operators of ModularForm_HeckeOperator as bundled $\mathbb{C}$-linear endomorphisms of the Mathlib
spaces ModularForm (CongruenceSubgroup.Gamma0 N) k and CuspForm (CongruenceSubgroup.Gamma0 N) k.
Recall the underlying operators on functions $f : \mathbb{H} \to \mathbb{C}$: with $\alpha_j = \begin{pmatrix}1 & j\\ 0 & p\end{pmatrix}$ and $\delta_p = \begin{pmatrix}p & 0\\ 0 & 1\end{pmatrix}$ acting by the weight-$k$ slash action, heckeU k p f $= \sum_{j=0}^{p-1} f \mid_k \alpha_j$, i.e. $\tau \mapsto p^{-1}\sum_{j<p} f((\tau+j)/p)$, and heckeT k p f $=$ heckeU k p f
$+\, f\mid_k \delta_p$, i.e. the extra term $p^{k-1}f(p\tau)$; on $q$-expansions these are the usual
normalisations $a_n \mapsto a_{np}$ and $a_n \mapsto a_{np} + p^{k-1}a_{n/p}$.
ModularForm.heckeTLin k hp hpN takes $p$ prime
and $p \nmid N$ (whence $N \neq 0$, since $p \mid 0$) and sends $f$ to the modular form whose
underlying function is heckeT k p ⇑f; its three structure fields — $\Gamma_0(N)$-invariance under
the weight-$k$ slash action, holomorphy as a map of the upper half-plane, and boundedness at the
cusps — are filled in by the imported theorems heckeT_slash_eq_self_of_mem_Gamma0,
mdifferentiable_heckeT and
ModularFormClass.isBoundedAt_heckeT.
ModularForm.heckeULin k hpN does the same with
heckeU under the hypotheses [NeZero N] and $p \mid N$; note that no primality of $p$ is assumed
for $U_p$. CuspForm.heckeTLin and
CuspForm.heckeULin are the parallel
constructions on cusp forms, with the boundedness field replaced by vanishing at the cusps via
CuspFormClass.isZeroAt_heckeT/isZeroAt_heckeU.
Additivity and $\mathbb{C}$-homogeneity come from heckeT_add, heckeT_smul, heckeU_add,
heckeU_smul through injectivity of the coercion to functions. Four rfl lemmas
(coe_heckeTLin_apply, coe_heckeULin_apply and their pointwise forms) record that the coercion of
the bundled operator is the raw operator. Only $T_p$ and $U_p$ at a single prime are constructed
here: no $T_n$ for composite $n$, and no $\Gamma_1(N)$ or nebentypus variants.
Relation to Mathlib. Built on Mathlib's ModularForm, CuspForm, CongruenceSubgroup.Gamma0
and weight-$k$ slash action; Mathlib provides no Hecke operators on these spaces, so these linear
endomorphisms are the project's own.
Where it is used. These bundled operators make the Hecke action on $S_k(\Gamma_0(N))$ expressible in Lean, and hence statements about commuting families, eigenforms and their eigenvalues — the input to the construction of the Galois representation attached to a weight-$2$ newform on $\Gamma_0(N)$ used in the Frey curve argument.
<!-- Generated by add_prove2me_provenance.py -->
The linear Hecke operator U on modular forms, using the specified slash-action sum.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The linear Hecke operator U restricted to cusp forms.
Equations
- One or more equations did not get rendered due to their size.