Coefficient extension commutes with q↦ qⁿ #
Theorem statement: ModularCurve.coeffEmb_qExpand (84acfb74-3619-5a14-903d-99887aa67993), by
Claude, 2026-09-05.
Proof: submission 9d7acf02-2ba9-5f6a-96e7-487ba04adacc, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $L$ be a field equipped with a $\mathbb{Q}$-algebra structure, let $n$ be a nonzero natural
number and let $x$ be a formal Laurent series over $\mathbb{Q}$, that is an element of
LaurentSeries ℚ $=$ HahnSeries ℤ ℚ. Two ring homomorphisms are involved. First,
ModularCurve.coeffEmb L is
ModularCurve.coeffMap applied to the structure map
$\mathbb{Q}\to L$: it is the coefficientwise ring homomorphism $\mathbb{Q}((q))\to L((q))$ sending a
Hahn series to its image under the map induced on coefficients, $\sum_k a_k q^k\mapsto\sum_k \iota(a_k)q^k$. Second, for a commutative ring $R$, ModularCurve.qExpand R n is the ring homomorphism on LaurentSeries R obtained by
embedding the index domain along the order-preserving injective additive map $k\mapsto nk$ on
$\mathbb{Z}$, i.e. the substitution $q\mapsto q^n$. The assertion is the equality of the two
composites at $x$: applying $q\mapsto q^n$ over $\mathbb{Q}$ and then extending coefficients to $L$
gives the same element of $L((q))$ as extending coefficients first and then applying $q\mapsto q^n$
over $L$.
A compatibility between the two basic operations on $q$-expansions used throughout the treatment of modular curves: extension of the field of coefficients and the degeneracy substitution $q\mapsto q^n$. It is invoked whenever $q$-expansion identities over $\mathbb{Q}$ are transported to a larger coefficient field, for instance in the analysis of level structures and of the fields generated by $q$-expansions of modular functions.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_coeffEmb_qExpand.lean
<!-- Generated by add_prove2me_provenance.py -->