The invariant polynomial of a Weierstrass curve

This file defines the polynomial

WeierstrassCurve.invar = 6 X² + b₂ X + b₄

and proves the division-polynomial identities that pin it down, together with the one identity connecting φ and ψ to IsEllipticNet.invarDenom. They are the first stage of the ω family of division polynomials, which gives the Y coordinate of scalar multiplication in Jacobian coordinates.

Throughout, ψ is Mathlib's division-polynomial sequence WeierstrassCurve.ψ, and nothing here uses or asserts that it is an elliptic net or an elliptic sequence. IsEllipticNet.invarNum and IsEllipticNet.invarDenom are defined for an arbitrary sequence — invarDenom W s n is W (n + s) * W n * W (n - s) — so applying invarDenom to ψ is the use of a formula, not an ellipticity hypothesis; the namespace is where those formulas live, not a claim about ψ.

The name invar records where the polynomial comes from, and that origin is motivation rather than anything established below: for a sequence that is an elliptic net, and over a field where the relevant denominators are nonzero, invarNum/invarDenom is independent of the index — that is the cancellation of IsEllipticNet.invarNum_mul_invarDenom — and its value modulo the Weierstrass polynomial is 6 X² + b₂ X + b₄. Neither the hypothesis nor that conclusion is proved here, and over a CommRing the quotient need not exist at all. What this file proves are the polynomial identities listed below.

Main definitions

• WeierstrassCurve.invar: the invariant polynomial 6 X² + b₂ X + b₄.

Main results

• WeierstrassCurve.preΨ₄_add_Ψ₂Sq_sq: preΨ₄ + Ψ₂Sq ^ 2 = invar * Ψ₃, the identity that pins invar down. Its certificate is the b-relation 4 b₈ = b₂ b₆ - b₄ ².
• WeierstrassCurve.preΨ₄_add_ψ₂_pow_four: the same identity in the bivariate ring, where it acquires a multiple of the Weierstrass polynomial.
• WeierstrassCurve.C_Ψ₃: Ψ₃ through the partial derivatives of the Weierstrass polynomial.
• WeierstrassCurve.Affine.CoordinateRing.mk_preΨ₄_add_ψ₂_pow_four: the bivariate identity in the coordinate ring, where the multiple of the Weierstrass polynomial vanishes; with WeierstrassCurve.map_invar and baseChange_invar, the naturality the surrounding division-polynomial API provides for its other objects.
• WeierstrassCurve.φ_mul_ψ: φ n * ψ n = X ψ(n)³ - invarDenom ψ 1 n, which is what connects the division polynomials to the invariant denominator formula evaluated at ψ.

What is deliberately not here

WeierstrassCurve.ω itself and its API — ω_spec, ω_def, two_mul_ω, ψc, ψc_def, ψ_mul_ψc, ω_zero, ω_one, ψc_neg, map_ψc, map_ω, ω_neg — are not in this file; they live in DivisionPolynomial/Omega.lean. ω is defined through reducedInvarDenom and complEDS₂Aux, so it belongs above the reduced-invariant layer rather than beside these identities. Every input ω_spec consumes exists by name — the source's chain redInvar_normEDS ← invar₂_normEDS ← invar_normEDS ← net_normEDS has landed in full as reducedInvarNum_eq_reducedInvarDenom_mul (EllipticDivisibilitySequence/ReducedInvariant.lean) ← IsEllipticNet.invarNum_normEDS_one_mul_eq_invarDenom_mul ← invarNum_mul_invarDenom ← isEllipticNet_normEDS. Nothing in this file depends on any of it.

Provenance

Ported from J. Xu and D. K. Angdinata's LutzNagell/DivisionPolynomialOmega.lean in AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0, main at 1c1c74664e40071c2c2165bc55ca2616a67ccd6b), declarations invar, C_Ψ₃_eq (here C_Ψ₃, matching Mathlib's C_Ψ₂Sq), preΨ₄_add_Ψ₂Sq_sq, preΨ₄_add_ψ₂_pow_four and φ_mul_ψ. That file's header reads Authors: Junyan Xu, David Kurniadi Angdinata; following this repository's convention for adapted material the upstream authorship is credited here rather than in the copyright header.

Two adaptations, neither of them a choice:

• the source proves φ_mul_ψ by rw [φ, invarDenom], unfolding both definitions. The invarDenom half does not port: EllipticDivisibilitySequence/Invariant/Basic.lean exports that body unexposed, so from this module rw [invarDenom] has nothing to rewrite with. It goes through the equation lemma IsEllipticNet.invarDenom_def instead. φ unfolds as before, being Mathlib's.
• the source's local C_simp macro is written out at its three use sites rather than carried across, a macro being more surface than the one simp only call it abbreviates.

The statement of φ_mul_ψ was checked against Mathlib's φ rather than assumed: Mathlib defines φ n = C X * ψ n ^ 2 - ψ (n + 1) * ψ (n - 1), so φ n * ψ n is C X * ψ n ^ 3 - ψ (n + 1) * ψ n * ψ (n - 1), and that subtrahend is exactly IsEllipticNet.invarDenom ψ 1 n.

noncomputable def WeierstrassCurve.invar {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Polynomial R

The polynomial 6 X² + b₂ X + b₄ of a Weierstrass curve. What ties it to the division polynomials is preΨ₄_add_Ψ₂Sq_sq below, preΨ₄ + Ψ₂Sq ^ 2 = invar * Ψ₃. The name records the classical invariant of an elliptic net, whose index-independence is not what is proved here; see the module docstring.

Equations

• W.invar = 6 * Polynomial.X ^ 2 + Polynomial.C W.b₂ * Polynomial.X + Polynomial.C W.b₄

theorem WeierstrassCurve.invar_def {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.invar = 6 * Polynomial.X ^ 2 + Polynomial.C W.b₂ * Polynomial.X + Polynomial.C W.b₄

The defining formula for invar. The definition body is not exposed, so this equation lemma is how a consumer computes with it. Not @[simp]: the point of naming the polynomial is that preΨ₄_add_Ψ₂Sq_sq can be stated over it, which unfolding everywhere would defeat.

theorem WeierstrassCurve.C_Ψ₃ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Polynomial.C W.Ψ₃ = (3 * Polynomial.C Polynomial.X + Polynomial.CC W.a₂) * Polynomial.C W.Ψ₂Sq - Affine.polynomialX W ^ 2 + Polynomial.CC W.a₁ * W.ψ₂ * Affine.polynomialX W - Polynomial.CC W.a₁ ^ 2 * Affine.polynomial W

Ψ₃ expressed through the partial derivatives of the Weierstrass polynomial.

theorem WeierstrassCurve.preΨ₄_add_Ψ₂Sq_sq {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.preΨ₄ + W.Ψ₂Sq ^ 2 = W.invar * W.Ψ₃

The identity that pins invar down: preΨ₄ + Ψ₂Sq ^ 2 = invar * Ψ₃. The certificate is the b-relation 4 * b₈ = b₂ * b₆ - b₄ ^ 2.

theorem WeierstrassCurve.preΨ₄_add_ψ₂_pow_four {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Polynomial.C W.preΨ₄ + W.ψ₂ ^ 4 = Polynomial.C (W.invar * W.Ψ₃) + 8 * Affine.polynomial W * (2 * Affine.polynomial W + Polynomial.C W.Ψ₂Sq)

The bivariate form of preΨ₄_add_Ψ₂Sq_sq. Passing to R[X][Y] costs a multiple of the Weierstrass polynomial: ψ₂ ^ 2 and C Ψ₂Sq differ by 4 * Affine.polynomial W, and the factor 8 here comes from expanding the square of that difference.

theorem WeierstrassCurve.Affine.CoordinateRing.mk_preΨ₄_add_ψ₂_pow_four {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : (mk W) (Polynomial.C W.preΨ₄ + W.ψ₂ ^ 4) = (mk W) (Polynomial.C (W.invar * W.Ψ₃))

The bivariate identity in the coordinate ring, where the multiple of the Weierstrass polynomial vanishes: consumers working modulo the curve equation read the identity in this form.

theorem WeierstrassCurve.φ_mul_ψ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : W.φ n * W.ψ n = Polynomial.C Polynomial.X * W.ψ n ^ 3 - IsEllipticNet.invarDenom W.ψ 1 n

The division polynomials meet the invariant denominator: φ n * ψ n is X ψ(n)³ less IsEllipticNet.invarDenom ψ 1 n, which is ψ(n+1) ψ(n) ψ(n-1). That denominator is a formula in an arbitrary sequence, so this is an identity between division polynomials and uses no ellipticity of ψ. It is the step through which the elliptic-net formulas reach the curve.

@[simp]

theorem WeierstrassCurve.map_invar {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {S : Type u_2} [CommRing S] (f : R →+* S) : (W.map f).invar = Polynomial.map f W.invar

invar commutes with mapping the coefficients along a ring homomorphism.

theorem WeierstrassCurve.baseChange_invar {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {S : Type u_2} [CommRing S] [Algebra R S] {A : Type u_3} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type u_4} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (g : A →ₐ[S] B) : (W.baseChange B).invar = Polynomial.map (↑g) (W.baseChange A).invar

invar commutes with base change along an algebra homomorphism between extensions.