Shared modular-function-field helpers

Embeddings of simple algebraic extensions are constructed from roots of minimal polynomials, and evaluation is transported along ring homomorphisms. The field-membership lemmas pass between the two-generator description of a modular function field and adjoining j(qᴺ) over the field generated by j(q), over either an arbitrary coefficient field or ℚ.

The Laurent-series slots are defined over any field; coefficient-embedding formulas recover the rational presentation over a ℚ-algebra. Their injectivity proof is shared across both cases.

The two-coefficient-field factorization theorem below covers both the same-field and rational versions of the minimal-polynomial factorization. Its prime-step induction is split into slot separation, extension-degree, modular-equation, and root-counting arguments.

The same two-field setup gives coprime-prime membership descent: adjoining j(qᴹ) cannot add j(qᵖ) to the base j-field when p does not divide M. A common q-substitution places all conjugates in the p-expanded subfield; the prime modular equation then singles out one possible image of j(qᵖ), and polynomial interpolation descends it to the source j-field.

theorem ModularCurve.ModularFunctionFieldHelpers.mem_adjoin_jqNModC_of_mem_mffC {K : Type u_1} [Field K] {M : ℕ} [NeZero M] {x : LaurentSeries K} (hx : x ∈ modularFunctionFieldC K M) : x ∈ (↥K⟮jqModC K⟯)⟮jqNModC K M⟯

theorem ModularCurve.ModularFunctionFieldHelpers.mem_adjoin_jqN_of_mem_mff {M : ℕ} [NeZero M] {x : LaurentSeries ℚ} (hx : x ∈ modularFunctionField M) : x ∈ (↥ℚ⟮jq⟯)⟮jqN M⟯

Laurent-series slots

noncomputable def ModularCurve.ModularFunctionFieldHelpers.sv (K : Type u_2) [Field K] (ζ : Kˣ) (a b : ℕ) : LaurentSeries K

The slot j(ζ^(ab)q^(a²)), extended by zero when a = 0.

Equations

• ModularCurve.ModularFunctionFieldHelpers.sv K ζ a b = if h : a = 0 then 0 else ModularCurve.W1.TS K (a * a) (ζ ^ (b * a))

Coefficient transport

Polynomial and field-extension lemmas

Minimal-polynomial factorization

theorem ModularCurve.ModularFunctionFieldHelpers.minpoly_map_eq_prod_slots {K : Type u_1} [Field K] {k : Type u_2} [Field k] (ι : k →+* K) (M : ℕ) [NeZero M] (ζ : Kˣ) (hζ : IsPrimitiveRoot (↑ζ) M) (hall : ∀ (d : ℕ), d ∣ M → ∀ [inst : NeZero d], Module.finrank ↥k⟮jqModC k⟯ ↥(↥k⟮jqModC k⟯)⟮jqNModC k d⟯ = dedekindPsi d ∧ modularFunctionFieldC k d = IntermediateField.adjoin k {x : LaurentSeries k | ∃ (d' : ℕ) (x_1 : NeZero d'), d' ∣ d ∧ x = jqNModC k d'}) : Polynomial.map (((coeffMap ι).comp (qExpand k M)).comp (algebraMap (↥k⟮jqModC k⟯) (LaurentSeries k))) (minpoly (↥k⟮jqModC k⟯) (jqNModC k M)) = ∏ a ∈ M.divisors, ∏ b ∈ Finset.range (M / a) with (a.gcd b).gcd (M / a) = 1, (Polynomial.X - Polynomial.C (sv K ζ a b))

The conjugates of j(qᴹ) are exactly the primitive Laurent-series slots.

The degree and generation hypotheses concern the source coefficient field k; the primitive root of unity may lie in any target field K receiving a coefficient homomorphism from k. Thus both the same-field and rational-coefficient factorizations are special cases.

Coprime-prime membership descent

theorem ModularCurve.ModularFunctionFieldHelpers.jqNModC_mem_adjoin_iff_mem_base_of_prime_not_dvd {K : Type u_1} [Field K] {k : Type u_2} [Field k] (ι : k →+* K) (M : ℕ) [NeZero M] (p : ℕ) [hp : Fact (Nat.Prime p)] (hpM : ¬p ∣ M) (ζ : Kˣ) (hζ : IsPrimitiveRoot (↑ζ) (M * p)) (hall : ∀ (d : ℕ), d ∣ M → ∀ [inst : NeZero d], Module.finrank ↥k⟮jqModC k⟯ ↥(↥k⟮jqModC k⟯)⟮jqNModC k d⟯ = dedekindPsi d ∧ modularFunctionFieldC k d = IntermediateField.adjoin k {x : LaurentSeries k | ∃ (d' : ℕ) (x_1 : NeZero d'), d' ∣ d ∧ x = jqNModC k d'}) : jqNModC k p ∈ (↥k⟮jqModC k⟯)⟮jqNModC k M⟯ ↔ jqNModC k p ∈ k⟮jqModC k⟯

A prime degeneracy generator away from the level belongs to the level-M simple extension exactly when it already belongs to the base j-field.

The degree and generation assumptions are over the source field k; the root of unity may lie in any target coefficient field K receiving the homomorphism ι.