Hecke operators Tp, Up on functions on the upper half-plane #

Definition: ModularForm_HeckeOperator (e1cf8d29-c1f1-569b-9fbd-05f00ec56b83), by Claude, 2026-09-05.

The module sets up the weight-$k$ Hecke operators $T_p$ and $U_p$ as operators on arbitrary functions $f\colon\mathbb H\to\mathbb C$, using Mathlib's weight-$k$ slash action of $\mathrm{GL}_2(\mathbb R)$ (normalisation $|\det\gamma|^{k-1}\,\mathrm{denom}(\gamma,\tau)^{-k}$). First come the matrices: upperTriangularGL a b d is $\begin{pmatrix}a&b\\0&d\end{pmatrix}$ as an element of $\mathrm{GL}_2(\mathbb R)$, given $ad\neq 0$; heckeMatrix p j is $\begin{pmatrix}1&j\\0&p\end{pmatrix}$ and heckeDiagMatrix p is $\begin{pmatrix}p&0\\0&1\end{pmatrix}$, both defined for all natural $p$ with the junk value $1$ at $p=0$ so as to be total. Accompanying lemmas record their entries, that both determinants equal $p$ and are positive, the values of UpperHalfPlane.denom ($p$, resp. $1$), the Möbius actions $\tau\mapsto(\tau+j)/p$ and $\tau\mapsto p\tau$, the triviality of the conjugation $\sigma$ attached to a positive determinant, and hence the pointwise slash formulas $(f\mid_k \texttt{heckeMatrix\ p\ j})(\tau)=p^{-1}f((\tau+j)/p)$ and $(f\mid_k\texttt{heckeDiagMatrix\ p})(\tau)=p^{k-1}f(p\tau)$ for $p\neq 0$.

Then heckeU k p f $=\sum_{j<p} f\mid_k\begin{pmatrix}1&j\\0&p\end{pmatrix}$ and heckeT k p f $=$ heckeU k p f $+\,f\mid_k\begin{pmatrix}p&0\\0&1\end{pmatrix}$, with the pointwise formulas $(U_pf)(\tau)=p^{-1}\sum_{j<p}f((\tau+j)/p)$ and $(T_pf)(\tau)=(U_pf)(\tau)+p^{k-1}f(p\tau)$ for $p\neq 0$, the degenerate values heckeU k 0 f = 0 and heckeT k 0 f = f, and additivity, $\mathbb C$-homogeneity, compatibility with negation and subtraction. Note that $p$ is an arbitrary natural number here: nothing in these definitions requires $p$ prime or imposes any modularity or growth condition on $f$.

Finally the same operators are given on the coefficient side, as operators on sequences $a\colon\mathbb N\to\mathbb C$: coeffHeckeU p a n = a (n * p) and `coeffHeckeT k p a n = a (n * p)

p^{k-1} a (n / p)` when $p\mid n$, the second term being $0$ otherwise; these are shown additive and $\mathbb C$-homogeneous. No theorem in this module links the two sides; the coefficient operators are purely algebraic data.

Relation to Mathlib. Mathlib supplies the upper half-plane, its $\mathrm{GL}_2(\mathbb R)$-action with UpperHalfPlane.denom, UpperHalfPlane.σ and the weight-$k$ slash action; the Hecke matrices and the operators $T_p$, $U_p$ built from them, together with their coefficient-side counterparts, are the project's own.

Where it is used. These operators are the input to the notion of a normalised Hecke eigenform used throughout the modularity part of the argument; the coefficient-side versions coeffHeckeT and coeffHeckeU allow eigenform conditions on $q$-expansion coefficients to be stated without analysis. Separate modules prove that $T_p$ and $U_p$ preserve the spaces of modular and cusp forms for $\Gamma_0(N)$ and relate the two descriptions.

Hecke operators Tp​, Up​ on functions on the upper half-plane #

Hecke operators Tp, Up on functions on the upper half-plane #