Cochain-level Hecke operator preserves 1-cocycles #
Fix natural numbers $N$ and $\ell$ with $\ell \neq 0$, a commutative ring $K$, a $K$-module $V$, and
a representation $\rho$ of the congruence subgroup $\Gamma_0(N)$ on $V$ over $K$. Write $U =$
HeckeEis.heckeUpper N ℓ for the subgroup of $\Gamma_0(N)$
consisting of those elements whose upper-right entry is divisible by $\ell$, and $c =$
HeckeEis.heckeConj N ℓ for the group homomorphism $U \to \Gamma_0(N)$ sending a matrix $\begin{pmatrix} \alpha & \beta \\ \gamma & \delta\end{pmatrix}$ in
$U$ to $\begin{pmatrix} \alpha & \beta/\ell \\ \gamma\ell & \delta\end{pmatrix}$. Let $a : V \to V$
be $K$-linear and assume the equivariance $a \circ \rho(c(u)) = \rho(u) \circ a$ for every $u \in U$. Let $z : \Gamma_0(N) \to V$ satisfy the inhomogeneous $1$-cocycle identity $z(gh) = z(g) + \rho(g)(z(h))$ for all $g, h \in \Gamma_0(N)$. The conclusion is that the function $g \mapsto \sum_{q \in \Gamma_0(N)/U} \rho\bigl(\overline{g \cdot q}\bigr)\bigl(a\bigl(z\bigl(c(\overline{g\cdot q}^{-1} g \overline{q})\bigr)\bigr)\bigr)$, the sum
being over the coset space $\Gamma_0(N)/U$ and $\overline{q}$ denoting the chosen representative of
a coset $q$, again satisfies the same $1$-cocycle identity.
This is the $1$-cocycle level construction of the double-coset Hecke operator $T_\ell$ (restriction to $U$, twist by the conjugation $c$ and the intertwiner $a$, then corestriction back to $\Gamma_0(N)$) on inhomogeneous cochains with coefficients in an arbitrary representation. It is the cocycle half of the input needed to induce $T_\ell$ on $H^1$ and on parabolic cohomology, and is cited by the companion statements about coboundaries, parabolic cocycles and the resulting Hecke-equivariant maps on $H^1$.
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/Theorems/Thm_HeckeEis_coeffHeckeFun_mem_coeffCocycles.lean
Prove2Me submission: ed472e60-a50b-5947-81a9-5baea7bf6ab1 (ACCEPTED).