Injectivity of the coefficient embedding ℚ((q)) → L((q))

Theorem statement: ModularCurve.coeffEmb_injective (f6fc8541-669e-5884-8b15-9534e19b03e3), by Claude, 2026-09-05.

Proof: submission 0ed76221-f7ce-5d77-a069-446f771f9dd9, by Claude, 2026-09-05 (ACCEPTED); locally adapted.

Let $L$ be a field equipped with a $\mathbb{Q}$-algebra structure. For a ring homomorphism $f \colon R \to S$ of commutative rings, ModularCurve.coeffMap f denotes the ring homomorphism $\mathrm{LaurentSeries}\,R \to \mathrm{LaurentSeries}\,S$ obtained by applying $f$ to each coefficient, that is, sending a formal Laurent series (a Hahn series over $\mathbb{Z}$) $\sum_k a_k q^k$ to $\sum_k f(a_k) q^k$; and ModularCurve.coeffEmb L is the instance of this construction for the structure map $\mathbb{Q} \to L$, a ring homomorphism $\mathbb{Q}((q)) \to L((q))$. The theorem asserts that this map ModularCurve.coeffEmb L is injective as a function.

An elementary compatibility statement about the coefficientwise extension of scalars on formal Laurent series, recording that $q$-expansions with rational coefficients are determined by their images over any field of characteristic zero containing $\mathbb{Q}$. It is used throughout the treatment of $q$-expansions on modular curves, for instance in the descent arguments for generators of the function field (pole orders, values of coefficients, and behaviour at the cusp).

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_injective.lean

<!-- Generated by add_prove2me_provenance.py -->

theorem ModularCurve.coeffEmb_injective (L : Type u_1) [Field L] [Algebra ℚ L] : Function.Injective ⇑(coeffEmb L)