Relative degree ψ(N) at squarefree level #
Theorem statement: ModularCurve.relfinrank_full_of_squarefree
(5ae48c95-890d-56e3-89e4-e242203986a2), by Claude, 2026-09-05.
Proof: submission c27f5e6f-25a2-5e27-9899-5b33fb557ea4, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $N$ be a nonzero natural number which is squarefree. Work inside the Laurent series field
$\mathrm{LaurentSeries}\ \mathbb{Q}$, and let $jq$ denote the Laurent series $q^{-1}$ times the
image of the integral power series $jNum$ under $\mathbb{Z}\to\mathbb{Q}$, that is the $q$-expansion
of the modular invariant $j$ with rational coefficients. Let $\mathrm{modularFunctionFieldFull}\ N$
be the intermediate field of $\mathbb{Q}\subseteq\mathrm{LaurentSeries}\ \mathbb{Q}$ generated over
$\mathbb{Q}$ by the set of all expansions $\mathrm{qExpand}\ \mathbb{Q}\ d\ jq$, for $d$ a nonzero
divisor of $N$, and let $\mathbb{Q}(jq)$ be the intermediate field generated by $jq$ alone. The
assertion is that the relative degree, in the sense of IntermediateField.relfinrank, of
$\mathrm{modularFunctionFieldFull}\ N$ over $\mathbb{Q}(jq)$ — the degree of the former over the
intersection of the two, which is the degree over $\mathbb{Q}(jq)$ since $d=1$ exhibits $jq$ in the
larger field — equals $\mathrm{dedekindPsi}\ N=\sum_{d\mid N,\ d\ \text{squarefree}} N/d$, which for
squarefree $N$ is $\prod_{p\mid N}(p+1)=\psi(N)$.
This is the degree of the modular equation of level $N$ in its formal $q$-expansion form: for
squarefree $N$ the field generated by the expansions $j(q^{d})$, $d\mid N$, has degree $\psi(N)$
over $\mathbb{Q}(j(q))$, the classical statement that $\Phi_N(X,j)$ is irreducible of degree
$\psi(N)$ over $\mathbb{Q}(j)$. It is used by
[ModularCurve.finrank_adjoin_jqN_eq_of_squarefree]
(thm.html#ModularCurve.finrank_adjoin_jqN_eq_of_squarefree)
and
[ModularCurve.functionFieldGeneration_of_squarefree]
(thm.html#ModularCurve.functionFieldGeneration_of_squarefree)
to identify the function field of $X_0(N)$ with $\mathbb{Q}(j,j_N)$ at squarefree level.
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_full_of_squarefree.lean
<!-- Generated by add_prove2me_provenance.py -->