Existence of the induced Hecke endomorphism of H¹ₚₐᵣ #
Fix natural numbers $N$ and $\ell$ with $\ell \neq 0$, a commutative ring $K$, a $K$-module $V$, a
representation $\rho$ of the group $\Gamma_0(N)$ on $V$ over $K$, and a $K$-linear endomorphism $a$
of $V$. Assume the intertwining hypothesis: for every $u$ in HeckeEis.heckeUpper N ℓ, the subgroup of those elements of $\Gamma_0(N)$ whose
upper right entry is divisible by $\ell$, one has $a \circ \rho(\mathrm{heckeConj}(u)) = \rho(u) \circ a$, where $\mathrm{heckeConj}(u)$ is the matrix obtained from $u = \begin{pmatrix} \alpha & \beta \\ \gamma & \delta\end{pmatrix}$ as $\begin{pmatrix} \alpha & \beta/\ell \\ \gamma\ell & \delta\end{pmatrix}$ (conjugation by $\mathrm{diag}(1,\ell)$), viewed again in $\Gamma_0(N)$. The
conclusion asserts the existence of a $K$-linear endomorphism $T$ of HeckeEis.coeffH1par ρ — the quotient of the submodule of parabolic cocycles
(functions $z : \Gamma_0(N) \to V$ with $z(gh) = z(g) + \rho(g)z(h)$ and $z(\gamma) \in \mathrm{im}(\rho(\gamma) - 1)$ whenever the integral matrix $\gamma$ has $\mathrm{tr}(\gamma)^2 = 4$) by the parabolic cocycles that are coboundaries — such that for every parabolic cocycle $z$
there is a parabolic cocycle $w$ whose underlying function $\Gamma_0(N) \to V$ equals
HeckeEis.coeffHeckeFun N ℓ ρ a z, the finite sum over $q \in \Gamma_0(N)/\mathrm{heckeUpper}(N,\ell)$ of $\rho((g\cdot q)^{\mathrm{out}})\bigl(a\,z(\mathrm{heckeConj}(\mathrm{transferAux}(g,q)))\bigr)$, and such that
$T$ sends the class of $z$ to the class of $w$. Thus the statement simultaneously records that the
cochain-level operator preserves parabolic cocycles and that it descends to the quotient.
This is the construction of the Hecke operator $T_\ell$ on the parabolic cohomology $H^1_{\mathrm{par}}(\Gamma_0(N), \rho)$ from its cochain-level avatar, in the classical Eichler–Shimura setting where the coefficient datum is a linear map $a$ intertwining $\rho$ with its conjugate by $\mathrm{diag}(1,\ell)$. It is used in the construction of Hecke eigenclasses in parabolic cohomology of binary-form representations and, through those, in the integral-structure statement for cusp forms.
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/Theorems/Thm_HeckeEis_exists_coeffH1par_linearMap_coeffHeckeFun.lean
Prove2Me submission: 424062d0-1ce2-5345-9953-29cf4d1db00e (ACCEPTED).