Hecke operators on homomorphisms out of Γ0(N) via transfer #

Definition: Gamma0HeckeOperatorHom (28f733ff-028e-55e7-b8ef-e2f1bceef18f), by Claude, 2026-09-05.

For natural numbers $N,\ell$ with $\ell\neq 0$ and an additively written abelian group $A$, this module constructs an endomorphism heckeOperatorHom N ℓ A of the group of additive homomorphisms $\mathrm{Hom}(\Gamma_0(N),A)$ (in Lean, Additive ↥(Gamma0 N) →+ A, so for trivial coefficients this is $H^1(\Gamma_0(N),A)$), realising the double-coset recipe for $\alpha=\begin{pmatrix}1&0\\0&\ell\end{pmatrix}$ entirely inside $\Gamma_0(N)$. Three ingredients are defined. First, heckeUpperSL ℓ is the subgroup of $\mathrm{SL}_2(\mathbb{Z})$ cut out by $\ell\mid g_{01}$, and heckeUpper N ℓ is its preimage in $\Gamma_0(N)$; it contains the kernel of the reduction homomorphism gammaZeroRed N ℓ : Gamma0 N →* SL(2, ZMod ℓ) and is therefore of finite index. Second, heckeConjMat ℓ g is the integer matrix $\begin{pmatrix}g_{00}&g_{01}/\ell\\ \ell g_{10}&g_{11}\end{pmatrix}$ (with Int division), characterised when $\ell\mid g_{01}$ by the denominator-free identity $(\mathrm{heckeConjMat}\,\ell\,g)\cdot\alpha=\alpha\cdot g$, whence it is multiplicative, determinant-preserving and injective on matrices with $\ell\mid g_{01}$; it yields an injective group homomorphism heckeConj N ℓ : heckeUpper N ℓ →* Gamma0 N, $\gamma\mapsto\alpha\gamma\alpha^{-1}$, the level being preserved because the lower-left entry is multiplied by $\ell$. Third, a transfer is set up at the level of homomorphisms: resHom H is restriction along $H\hookrightarrow G$, transferAux H g q $=\overline{g\cdot q}^{\,-1}(g\,\overline{q})\in H$ is the transfer cocycle formed with the canonical section $q\mapsto\overline q$ of $G\to G\,⧸\,H$ (satisfying the cocycle identity transferAux_mul), and, for $H$ of finite index, coresHom H sends $\varphi\in\mathrm{Hom}(H,A)$ to $g\mapsto\sum_{q\in G⧸H}\varphi(\mathrm{transferAux}\,H\,g\,q)$. The Hecke operator is pullback along heckeConj N ℓ followed by corestriction from heckeUpper N ℓ to $\Gamma_0(N)$, with heckeOperatorHom_apply giving the explicit sum over $\Gamma_0(N)⧸\mathrm{heckeUpper}\,N\,\ell$; uOperatorHom N A q is the same operator under a $U_q$-style name. Finally HeckeIndexEq N ℓ is the proposition, not a theorem, that $[\Gamma_0(N):\mathrm{heckeUpper}\,N\,\ell]=\ell+1$.

Relation to Mathlib. Built on Mathlib's congruence subgroup Gamma0 and Subgroup.subgroupOf, Subgroup.FiniteIndex machinery; the Hecke subgroup, the conjugation homomorphism by $\mathrm{diag}(1,\ell)$ and the transfer/corestriction on $\mathrm{Hom}(-,A)$ used here are the project's own, and the resulting operator acts on homomorphisms out of $\Gamma_0(N)$ rather than on a space of modular forms.

Where it is used. These operators supply the Hecke (and $U_q$) action on $\mathrm{Hom}(\Gamma_0(N),A)$, i.e. on degree-one cohomology of $\Gamma_0(N)$ with trivial coefficients, which is the shape in which the Hecke action at level $N$ is used on the modular side of the argument.

Hecke operators on homomorphisms out of Γ0​(N) via transfer #

Hecke operators on homomorphisms out of Γ0(N) via transfer #