Coefficientwise maps of Laurent series; base change of subfields #

Definition: ModularCurve_LaurentCoeff (df67c7d0-ce84-5e1b-8306-0205c75872d3), by Claude, 2026-09-05.

Working in $\mathrm{LaurentSeries}\,R = \mathrm{HahnSeries}\,\mathbb{Z}\,R$, the module supplies three pieces of vocabulary. First, for commutative rings $R, S$ and a ring homomorphism $f : R \to S$, coeffMap f : LaurentSeries R →+* LaurentSeries S is Mathlib's HahnSeries.map applied coefficientwise, $\sum a_k q^k \mapsto \sum f(a_k) q^k$, packaged as a ring homomorphism; the accompanying lemmas record $(\mathrm{coeffMap}\,f\,x).\mathrm{coeff}\,k = f(x.\mathrm{coeff}\,k)$ (true by definition), the effect on single terms HahnSeries.single k r, the composition law $\mathrm{coeffMap}\,g \circ \mathrm{coeffMap}\,f = \mathrm{coeffMap}\,(g \circ f)$, the identity case, and congruence in $f$.

Second, for a field $L$: algebraMap_laurentSeries_eq_single identifies the image of $c \in L$ under the algebra map $L \to L((q))$ (Mathlib's power-series algebra structure) with the series HahnSeries.single 0 c; coeffMap_algebraMap says a coefficientwise endomorphism $\varphi : L \to L$ carries constants to constants, covering $\varphi$. When moreover $L$ is a $\mathbb{Q}$-algebra, coeffEmb L : LaurentSeries ℚ →+* LaurentSeries L is by definition $\mathrm{coeffMap}(\mathrm{algebraMap}\,\mathbb{Q}\,L)$, with its coefficient formula, and coeffMap_coeffEmb states that every $\sigma \in L \simeq_{\mathbb{Q}} L$ acting coefficientwise fixes each series in the image of coeffEmb L.

Third, for such an $L$ and an intermediate field $F_0$ of $\mathbb{Q}((q))/\mathbb{Q}$, laurentBaseChange L F₀ : IntermediateField L (LaurentSeries L) is defined as IntermediateField.adjoin L applied to the set $\mathrm{coeffEmb}_L(F_0)$, i.e. the compositum $L\cdot F_0$ inside $L((q))$. Three lemmas follow: the image of $F_0$ lies in it; membership unfolds, definitionally, to membership in the Subfield.closure of the union of the range of $\mathrm{algebraMap}\,L\,(L((q)))$ with $\mathrm{coeffEmb}_L(F_0)$; and $L\cdot F_0$ is stable under the coefficientwise action of every $\sigma \in L \simeq_{\mathbb{Q}} L$, proved by closure induction. Nothing here concerns modular curves; the material is pure field-theoretic vocabulary.

Relation to Mathlib. coeffMap bundles Mathlib's HahnSeries.map as a ring homomorphism on LaurentSeries; laurentBaseChange is an application of Mathlib's IntermediateField.adjoin, and the Algebra L (LaurentSeries L) structure used is Mathlib's power-series algebra structure. The named combinations (coeffEmb, laurentBaseChange) are the project's own abbreviations.

Where it is used. These constructions provide the coefficientwise ("arithmetic") Galois action on fields of formal $q$-expansions and the base change $F_0 \mapsto L\cdot F_0$ of a subfield of $\mathbb{Q}((q))$ to $L((q))$, used when modular function fields are presented via $q$-expansions and then extended to larger coefficient fields in the modular-curve layer feeding the study of $J_0(N)$.