Hecke conjugation commutes with diag(ℓ,1) on binary forms #
Theorem statement: HeckeEis.binaryFormAlphaAdj_comp_binaryFormRepSL_heckeConj
(b6bda1d4-8f2d-5ef9-956e-c4fa45302310), by Claude, 2026-09-05.
Proof: submission a1f2509f-1d70-5f33-be78-8e47a990f76a, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Fix a commutative ring $K$ and natural numbers $n$, $N$, $\ell$ with $\ell\neq 0$. Write
$\mathrm{BinaryForm}\,K\,n$ for the $K$-submodule of degree-$n$ homogeneous polynomials in
$K[X_0,X_1]$, and for an integral $2\times 2$ matrix $M$ let $\mathrm{binarySubst}\,K\,M$ be the
$K$-algebra endomorphism of $K[X_0,X_1]$ determined by $X_j\mapsto\sum_i (M_{ij}\bmod K)\,X_i$; this
preserves $\mathrm{BinaryForm}\,K\,n$, and HeckeEis.binaryFormRepSL K n is the resulting representation of $\mathrm{SL}_2(\mathbb Z)$ on it, while HeckeEis.binaryFormAlphaAdj K n ℓ is the
endomorphism induced by $\begin{pmatrix}\ell&0\\0&1\end{pmatrix}$, i.e. $P(X_0,X_1)\mapsto P(\ell X_0,X_1)$. Let $u$ lie in HeckeEis.heckeUpper N ℓ, the
subgroup of those $\gamma\in\Gamma_0(N)$ whose upper-right entry is divisible by $\ell$, and let
$\mathrm{heckeConj}\,N\,\ell\,(u)\in\Gamma_0(N)$ be the element obtained from
$u=\begin{pmatrix}a&b\\c&d\end{pmatrix}$ by the entrywise recipe $\begin{pmatrix}a&b/\ell\\ \ell c&d\end{pmatrix}$. The assertion is the equality of $K$-linear endomorphisms of
$\mathrm{BinaryForm}\,K\,n$: the representation of $\mathrm{heckeConj}\,N\,\ell\,(u)$ followed by
binaryFormAlphaAdj K n ℓ equals binaryFormAlphaAdj K n ℓ followed by the representation of $u$,
where the representation of $\Gamma_0(N)$ is the restriction of binaryFormRepSL K n along the
inclusion $\Gamma_0(N)\hookrightarrow\mathrm{SL}_2(\mathbb Z)$.
This is the coefficient-module compatibility condition for the degree-$n$ binary-form coefficients under conjugation by $\mathrm{diag}(1,\ell)$, the matrix part of the Hecke operator $T_\ell$ on $\Gamma_0(N)$. It is what makes the cochain-level Hecke operator with binary-form coefficients preserve cocycles and coboundaries, and it is cited in the proofs of the Hecke equivariance of the Eichler–Shimura map and of the existence of an integral structure on spaces of cusp forms.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_HeckeEis_binaryFormAlphaAdj_comp_binaryFormRepSL_heckeConj.lean
<!-- Generated by add_prove2me_provenance.py -->