Evaluating the division polynomials at a point of a Weierstrass curve

Mathlib relates the bivariate division polynomials ψₙ, Ψₙ, φₙ to their univariate companions ΨSqₙ, Φₙ only inside the coordinate ring R[W], as the identities Affine.CoordinateRing.mk_ψ, mk_Ψ_sq and mk_φ. This file transports those identities to honest equalities of ring elements at a point (x, y) on the curve, where evaluation Polynomial.evalEval x y factors through R[W] by Mathlib's AdjoinRoot.evalEval.

The point of doing so is that ΨSqₙ and Φₙ are univariate: on the curve, evalEval x y (ψ n) and evalEval x y (Ψ n) agree, and the square of the latter is a polynomial in x alone. That is what later lets a rational-root argument run — not here, where R is an arbitrary commutative ring and the theorem's coefficient hypotheses are not available, but downstream over a unique factorization domain, where the degrees are Mathlib's natDegree_Φ (n², over a nontrivial ring) and natDegree_ΨSq (n² - 1, needing no zero divisors and (n : R) ≠ 0; in characteristic dividing n the degree can drop). The identities below need none of those hypotheses.

Main results

• WeierstrassCurve.evalEval_ψ_eq_evalEval_Ψ, evalEval_Ψ_sq_eq_eval_ΨSq, evalEval_φ_eq_eval_Φ: the three coordinate-ring identities, evaluated.
• WeierstrassCurve.evalEval_Ψ_odd: for odd n, Ψₙ evaluates to (preΨ n).eval x, with no y left. Composed with the first bullet, simp reduces ψₙ the same way.

Everything is stated over an arbitrary commutative ring; no domain, field or ellipticity hypothesis is needed, because a coordinate-ring identity evaluates wherever the Weierstrass equation holds.

This is a prerequisite of the Nagell–Lutz integrality milestone of TauCetiRoadmap/EllipticCurves/README.md, Layer 6, item "The torsion subgroup and Nagell–Lutz", whose route the roadmap records as "division polynomials".

Provenance

Ported from the AINTLIB NagellLutz project (github.com/CBirkbeck/AINTLIB, Apache-2.0), pinned by that roadmap at dev/modular-curves @ 9fec8eba7652: LutzNagell/LutzNagellTheorem/EvalBridge.lean. That project runs against its own vendored copy of Mathlib's division polynomials; here the statements are rebased onto pinned Mathlib's WeierstrassCurve.{ψ, Ψ, ΨSq, φ, Φ, preΨ} and generalised from a field to a commutative ring.

@[simp]

theorem WeierstrassCurve.evalEval_ψ_eq_evalEval_Ψ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} (h : W.toAffine.Equation x y) (n : ℤ) : Polynomial.evalEval x y (W.ψ n) = Polynomial.evalEval x y (W.Ψ n)

The division polynomials ψₙ and Ψₙ evaluate equally at a point of W.

@[simp]

theorem WeierstrassCurve.evalEval_Ψ_sq_eq_eval_ΨSq {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} (h : W.toAffine.Equation x y) (n : ℤ) : Polynomial.evalEval x y (W.Ψ n) ^ 2 = Polynomial.eval x (W.ΨSq n)

At a point of W, the square of Ψₙ is the univariate ΨSqₙ evaluated at the x-coordinate.

@[simp]

theorem WeierstrassCurve.evalEval_φ_eq_eval_Φ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} (h : W.toAffine.Equation x y) (n : ℤ) : Polynomial.evalEval x y (W.φ n) = Polynomial.eval x (W.Φ n)

At a point of W, φₙ is the univariate Φₙ evaluated at the x-coordinate.

@[simp]

theorem WeierstrassCurve.evalEval_Ψ_odd {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} (n : ℤ) (hodd : ¬Even n) : Polynomial.evalEval x y (W.Ψ n) = Polynomial.eval x (W.preΨ n)

For odd n the polynomial Ψₙ carries no y, so it evaluates to (preΨ n).eval x at any point. This one needs no curve hypothesis.