The j-expansion over any commutative ring, and K(j(q),j(qN)) #

Definition: ModularCurve_JqCoeff (21e203b4-817f-5557-90de-372a2e28e137), by Claude, 2026-09-05.

Two pieces of coefficient bookkeeping for the formal $q$-expansion of the modular $j$-invariant, carried out inside Laurent series rather than on any curve.

First, for any commutative ring $K$, ModularCurve.jqModC K : LaurentSeries K is defined as HahnSeries.single (-1) 1 * HahnSeries.ofPowerSeries ℤ K (jNum.map (Int.castRingHom K)): the integral power series jNum of the imported module has its coefficients pushed along the unique ring map $\mathbb{Z} \to K$ and the result is shifted by $q^{-1}$, so that one obtains $q^{-1} + 744 + 196884\,q + \cdots$ read in $K$. By construction this is definitionally the project's rational series jq when $K = \mathbb{Q}$ (jqModC_rat, proved by rfl), and it commutes with arbitrary change of coefficients: map_jqModC states (jqModC K).map f = jqModC K' for every ring homomorphism $f : K \to K'$, whence jqModC_eq_map_intCast : jqModC K = (jqModC ℤ).map (Int.castRingHom K). For $N$ with NeZero N, jqNModC K N := qExpand K N (jqModC K) is the substitution $q \mapsto q^N$ applied to this series, i.e. $j(q^N)$, with jqNModC_one recording $N = 1$.

Second, for a field $K$ and $N \geq 1$, ModularCurve.modularFunctionFieldC K N is the intermediate field IntermediateField.adjoin K {jqModC K, jqNModC K N} of $K((q))$, that is $K(j(q), j(q^N))$ generated by the two displayed Laurent series; jqModC_mem and jqNModC_mem record that the two generators lie in it, modularFunctionFieldC_one that for $N = 1$ it is the single-generator field, and modularFunctionFieldC_rat that over $\mathbb{Q}$ it is definitionally the two-generator field modularFunctionField N of the imported module (not the full modular function field). No property of these series — order of the pole, non-vanishing, transcendence, Frobenius identities in characteristic $\ell$ — is asserted here; the module is purely definitional.

Relation to Mathlib. Built on Mathlib's LaurentSeries/HahnSeries and IntermediateField.adjoin; Mathlib has no $q$-expansion of $j$ with coefficients in an arbitrary commutative ring, so jqModC and the field it generates are the project's own, defined by transporting the project's integral series jNum along $\mathbb{Z} \to K$.

Where it is used. These series provide the single definition of 'the $j$-expansion with coefficients in $K$' used throughout the project, allowing the characteristic-zero and characteristic-$\ell$ situations (e.g. $K = \mathbb{Z}$, $K = \mathbb{Q}$, $K = \mathbb{Z}/\ell$) to be compared through a common formula, and the fields $K(j(q),j(q^N))$ serve as the function-field model of the modular curve $X_0(N)$ used in the algebraic construction of modular curves and their Jacobians.

source