Substitution q↦ q^ℓ on ratios of integral forms #
Theorem statement: ModularCurve.qExpand_image_intFormRatiosC_subset
(fb14d131-f259-581d-91cd-f5b2891d646b), by Claude, 2026-09-05.
Proof: submission c50984d4-0b5d-5469-b3bb-af2c21e8f9f6, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $K$ be a field, let $\Gamma,\Gamma'\le \mathrm{SL}_2(\mathbb Z)$ be subgroups with $\Gamma$ of
finite index and containing $T=\begin{pmatrix}1&1\\0&1\end{pmatrix}$, and let $\ell$ be a nonzero
natural number. Assume that for every $\gamma\in\Gamma'$ there is a $\gamma_1\in\Gamma$ with
$(\gamma_1)_{00}=\gamma_{00}$, $(\gamma_1)_{01}=\ell\,\gamma_{01}$,
$\ell\,(\gamma_1)_{10}=\gamma_{10}$ and $(\gamma_1)_{11}=\gamma_{11}$; that is,
$\operatorname{diag}(\ell,1)\gamma\operatorname{diag}(\ell,1)^{-1}$ has integral entries and lies in
$\Gamma$. For a subgroup $\Delta\le\mathrm{SL}_2(\mathbb Z)$, ModularCurve.intFormRatiosC K Δ is the set of Laurent series over $K$ of the form $\bar p_f/\bar p_g$, where for some integer weight $k$ there are modular forms $f,g$ of weight $k$ for the image of
$\Delta$ in $\mathrm{GL}_2(\mathbb R)$ and power series $p_f,p_g\in\mathbb Z[[q]]$ whose images in
$\mathbb C[[q]]$ are the $q$-expansions of $f$ and $g$ of width $1$, $\bar p$ denoting the Laurent
series obtained by reducing coefficients to $K$, subject to $\bar p_g\neq 0$. The assertion is that
the ring endomorphism ModularCurve.qExpand K ℓ of $K((q))$, given
by rescaling the exponent support by $\ell$ (so $q\mapsto q^{\ell}$), carries
ModularCurve.intFormRatiosC K Γ into ModularCurve.intFormRatiosC K Γ'.
This is the formal-$q$-expansion shadow of the classical fact that, for $f$ modular of weight $k$ on $\Gamma$, the function $\tau\mapsto f(\ell\tau)$ is modular of the same weight on any group $\Gamma'$ with $\operatorname{diag}(\ell,1)\Gamma'\operatorname{diag}(\ell,1)^{-1}\subseteq\Gamma$, so that $q\mapsto q^{\ell}$ respects the $q$-expansion function fields of the corresponding modular curves. It is used in the construction and comparison of degeneracy maps and Hecke operators on modular curves and their Jacobians.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_qExpand_image_intFormRatiosC_subset.lean
<!-- Generated by add_prove2me_provenance.py -->