Function field of X0(N) inside Q((q)) #

Definition: ModularCurve_X0 (23b22550-cc5b-5ca8-a5e3-1c4c7dd76b29), by Claude, 2026-09-05.

The module presents the modular curve $X_0(N)$ over $\mathbb{Q}$ by its function field, realised concretely inside the formal Laurent series field LaurentSeries ℚ $=\mathbb{Q}((q))$. For a coefficient ring $R$ and $N\neq 0$, qExpand R N is the ring endomorphism of LaurentSeries R obtained by embedding the index domain along $k\mapsto Nk$, i.e. the substitution $q\mapsto q^{N}$; it is injective, is the identity for $N=1$, fixes constants, and composes as qExpand M ∘ qExpand N = qExpand (M*N). Over $\mathbb{Q}$ the same map is packaged as the algebra endomorphism qExpandₐ N. The $q$-expansion of the $j$-invariant is built integrally: eisenstein4 is the power series with constant term $1$ and $n$-th coefficient $240\sum_{d\mid n}d^{3}$; etaProd $=\prod_{n\ge 1}(1-q^{n})$ (an infinite product in the product topology on power series); dedekindEtaUnit is its $24$-th power, with constant term $1$, and dedekindEtaUnitInv its power-series inverse. Then jNum $=E_4^{3}\prod_{n\ge1}(1-q^{n})^{-24}$ over $\mathbb{Z}$, jNumQ its image over $\mathbb{Q}$, and jq $=q^{-1}E_4^{3}\prod_{n\ge1}(1-q^{n})^{-24}$; the coefficient lemmas record that jq has leading term $q^{-1}$ with coefficient $1$ and vanishes below, and that jq ≠ 0. Further, jqN N $=$ qExpand ℚ N jq, i.e. $j(q^{N})$.

The fields are modularFunctionField N $=\mathbb{Q}(j(q),j(q^{N}))$ and modularFunctionFieldFull N, the subfield generated by divisorExpansions N $=\{j(q^{d}) : 0\neq d\mid N\}$; there are the containments $\mathbb{Q}(j)\le$ modularFunctionField N $\le$ modularFunctionFieldFull N, monotonicity of the full field in $N$ under divisibility, and $(q\mapsto q^{\ell})$ sends modularFunctionFieldFull N into modularFunctionFieldFull (N*ℓ). Two inputs are isolated rather than proved. ModularPolynomialData N is a structure carrying a polynomial $\Phi\in(\mathbb{Z}[X])[Y]$ together with proofs that it is monic, that its degree in $Y$ equals dedekindPsi N $=\sum_{d\mid N,\,d\text{ squarefree}}N/d$, and that $\Phi(j(q),j(q^{N}))=0$ under evalAtJ : ℤ[X] →+* ℚ((q)), $X\mapsto j(q)$; only the level-one instance $\Phi=Y-X$ is constructed. FunctionFieldGeneration M is the proposition that $j(q^{d})\in\mathbb{Q}(j(q),j(q^{M}))$ for every nonzero $d\mid M$, proved here only for $M=1$. Auxiliary items jGen, evalAtJGen and ModularPolynomialData.toAdjoin read $\Phi$ as a monic polynomial over $\mathbb{Q}(j(q))$.

Relation to Mathlib. Mathlib has no modular curve, modular polynomial or Dedekind psi function; these are the project's own definitions, built on Mathlib's HahnSeries/LaurentSeries API (embDomainRingHom, ofPowerSeries), on PowerSeries.invOfUnit and on infinite products in the product topology on power series.

Where it is used. This is the curve layer of an algebraic presentation of $X_0(N)$ over $\mathbb{Q}$ by its function field, on which the later construction of $J_0(N)$ and its Hecke action rests; by itself it says nothing about Jacobians or Galois representations. The modular polynomial data and the generation predicate are carried as hypotheses by the statements that use them, with only the level-one cases constructed here.

Function field of X0​(N) inside Q((q)) #

Function field of X0(N) inside Q((q)) #