Division polynomials of the universal curve

Every Weierstrass curve is a specialization of the universal one, and division polynomials commute with base change. Composing the two identifies the division polynomials of a curve W over R, evaluated at a point (x, y) of the affine plane, with those of Universal.curve pushed forward along Universal.polyEval.

Each proof is the same two steps: unfold polyEval into a map followed by evalEval (polyEval_apply), then rewrite the base change of the universal curve back to W (map_specialize). The division polynomial in between is carried across by the relevant Mathlib map_* lemma.

Main results

• WeierstrassCurve.Universal.evalEval_ψ₂, .evalEval_Ψ₃, .evalEval_preΨ₄, .evalEval_ψ, .evalEval_φ, .evalEval_ω, .evalEval_ψc: the polynomials ψ₂, Ψ₃, ψₙ, φₙ, ωₙ and the complement ψc n of W at (x, y), together with the auxiliary preΨ₄, are the universal ones evaluated through Universal.polyEval.
• WeierstrassCurve.Universal.isEllipticNet_polyToField_ψ: the universal ψ family, taken into Universal.Field, is an elliptic net.
• WeierstrassCurve.Universal.polyEval_cusp_ψ, .polyEval_cusp_φ, .polyEval_cusp_ψc, .polyEval_cusp_ω: specialised to the cusp curve at (1, 1), ψₙ evaluates to n itself, the numerator φₙ to 1, the complement ψc n to 2, and ωₙ to 1.
• WeierstrassCurve.Universal.polyToField_ψ_ne_zero, .polyToField_φ_ne_zero: in Universal.Field, ψₙ is nonzero for every n ≠ 0 and φₙ for every n — the cusp evaluations above, read back through the retraction onto ℤ.
• WeierstrassCurve.Universal.polyToField_Ψ₂Sq: Ψ₂Sq is the square of ψ 2 in the universal field, the Weierstrass relation being exactly what Universal.Ring quotients out.

Implementation notes

Ψ₃ and preΨ₄ are univariate, so their statements evaluate C W.Ψ₃ rather than W.Ψ₃; the two extra rewrites in those proofs (map_C, coe_mapRingHom) only move that C past the base change.

polyEval_cusp_ψ is where the three transport lemmas above earn their keep. Cusp.lean collapses ψ₂, Ψ₃ and preΨ₄ on cusp R to 2Y, 3X⁴ and 2X⁶; rewriting the transports backwards turns polyEval (cusp ℤ) 1 1 (curve.ψ n) into those three evaluated at (1, 1), which are 2, 3 and 2 — so the sequence is normEDS 2 3 2, and the identity of #3364 finishes it. That is the only reason this file imports Cusp.lean.

polyEval_cusp_φ does not port as written, and the reason is the module system rather than a missing prerequisite. The source closes it with simp_rw [φ, map_sub, …, polyEval], unfolding polyEval's definition, which is rejected across a module boundary — "Invalid simp theorem polyEval: Expected a definition with an exposed body". Supplying the equation lemma instead does not help either: polyEval's image lives in Poly, whose Sub and Mul instances are themselves unexposed, so a bare map_sub cannot solve ?f in the pattern ?f (?a - ?b) and fails to fire at all. Naming the ring hom is what fixes it — map_sub (polyEval (cusp ℤ) 1 1) makes the match first-order, and the same for map_mul and map_pow. That leaves the arithmetic polyEval (cusp ℤ) 1 1 (C X) * n ^ 2 - (n + 1) * (n - 1) = 1, which ring closes once C X evaluates to 1.

The remaining two companions, polyEval_cusp_ψc and polyEval_cusp_ω, together with the sixth and seventh transports evalEval_ψc and evalEval_ω, needed ψc, two_mul_ω, map_ψc and map_ω — the ω API this passage once recorded as not yet here. DivisionPolynomial/Omega.lean now supplies all four, on top of reducedInvarNum_eq_reducedInvarDenom_mul, so they are below: evalEval_ψc and evalEval_ω close the transport family, polyEval_cusp_ψc reads the complement off complEDS₂_two_three_two, and polyEval_cusp_ω divides the cusp evaluation of two_mul_ω by two.

Provenance

Adapted from LutzNagell/ZSMul.lean in AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), at dev/modular-curves @ 9fec8eba7652 — the revision TauCetiRoadmap/EllipticCurves/README.md pins for the NagellLutz project. Declarations Universal.evalEval_ψ₂, evalEval_Ψ₃, evalEval_preΨ₄, evalEval_ψ, evalEval_φ and (added with the ω port, read at main @ 1c1c74664e40071c2c2165bc55ca2616a67ccd6b) evalEval_ψc and evalEval_ω. isEllipticNet_polyToField_ψ adapts that same file's net_ψᵤ (:140); the source's neighbouring isEllSequence_ψᵤ (:139) is the s = 0 shift of it and is not separately ported, since IsEllipticNet.isEllipticSequence recovers it. That file's header reads Authors: David Kurniadi Angdinata, Junyan Xu; following this repository's convention for adapted material the upstream authorship is credited here rather than in the copyright header.

polyEval_cusp_ψ and polyEval_cusp_φ adapt that same file's declarations of those names, at the roadmap's NagellLutz pin dev/modular-curves @ 9fec8eba7652. Three changes. ψ and φ need qualifying, because this file opens Universal rather than WeierstrassCurve alone. The source's normEDS_two_three_two hint is dropped rather than renamed — normEDS_two_three_two_eq_id is redundant here, since #3364's general normEDS_two_three_two_eq_intCast is @[simp] and reaches the same normal form first. And polyEval_cusp_φ's proof is restructured for the reason given above: the source's unfold of polyEval is unavailable, so each map_* names its ring hom. The source's polyEval_cusp_ψc and polyEval_cusp_ω are adapted below (read at main @ 1c1c74664e40071c2c2165bc55ca2616a67ccd6b), with the same two mechanical changes as their siblings — qualified names, ring-hom-named map_* rewrites in place of unfolding polyEval — plus ψc_def in place of unfolding ψc, whose body is likewise unexposed.

The evalEval_* statements are the source's unchanged. Docstrings are added here, and the source's shared variable {m n : ℤ} is narrowed to n: of the seven transports only evalEval_ψ, evalEval_φ, evalEval_ω and evalEval_ψc carry an index, and all four use n alone. net_ψᵤ is stated upstream through an abbrev ψᵤ and its own ψᵤ_eq_normEDS; here the abbreviation is dropped, the identification of ψ with normEDS is the named ψ_eq_normEDS (DivisionPolynomial/NormEDS.lean), and a have transports it through polyToField, so the statement is spelled on fun n ↦ polyToField (curve.ψ n) directly.

The nonvanishing block adapts, at the same main revision, ψᵤ_ne_zero (:142, respelt polyToField_ψ_ne_zero with the abbreviation dropped as above), polyToField_φ_ne_zero (:148, source name kept) and polyToField_ψ₂Sq (:154, here polyToField_Ψ₂Sq: the constant in its conclusion is Ψ₂Sq, capitalised). The first two port essentially unchanged, both retracting to the cusp curve at (1, 1) through ringEval, where ψₙ reads off as n and φₙ as 1. One departure beyond the ψᵤ respelling, and it is confined to polyToField_Ψ₂Sq: the source expands ψ₂_sq and clears the Weierstrass polynomial term by hand with polyToField_polynomial. That lemma exists here too (EllipticCurve/Universal.lean), but this proof does not need it — Mathlib packages the same cancellation as the coordinate-ring identity Affine.CoordinateRing.mk_ψ₂_sq, which is what the proof pushes into the field of fractions.

theorem WeierstrassCurve.Universal.evalEval_ψ₂ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} : Polynomial.evalEval x y W.ψ₂ = (polyEval W x y) (ψ₂ curve)

The 2-division polynomial of W at (x, y) is the universal one under polyEval.

theorem WeierstrassCurve.Universal.evalEval_Ψ₃ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} : Polynomial.evalEval x y (Polynomial.C W.Ψ₃) = (polyEval W x y) (Polynomial.C (Ψ₃ curve))

The 3-division polynomial of W at (x, y) is the universal one under polyEval.

theorem WeierstrassCurve.Universal.evalEval_preΨ₄ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} : Polynomial.evalEval x y (Polynomial.C W.preΨ₄) = (polyEval W x y) (Polynomial.C (preΨ₄ curve))

The polynomial preΨ₄ of W at (x, y) is the universal one under polyEval.

theorem WeierstrassCurve.Universal.evalEval_ψ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} {n : ℤ} : Polynomial.evalEval x y (W.ψ n) = (polyEval W x y) (WeierstrassCurve.ψ curve n)

The n-division polynomial ψₙ of W at (x, y) is the universal one under polyEval.

theorem WeierstrassCurve.Universal.evalEval_φ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} {n : ℤ} : Polynomial.evalEval x y (W.φ n) = (polyEval W x y) (WeierstrassCurve.φ curve n)

The numerator φₙ of W at (x, y) is the universal one under polyEval.

theorem WeierstrassCurve.Universal.isEllipticNet_polyToField_ψ : IsEllipticNet fun (n : ℤ) => polyToField (WeierstrassCurve.ψ curve n)

The universal ψ family is an elliptic net. Pushing ψₙ of the universal curve into Universal.Field gives a normalised EDS, hence an elliptic net — over the universal field, with no hypothesis on any coefficient.

The proof recognises the family as a normEDS outright, which is what puts the whole normEDS API — including NormEDS.lean's universalNormEDS_ne_zero — within reach of the universal division polynomials. The elliptic-sequence consequence is the shift s = 0, which IsEllipticNet.isEllipticSequence reads off; consumers that need a nonzero shift, as the addition formula for n • (X, Y) does, need the net.

theorem WeierstrassCurve.Universal.polyEval_cusp_ψ {n : ℤ} : (polyEval (cusp ℤ) 1 1) (WeierstrassCurve.ψ curve n) = n

On the cusp curve at (1, 1), the n-division polynomial evaluates to n.

theorem WeierstrassCurve.Universal.polyEval_cusp_φ {n : ℤ} : (polyEval (cusp ℤ) 1 1) (WeierstrassCurve.φ curve n) = 1

On the cusp curve at (1, 1), the numerator φₙ evaluates to 1.

theorem WeierstrassCurve.Universal.evalEval_ω {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} {n : ℤ} : Polynomial.evalEval x y (W.ω n) = (polyEval W x y) (WeierstrassCurve.ω curve n)

The ω-division polynomial of W at (x, y) is the universal one under polyEval.

theorem WeierstrassCurve.Universal.evalEval_ψc {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} {n : ℤ} : Polynomial.evalEval x y (W.ψc n) = (polyEval W x y) (WeierstrassCurve.ψc curve n)

The complement ψc n of W at (x, y) is the universal one under polyEval.

theorem WeierstrassCurve.Universal.polyEval_cusp_ψc {n : ℤ} : (polyEval (cusp ℤ) 1 1) (WeierstrassCurve.ψc curve n) = 2

On the cusp curve at (1, 1), the complement ψc n evaluates to 2.

theorem WeierstrassCurve.Universal.polyEval_cusp_ω {n : ℤ} : (polyEval (cusp ℤ) 1 1) (WeierstrassCurve.ω curve n) = 1

On the cusp curve at (1, 1), ω n evaluates to 1.

theorem WeierstrassCurve.Universal.polyToField_ψ_ne_zero {n : ℤ} (h0 : n ≠ 0) : polyToField (WeierstrassCurve.ψ curve n) ≠ 0

The universal ψₙ is nonzero in Universal.Field for every n ≠ 0. Evaluating at the cusp curve's point (1, 1) retracts the universal coefficients onto ℤ, where ψₙ reads off as n itself (polyEval_cusp_ψ) — so ψₙ = 0 would force n = 0. This is the nonvanishing the n • (X, Y) coordinate formulas divide by.

theorem WeierstrassCurve.Universal.polyToField_φ_ne_zero {n : ℤ} : polyToField (WeierstrassCurve.φ curve n) ≠ 0

The universal φₙ is nonzero in Universal.Field, for every n. The same cusp retraction: at (1, 1) it evaluates to 1 (polyEval_cusp_φ).

theorem WeierstrassCurve.Universal.polyToField_Ψ₂Sq : polyToField (Polynomial.C (Ψ₂Sq curve)) = polyToField (WeierstrassCurve.ψ curve 2) ^ 2

Ψ₂Sq in the universal field is the square of ψ 2: the coordinate-ring identity mk_ψ₂_sq, pushed into the field of fractions.