j-expansions and modular function fields over an arbitrary field

Definition: ModularCurve_X0ModL (8d529f3c-af58-58c3-8775-59af521964b5), by Claude, 2026-09-05.

Working inside the field of formal Laurent series $K((q))$ over a field $K$ (and, for the coefficient lemmas, inside $R((q))$ for a commutative ring $R$), this module assembles the base-changed version of the project's characteristic-zero $q$-expansion picture. The series jqModC R of the imported definition module is $q^{-1}$ times the image in $R[[q]]$ of the integral power series jNum $= E_4^3\cdot\prod_{n\ge 1}(1-q^n)^{-24}$, and jqNModC R N is its image under $q\mapsto q^N$. The lemmas record that coefficientwise application of a ring homomorphism $f\colon R\to S$ sends ofPowerSeries to ofPowerSeries of the mapped power series, sends jqModC R to jqModC S and jqNModC R N to jqNModC S N; that every coefficient of jqModC R is the image of the corresponding integer coefficient of jqModC ℤ; that jqModC R ^ n equals $q^{-n}$ times the $n$-th power of the mapped jNum; that the coefficients in degrees $< -1$ vanish; and that jqModC R is non-zero when $R$ is non-trivial. Over $\mathbb{Q}$ these objects are the rational ones already defined: jqNModC ℚ N = jqN N.

Three definitions are made. First, qExpandAlgHomC K N upgrades the substitution ring homomorphism $q\mapsto q^N$ on $K((q))$ to a $K$-algebra homomorphism, the constants $\mathrm{single}\;0\;c$ being fixed. Second, divisorExpansionsC K N is the set of Laurent series $\bar j_K(q^d)$ for the non-zero divisors $d$ of $N$, and modularFunctionFieldFullC K N is the intermediate field of $K((q))/K$ generated by this set; at $K=\mathbb{Q}$ it is the field modularFunctionFieldFull N. The accompanying inclusions state that the two-generator field modularFunctionFieldC K N lies in it, that $N \mid M$ gives modularFunctionFieldFullC K N ≤ modularFunctionFieldFullC K M, and that the image of modularFunctionFieldFullC K N under qExpandAlgHomC K ℓ lies in modularFunctionFieldFullC K (N * ℓ). Third, JZeroC K N is the group $\mathrm{Pic}^0$ of that field over $K$: degree-zero divisors supported on the places of modularFunctionFieldFullC K N (valuation subrings containing $K$, proper, with principal ideals; degree of a place the residue-field degree over $K$) modulo principal divisors. No identification with $X_0(N)$ or its Jacobian is asserted here; only the carriers are built, for a field $K$ of any characteristic.

Relation to Mathlib. Mathlib supplies the ambient $K((q))$ as Hahn series over $\mathbb{Z}$ and the substitution homomorphism through HahnSeries.embDomain; the modular function field presented as a subfield of a Laurent series field, and the divisor class group attached to it, are the project's own notions.

Where it is used. These carriers over a field of characteristic $\ell \nmid N$ are the targets of the reduction map on $J_0(N)$ and of the Eichler–Shimura relation on the special fibre, which enter the level-lowering step of the route to Fermat's Last Theorem.

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

theorem ModularCurve.coeffMap_ofPowerSeries {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (p : PowerSeries R) : (coeffMap f) ((HahnSeries.ofPowerSeries ℤ R) p) = (HahnSeries.ofPowerSeries ℤ S) ((PowerSeries.map f) p)

theorem ModularCurve.jqNModC_rat (N : ℕ) [NeZero N] : jqNModC ℚ N = jqN N

theorem ModularCurve.coeffMap_jqModC {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) : (coeffMap f) (jqModC R) = jqModC S

theorem ModularCurve.coeffMap_jqNModC {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (N : ℕ) [NeZero N] : (coeffMap f) (jqNModC R N) = jqNModC S N

theorem ModularCurve.coeff_jqModC_eq_intCast {R : Type u_1} [CommRing R] (k : ℤ) : (jqModC R).coeff k = ↑((jqModC ℤ).coeff k)

theorem ModularCurve.jqModC_pow (R : Type u_1) [CommRing R] (n : ℕ) : jqModC R ^ n = (HahnSeries.single (-↑n)) 1 * (HahnSeries.ofPowerSeries ℤ R) ((PowerSeries.map (Int.castRingHom R)) jNum ^ n)

theorem ModularCurve.coeff_jqModC_of_lt (R : Type u_1) [CommRing R] {k : ℤ} (hk : k < -1) : (jqModC R).coeff k = 0

theorem ModularCurve.jqModC_ne_zero_of_nontrivial (R : Type u_1) [CommRing R] [Nontrivial R] : jqModC R ≠ 0

noncomputable def ModularCurve.qExpandAlgHomC (K : Type u_1) [Field K] (N : ℕ) [NeZero N] : LaurentSeries K →ₐ[K] LaurentSeries K

The constant-field algebra endomorphism of Laurent series given by q ↦ q^N.

Equations

• ModularCurve.qExpandAlgHomC K N = { toRingHom := ModularCurve.qExpand K N, commutes' := ⋯ }

@[simp]

theorem ModularCurve.qExpandAlgHomC_apply (K : Type u_1) [Field K] (N : ℕ) [NeZero N] (f : LaurentSeries K) : (qExpandAlgHomC K N) f = (qExpand K N) f

def ModularCurve.divisorExpansionsC (K : Type u_1) [Field K] (N : ℕ) : Set (LaurentSeries K)

The expansions j(q^d) for nonzero divisors d of the level.

Equations

• ModularCurve.divisorExpansionsC K N = {x : LaurentSeries K | ∃ (d : ℕ) (x_1 : NeZero d), d ∣ N ∧ x = (ModularCurve.qExpand K d) (ModularCurve.jqModC K)}

theorem ModularCurve.mem_divisorExpansionsC (K : Type u_1) [Field K] (N : ℕ) {d : ℕ} [NeZero d] (hd : d ∣ N) : (qExpand K d) (jqModC K) ∈ divisorExpansionsC K N

noncomputable def ModularCurve.modularFunctionFieldFullC (K : Type u_1) [Field K] (N : ℕ) : IntermediateField K (LaurentSeries K)

The intermediate field generated by the divisor-indexed expansions j(q^d) over the coefficient field.

Equations

• ModularCurve.modularFunctionFieldFullC K N = IntermediateField.adjoin K (ModularCurve.divisorExpansionsC K N)

theorem ModularCurve.modularFunctionFieldFullC_rat (N : ℕ) : modularFunctionFieldFullC ℚ N = modularFunctionFieldFull N

theorem ModularCurve.jqModCd_mem_full (K : Type u_1) [Field K] (N : ℕ) {d : ℕ} [NeZero d] (hd : d ∣ N) : (qExpand K d) (jqModC K) ∈ modularFunctionFieldFullC K N

theorem ModularCurve.jqModC_mem_full (K : Type u_1) [Field K] (N : ℕ) : jqModC K ∈ modularFunctionFieldFullC K N

theorem ModularCurve.modularFunctionFieldC_le_full (K : Type u_1) [Field K] (N : ℕ) [NeZero N] : modularFunctionFieldC K N ≤ modularFunctionFieldFullC K N

theorem ModularCurve.full_degeneracyC_le (K : Type u_1) [Field K] {N M : ℕ} (h : N ∣ M) : modularFunctionFieldFullC K N ≤ modularFunctionFieldFullC K M

theorem ModularCurve.full_degeneracyC_map_le (K : Type u_1) [Field K] (N ℓ : ℕ) [NeZero ℓ] : IntermediateField.map (qExpandAlgHomC K ℓ) (modularFunctionFieldFullC K N) ≤ modularFunctionFieldFullC K (N * ℓ)

@[reducible, inline]

abbrev ModularCurve.JZeroC (K : Type u_1) [Field K] (N : ℕ) : Type u_1

The degree-zero divisor-class group of the full modular function field over the specified coefficient field.

Equations

• ModularCurve.JZeroC K N = AlgebraicCurve.Pic0 K ↥(ModularCurve.modularFunctionFieldFullC K N)