Relative degree of ℚ(j,j_N) over ℚ(j) #
Theorem statement: ModularCurve.relfinrank_modularFunctionField
(19d6be68-bdd4-543c-8d62-a8b0a05dc95d), by Claude, 2026-09-05.
Proof: submission 006c8835-6c3e-5f21-afdf-108c317687c0, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Fix a natural number $N \neq 0$. Work inside the field $\mathrm{LaurentSeries}\ \mathbb{Q}$ of
formal Laurent series over $\mathbb{Q}$, and let $jq$ be the element $q^{-1}$ times the power series
$jNumQ$ obtained from $jNum$ by mapping its integer coefficients into $\mathbb{Q}$, and let $jqN\ N$
be the image $\mathrm{qExpand}\ \mathbb{Q}\ N\ (jq)$ of $jq$ under the ring homomorphism of Laurent
(Hahn) series induced by multiplication by $N$ on exponents, i.e. the substitution $q \mapsto q^{N}$. Let $\mathrm{modularFunctionField}\ N$ be the intermediate field $\mathbb{Q}(jq,\ \mathrm{qExpand}\ \mathbb{Q}\ N\ (jq))$ of $\mathrm{LaurentSeries}\ \mathbb{Q}$ generated over
$\mathbb{Q}$ by these two series. The assertion is an equality of (possibly infinite)
cardinal-valued degrees: the relative finrank, in the sense of IntermediateField.relfinrank, of
the pair consisting of the intermediate field $\mathbb{Q}(jq)$ and $\mathrm{modularFunctionField}\ N$ coincides with the $\mathbb{Q}(jq)$-module rank of the intermediate field of
$\mathrm{LaurentSeries}\ \mathbb{Q}$ generated over $\mathbb{Q}(jq)$ by the single element $jqN\ N$.
This is the bookkeeping identity that converts the relative degree of the two-generator modular function field $\mathbb{Q}(j(q), j(q^{N}))$ over $\mathbb{Q}(j(q))$ into the degree of a simple extension $\mathbb{Q}(j)(j_N)/\mathbb{Q}(j)$, the shape in which the degree $\psi(N)$ and the irreducibility of the modular polynomial $\Phi_N$ are established. It is used by the statements identifying this degree with $\psi(N)$, by the irreducibility statement for $\Phi_N$, and by the generation statement for the function field.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_relfinrank_modularFunctionField.lean
<!-- Generated by add_prove2me_provenance.py -->