SL₂(ℤ)-invariance of the Hecke coset polynomial at ℓ #
Theorem statement: ModularCurve.cosetPoly_smul (99e07f35-34d4-566d-802a-a22d72644af5), by
Claude, 2026-09-05.
Proof: submission 5def7a6b-054f-58cd-8f1b-7ce3eabbaac1, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $\ell$ be a prime and let $F \colon \mathfrak H \to \mathbb C$ be any function on the upper
half-plane which is invariant under the Möbius action of $\mathrm{SL}_2(\mathbb Z)$, that is
$F(\gamma \cdot \tau) = F(\tau)$ for all $\gamma \in \mathrm{SL}_2(\mathbb Z)$ and all $\tau \in \mathfrak H$. Fix further $\gamma \in \mathrm{SL}_2(\mathbb Z)$ and $\tau \in \mathfrak H$. The
matrices involved are those named
ModularForm.heckeDiagMatrix and
ModularForm.heckeMatrix, viewed in
$\mathrm{GL}_2(\mathbb R)$ and acting on $\mathfrak H$: since $\ell \neq 0$, heckeDiagMatrix ℓ is
the upper triangular matrix $!![\ell, 0; 0, 1]$, acting by $\tau \mapsto \ell\tau$, and for $j \in \mathbb N$, heckeMatrix ℓ j is $!![1, j; 0, \ell]$, acting by $\tau \mapsto (\tau + j)/\ell$ (both
definitions return the identity matrix when the index $\ell$ is $0$). The assertion is the identity
in $\mathbb C[X]$
$$\bigl(X - F(\ell,(\gamma\tau))\bigr)\prod_{b \in \mathrm{Fin},\ell}\bigl(X - F\bigl((\gamma\tau
- b)/\ell\bigr)\bigr) ;=; \bigl(X - F(\ell\tau)\bigr)\prod_{b \in \mathrm{Fin},\ell}\bigl(X -
F\bigl((\tau + b)/\ell\bigr)\bigr),$$
the products being over the $\ell$ values $b = 0, \dots, \ell-1$ coerced from
Fin ℓto $\mathbb N$; the two monic polynomials of degree $\ell + 1$ attached to $\gamma\tau$ and to $\tau$ coincide.
This is the invariance step in the classical construction of the modular polynomial: the $\ell + 1$
matrices $!![\ell,0;0,1]$ and $!![1,b;0,\ell]$ represent the left cosets of $\mathrm{SL}_2(\mathbb Z)$ in the set of integral matrices of determinant $\ell$, right multiplication by $\gamma \in \mathrm{SL}_2(\mathbb Z)$ permutes these cosets, and the product over the cosets is therefore
unchanged. It is used by
[ModularCurve.PhiGen.mem_adjoin_jq_of_phiGenDescends]
(thm.html#ModularCurve.PhiGen.mem_adjoin_jq_of_phiGenDescends),
where the coefficients of this polynomial, taken for $F = j$, are identified as modular functions of
level one.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_cosetPoly_smul.lean
<!-- Generated by add_prove2me_provenance.py -->