Cochain Hecke operator preserves coefficient coboundaries #
Let $N,\ell$ be natural numbers with $\ell\neq 0$, let $K$ be a commutative ring, $V$ a $K$-module,
and let $\rho$ be a $K$-linear representation of $\Gamma_0(N)$ on $V$. Write $U=$
HeckeEis.heckeUpper N ℓ for the subgroup of $\Gamma_0(N)$
consisting of those matrices $g$ with $\ell \mid g_{01}$, and let HeckeEis.heckeConj N ℓ be the group homomorphism $U\to\Gamma_0(N)$ sending
$g=\begin{pmatrix}a&b\\c&d\end{pmatrix}$ to $\begin{pmatrix}a&b/\ell\\ c\ell&d\end{pmatrix}$, i.e.
conjugation by $\mathrm{diag}(1,\ell)$. Let $a\colon V\to V$ be $K$-linear and assume
$a\circ\rho(\mathrm{heckeConj}(u))=\rho(u)\circ a$ for every $u\in U$. Let $z\colon\Gamma_0(N)\to V$
lie in HeckeEis.coeffCoboundaries ρ, the image of the linear
map $v\mapsto (g\mapsto \rho(g)v-v)$; that is, $z(g)=\rho(g)v-v$ for some $v\in V$. The conclusion
is that the function
$$g\longmapsto \sum_{q\in\Gamma_0(N)/U}\rho\bigl(\overline{g\cdot q}\bigr)\,a\bigl(z\bigl(\mathrm{heckeConj}(\overline{g\cdot q}^{-1}\,g\,\overline q)\bigr)\bigr),$$
where $\overline{\,\cdot\,}$ denotes the chosen representative of a coset and the finite sum is over
the (finite-index) quotient $\Gamma_0(N)/U$, again lies in HeckeEis.coeffCoboundaries ρ.
This is the statement that the cochain-level Hecke operator $T_\ell$ on $V$-valued functions on $\Gamma_0(N)$, built from a double-coset decomposition together with an intertwining endomorphism $a$ of the coefficient module, carries $1$-coboundaries to $1$-coboundaries. Together with the companion statement for cocycles it allows $T_\ell$ to be defined on $H^1(\Gamma_0(N),\rho)$, and it is used by the subsequent results on Hecke-equivariant maps to and from coefficient cohomology.
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/Theorems/Thm_HeckeEis_coeffHeckeFun_mem_coeffCoboundaries.lean
Prove2Me submission: ef4c7cb3-2936-51c4-953d-94be9ec44797 (ACCEPTED).