Shared modular-polynomial and Laurent-series helpers

ModularCurve.W1.TS is the Laurent series j(u q^e) over an arbitrary field, including positive characteristic. Its coefficients recover the parameters, and its substitution lemmas describe rescaling and expansion of q. Over a ℚ-algebra, TS_eq_coeffEmb identifies it with the coefficientwise image of the rational series.

ModularCurve.W1.phiAtSeed specializes the first variable of a modular polynomial. The accompanying lemmas preserve monicity and degree and transport specialization and roots along ring homomorphisms.

Further helpers identify the rational and arbitrary-field series, specialize modular equations, and count primitive slots, whose number is Dedekind's ψ function. These are shared by the minimal-polynomial and prime-level nonmembership proofs.

noncomputable def ModularCurve.W1.TS (K : Type u_2) [Field K] (e : ℕ) [NeZero e] (u : Kˣ) : LaurentSeries K

The twisted and expanded j-series obtained by applying qTwist u and then qExpand e.

Equations

• ModularCurve.W1.TS K e u = (ModularCurve.qExpand K e) ((ModularCurve.qTwist u) (ModularCurve.jqModC K))

theorem ModularCurve.W1.TS_coeff_neg {K : Type u_1} [Field K] (e : ℕ) [NeZero e] (u : Kˣ) : (TS K e u).coeff (-↑e) = ↑u⁻¹

theorem ModularCurve.W1.TS_coeff_of_lt {K : Type u_1} [Field K] (e : ℕ) [NeZero e] (u : Kˣ) {k : ℤ} (hk : k < -↑e) : (TS K e u).coeff k = 0

theorem ModularCurve.W1.TS_ne_zero {K : Type u_1} [Field K] (e : ℕ) [NeZero e] (u : Kˣ) : TS K e u ≠ 0

theorem ModularCurve.W1.TS_injective {K : Type u_1} [Field K] {e e' : ℕ} [NeZero e] [NeZero e'] {u u' : Kˣ} (h : TS K e u = TS K e' u') : e = e' ∧ u = u'

theorem ModularCurve.W1.qTwist_TS {K : Type u_1} [Field K] (v : Kˣ) (e : ℕ) [NeZero e] (u : Kˣ) : (qTwist v) (TS K e u) = TS K e (v ^ ↑e * u)

theorem ModularCurve.W1.qExpand_TS {K : Type u_1} [Field K] (m e : ℕ) [NeZero m] [NeZero e] (u : Kˣ) : (qExpand K m) (TS K e u) = TS K (m * e) u

theorem ModularCurve.W1.TS_congr {K : Type u_1} [Field K] {e e' : ℕ} [NeZero e] [NeZero e'] (h : e = e') (u : Kˣ) : TS K e u = TS K e' u

theorem ModularCurve.W1.TS_eq_coeffEmb {K : Type u_1} [Field K] [Algebra ℚ K] (e : ℕ) [NeZero e] (u : Kˣ) : TS K e u = (qExpand K e) ((qTwist u) ((coeffEmb K) jq))

noncomputable def ModularCurve.W1.phiAtSeed {R : Type u_2} [CommRing R] {n : ℕ} [NeZero n] (data : ModularPolynomialData n) (x : R) : Polynomial R

The polynomial in the second variable obtained by specializing the modular polynomial's first variable at the supplied seed.

Equations

• ModularCurve.W1.phiAtSeed data x = Polynomial.map (Polynomial.eval₂RingHom (Int.castRingHom R) x) data.Φ

theorem ModularCurve.W1.phiAtSeed_map {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] {n : ℕ} [NeZero n] (data : ModularPolynomialData n) (x : R) (f : R →+* S) : Polynomial.map f (phiAtSeed data x) = phiAtSeed data (f x)

theorem ModularCurve.W1.phiAtSeed_monic {R : Type u_2} [CommRing R] {n : ℕ} [NeZero n] (data : ModularPolynomialData n) (x : R) : (phiAtSeed data x).Monic

theorem ModularCurve.W1.phiAtSeed_natDegree {R : Type u_2} [CommRing R] [Nontrivial R] {n : ℕ} [NeZero n] (data : ModularPolynomialData n) (x : R) : (phiAtSeed data x).natDegree = dedekindPsi n

theorem ModularCurve.W1.phiAtSeed_eval_map {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] {n : ℕ} [NeZero n] (data : ModularPolynomialData n) (x y : R) (f : R →+* S) (h : Polynomial.eval y (phiAtSeed data x) = 0) : Polynomial.eval (f y) (phiAtSeed data (f x)) = 0

Series identities and roots of unity

theorem ModularCurve.ModularPolynomialHelpers.qExpand_jqNModC {K : Type u_1} [Field K] (A d : ℕ) [NeZero A] [NeZero d] : (qExpand K A) (jqNModC K d) = W1.TS K (A * d) 1

theorem ModularCurve.ModularPolynomialHelpers.qExpand_jqModC_eq_TS {K : Type u_1} [Field K] (A : ℕ) [NeZero A] : (qExpand K A) (jqModC K) = W1.TS K A 1

theorem ModularCurve.ModularPolynomialHelpers.isPrimitiveRoot_pow_div {K : Type u_1} [Field K] {N : ℕ} [NeZero N] {ζ : Kˣ} (hζ : IsPrimitiveRoot (↑ζ) N) {p : ℕ} (hpN : p ∣ N) : IsPrimitiveRoot (↑(ζ ^ (N / p))) p

theorem ModularCurve.ModularPolynomialHelpers.TS_congr' {K : Type u_1} [Field K] {e e' : ℕ} [NeZero e] [NeZero e'] {u u' : Kˣ} (he : e = e') (hu : u = u') : W1.TS K e u = W1.TS K e' u'

theorem ModularCurve.ModularPolynomialHelpers.jqNModC_congr {K : Type u_1} [Field K] {n m : ℕ} [NeZero n] [NeZero m] (h : n = m) : jqNModC K n = jqNModC K m

theorem ModularCurve.ModularPolynomialHelpers.iota_jqN {K : Type u_1} [Field K] [Algebra ℚ K] (N d : ℕ) [NeZero N] [NeZero d] : (coeffEmb K) ((qExpand ℚ N) (jqN d)) = W1.TS K (N * d) 1

noncomputable def ModularCurve.ModularPolynomialHelpers.cycUnit (N : ℕ) [NeZero N] : (CyclotomicField N ℚ)ˣ

A chosen primitive Nth root of unity in the cyclotomic field, bundled as a unit.

Equations

• ModularCurve.ModularPolynomialHelpers.cycUnit N = ⋯.unit

theorem ModularCurve.ModularPolynomialHelpers.cycUnit_spec (N : ℕ) [NeZero N] : IsPrimitiveRoot (↑(cycUnit N)) N

theorem ModularCurve.ModularPolynomialHelpers.jqN_congr {n m : ℕ} [NeZero n] [NeZero m] (h : n = m) : jqN n = jqN m

Specialization of modular equations

theorem ModularCurve.ModularPolynomialHelpers.phiAtSeed_jqNModC_eval {R : Type u_2} [CommRing R] (n : ℕ) [NeZero n] (data : ModularPolynomialData n) (d : ℕ) [NeZero d] : Polynomial.eval (jqNModC R (d * n)) (W1.phiAtSeed data (jqNModC R d)) = 0

theorem ModularCurve.ModularPolynomialHelpers.phiAtSeed_jqNModC_eval_symm {R : Type u_2} [CommRing R] (n : ℕ) [NeZero n] (data : ModularPolynomialData n) (hsymm : EvalSymm data.Φ) (d : ℕ) [NeZero d] : Polynomial.eval (jqNModC R d) (W1.phiAtSeed data (jqNModC R (d * n))) = 0

theorem ModularCurve.ModularPolynomialHelpers.aeval_intermediateField_eq_zero {F₀ : Type u_2} {L : Type u_3} [Field F₀] [Field L] [Algebra F₀ L] {E : IntermediateField F₀ L} {P : Polynomial F₀} {x : ↥E} (h : (Polynomial.aeval (E.val x)) P = 0) : (Polynomial.aeval x) P = 0

theorem ModularCurve.ModularPolynomialHelpers.phiAtSeed_eval_of_injective {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] {n : ℕ} [NeZero n] (data : ModularPolynomialData n) (x y : R) (f : R →+* S) (hf : Function.Injective ⇑f) (h : Polynomial.eval (f y) (W1.phiAtSeed data (f x)) = 0) : Polynomial.eval y (W1.phiAtSeed data x) = 0

theorem ModularCurve.ModularPolynomialHelpers.phiAtSeed_jqN_eval (n : ℕ) [NeZero n] (data : ModularPolynomialData n) (M : ℕ) [NeZero M] : Polynomial.eval (jqN (M * n)) (W1.phiAtSeed data (jqN M)) = 0

theorem ModularCurve.ModularPolynomialHelpers.phiAtSeed_eval_symm {n : ℕ} [NeZero n] (data : ModularPolynomialData n) (hsym : EvalSymm data.Φ) (x y : LaurentSeries ℚ) : Polynomial.eval y (W1.phiAtSeed data x) = Polynomial.eval x (W1.phiAtSeed data y)

Counting primitive slots

def ModularCurve.ModularPolynomialHelpers.slotAt (n d : ℕ) : ℕ

Count residues b modulo d for which the triple (n / d, b, d) is primitive.

Equations

• ModularCurve.ModularPolynomialHelpers.slotAt n d = {b ∈ Finset.range d | ((n / d).gcd b).gcd d = 1}.card

def ModularCurve.ModularPolynomialHelpers.slots (n : ℕ) : ℕ

The total number of primitive coset slots, summed over divisors of the level.

Equations

• ModularCurve.ModularPolynomialHelpers.slots n = ∑ d ∈ n.divisors, ModularCurve.ModularPolynomialHelpers.slotAt n d

theorem ModularCurve.ModularPolynomialHelpers.slots_eq_dedekindPsi (n : ℕ) : n ≠ 0 → slots n = dedekindPsi n

theorem ModularCurve.ModularPolynomialHelpers.dedekindPsi_mul_prime_not_dvd {m p : ℕ} (hp : Nat.Prime p) (hpm : ¬p ∣ m) : dedekindPsi (m * p) = dedekindPsi m * (p + 1)

theorem ModularCurve.ModularPolynomialHelpers.dedekindPsi_mul_prime_dvd {m p : ℕ} (hm : m ≠ 0) (hp : Nat.Prime p) (hpm : p ∣ m) : dedekindPsi (m * p) = dedekindPsi m * p