Function fields of X1(M) via q-expansions, and J1(M) #

Definition: ModularCurve_X1 (a97393e1-e3b4-528c-899e-0baec08e606f), by Claude, 2026-09-05.

Work inside the Laurent series field $K((q))$ over a field $K$. A power series $p\in\mathbb Z[[q]]$ is an integral $q$-expansion of a function $f:\mathbb H\to\mathbb C$, written ModularCurve.IsIntegralQExp f p, when the image of $p$ under $\mathbb Z\to\mathbb C$ equals Mathlib's qExpansion 1 f, the $q$-expansion of $f$ of width $1$; such a $p$ is unique, and $0$ and $1$ have the evident integral expansions. For $p\in\mathbb Z[[q]]$, intSeriesC K p denotes the Laurent series obtained by reducing the coefficients along $\mathbb Z\to K$; it is multiplicative and unital. For a subgroup $\Gamma\le\mathrm{SL}_2(\mathbb Z)$, intFormRatiosC K Γ is the set of quotients $\mathrm{intSeriesC}\,p_f/\mathrm{intSeriesC}\,p_g$ in $K((q))$ where, for some weight $k\in\mathbb Z$, $f,g$ are modular forms of weight $k$ for the image of $\Gamma$ in $\mathrm{GL}_2(\mathbb R)$ admitting integral $q$-expansions $p_f,p_g$, with $\mathrm{intSeriesC}\,p_g\neq 0$; and qExpFunctionFieldC K Γ is the intermediate field of $K((q))/K$ generated by this set. This construction is antitone: $\Gamma'\le\Gamma$ gives $\mathrm{qExpFunctionFieldC}\,K\,\Gamma\le \mathrm{qExpFunctionFieldC}\,K\,\Gamma'$. Specialising, x1FunctionFieldC K M takes $\Gamma=\Gamma_1(M)$ (with x1FunctionField M the case $K=\mathbb Q$) and x1x0FunctionFieldC K M t takes $\Gamma_1(M)\cap\Gamma_0(t)$; the former is contained in the latter, equality holding for $t=1$, and $M\mid M'$ gives $\Gamma_1(M')\le\Gamma_1(M)$ and hence an inclusion of the corresponding fields. Finally x1FunctionFieldBar M is the compositum of $\overline{\mathbb Q}$ with x1FunctionField M inside $\overline{\mathbb Q}((q))$, JOne M is its degree-zero divisor class group $\mathrm{Pic}^0$ over $\overline{\mathbb Q}$ (divisors supported on places, i.e. proper valuation subrings containing the constants that are principal ideal rings, modulo principal divisors), carrying the action of $\mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q)$ induced by coefficientwise action on Laurent series; JOne.torsionGaloisRep M n is the resulting homomorphism from that Galois group to $\mathbb Z/n$-linear endomorphisms of the $n$-torsion of $\mathrm{Pic}^0$. JOneC M K is the same $\mathrm{Pic}^0$ over an arbitrary base field $K$.

Relation to Mathlib. Mathlib supplies ModularForm, the congruence subgroups $\Gamma_0,\Gamma_1$ and the $q$-expansion qExpansion; the integrality predicate for $q$-expansions, the realisation of modular function fields as intermediate fields of $K((q))$, and the divisor-class group $\mathrm{Pic}^0$ of a field over a base field with its semilinear Galois action are the project's own.

Where it is used. The field x1FunctionField M is the model of the modular curve $X_1(M)$ used throughout, and JOne M plays the role of the Jacobian $J_1(M)$ over $\overline{\mathbb Q}$; the representations JOne.torsionGaloisRep on its $n$-torsion are the source of the mod $\ell$ Galois representations attached to modular forms, used in level lowering and modularity lifting.

Function fields of X1​(M) via q-expansions, and J1​(M) #

Function fields of X1(M) via q-expansions, and J1(M) #