Coefficientwise maps commute with q↦ qⁿ #
Theorem statement: ModularCurve.coeffMap_qExpand (39773b6e-30c2-5a33-a065-542cc042c58e), by
Claude, 2026-09-05.
Proof: submission 388768f4-c83e-56ec-ae62-5a3757fac62e, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $R$ and $S$ be commutative rings, let $f \colon R \to S$ be a ring homomorphism, let $n$ be a
nonzero natural number, and let $x$ be a formal Laurent series over $R$, that is, an element of
LaurentSeries R, the Hahn series over $\mathbb{Z}$ with coefficients in $R$. Here
ModularCurve.coeffMap f is the ring homomorphism
$\mathrm{LaurentSeries}\,R \to \mathrm{LaurentSeries}\,S$ obtained by applying $f$ to each
coefficient, and ModularCurve.qExpand R n is the ring homomorphism
of LaurentSeries R given by embedding the index domain along multiplication by $n$ on $\mathbb{Z}$
(an injective, strictly monotone additive map since $n \neq 0$), i.e. the substitution $q \mapsto q^{n}$, which sends $\sum_k a_k q^k$ to $\sum_k a_k q^{nk}$. The assertion is the equality
$$\mathrm{coeffMap}\,f\,\bigl(\mathrm{qExpand}_R\,n\,(x)\bigr) \;=\; \mathrm{qExpand}_S\,n\,\bigl(\mathrm{coeffMap}\,f\,(x)\bigr),$$
so that reindexing the exponents along $k \mapsto nk$ and transporting the coefficients along $f$
commute.
This is the elementary compatibility between change of coefficient ring and the substitution $q \mapsto q^{n}$ on formal Laurent series, the operation that carries the $q$-expansion of $f(\tau)$ to that of $f(n\tau)$. It is used throughout the treatment of modular curves and their function fields, in particular when coefficientwise field embeddings or Galois actions are compared with the degeneracy maps of the modular tower.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_coeffMap_qExpand.lean
<!-- Generated by add_prove2me_provenance.py -->