At squarefree level, divisor expansions are generated by prime ones #
Theorem statement: ModularCurve.full_eq_adjoin_primes (8842403e-a8ed-525d-bc7f-84e1e01e224e), by
Claude, 2026-09-05.
Proof: submission 1599ae03-e0bf-5c5e-bed5-29f4271973fb, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $N$ be a natural number, nonzero as a typeclass hypothesis, and assume $N$ is squarefree. Work
inside the field $\mathbb{Q}((q))$ of Laurent series over $\mathbb{Q}$, in which jq denotes the
Laurent series $q^{-1}$ times the rational power series jNumQ (the $q$-expansion of the
$j$-invariant), and in which qExpand ℚ n is the ring endomorphism substituting $q \mapsto q^{n}$,
obtained by multiplying exponents by $n$; thus jqN p $=$ qExpand ℚ p jq is the expansion of
$j(q^{p})$. The assertion is an equality of intermediate fields of $\mathbb{Q}((q))$ over
$\mathbb{Q}$: the field modularFunctionFieldFull N, defined as the subfield generated over
$\mathbb{Q}$ by all the series qExpand ℚ d jq for nonzero divisors $d$ of $N$, coincides with the
subfield generated over $\mathbb{Q}$ by jq together with the series jqN p for $p$ ranging over
the prime factors of $N$ (the nonzero condition on $p$ being automatic there).
This identifies, at squarefree level, the formal $q$-expansion model of the compositum of the
function fields of the curves $X_0(d)$, $d \mid N$, with the field generated by the prime-level
expansions alone: $\mathbb{Q}(j(q^{d}) : d \mid N) = \mathbb{Q}(j, j(q^{p}) : p \mid N)$. It is used
in the degree computations for the fields $\mathbb{Q}(j)(j(q^{N}))$, in particular by
[ModularCurve.finrank_adjoin_jqN_eq_of_squarefree]
(thm.html#ModularCurve.finrank_adjoin_jqN_eq_of_squarefree),
ModularCurve.relfinrank_adjoin_primes and
ModularCurve.relfinrank_full_mul_prime, which
together give the degree $\psi(N)$ of the modular equation of level $N$.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_full_eq_adjoin_primes.lean
<!-- Generated by add_prove2me_provenance.py -->