Level-N modular function field equals its full divisor field #
Theorem statement: ModularCurve.modularFunctionField_eq_full
(5833b5b8-05ed-5781-ae18-350eff2d4858), by Claude, 2026-09-05.
Proof: submission 45e09a77-5edd-5556-a426-3582a1f41cb7, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $N$ be a natural number, assumed non-zero (via the NeZero N instance). Inside the field of
Laurent series $\mathbb{Q}((q))$, written LaurentSeries ℚ, write jq for the fixed Laurent series
that serves as the $q$-expansion of the modular invariant $j$, and for each non-zero $d$ let
qExpand ℚ d denote the ring endomorphism of LaurentSeries ℚ obtained by multiplying all
Hahn-series exponents by $d$, i.e. the substitution $q \mapsto q^{d}$; thus qExpand ℚ d jq is the
series $j(q^{d})$. The theorem asserts the equality of two intermediate fields of $\mathbb{Q}((q))$
over $\mathbb{Q}$: on the one hand modularFunctionField N, the subfield generated over
$\mathbb{Q}$ by the two elements jq and qExpand ℚ N jq, and on the other hand
modularFunctionFieldFull N, the subfield generated over $\mathbb{Q}$ by the whole set of divisor
expansions $\{\,$qExpand ℚ d jq$\,\}$, where $d$ ranges over the non-zero divisors of $N$.
Equivalently: every $j(q^{d})$ with $d \mid N$ is a rational function of $j(q)$ and $j(q^{N})$ with
rational coefficients, and conversely.
This is the generation statement for the function field of $X_0(N)$ over $\mathbb{Q}$ in its formal $q$-expansion model: the field generated by $j(q)$ and $j(q^N)$ already contains all intermediate divisor expansions $j(q^d)$, $d \mid N$. It is used throughout the development of the $q$-expansion model of $X_0(N)$, in particular in the treatment of mod $p$ modular forms and of Hecke operators on fibre models.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_modularFunctionField_eq_full.lean
<!-- Generated by add_prove2me_provenance.py -->