Division polynomials of Weierstrass curves

This file defines certain polynomials associated to division polynomials of Weierstrass curves. These are defined in terms of the auxiliary sequences for normalised elliptic divisibility sequences (EDS) as defined in Mathlib.NumberTheory.EllipticDivisibilitySequence.

Mathematical background

Let W be a Weierstrass curve over a commutative ring R. The sequence of n-division polynomials ψₙ ∈ R[X, Y] of W is the normalised EDS with initial values

• ψ₀ := 0,
• ψ₁ := 1,
• ψ₂ := 2Y + a₁X + a₃,
• ψ₃ := 3X⁴ + b₂X³ + 3b₄X² + 3b₆X + b₈, and
• ψ₄ := ψ₂ ⬝ (2X⁶ + b₂X⁵ + 5b₄X⁴ + 10b₆X³ + 10b₈X² + (b₂b₈ - b₄b₆)X + (b₄b₈ - b₆²)).

Furthermore, define the associated sequences φₙ, ωₙ ∈ R[X, Y] by

• φₙ := Xψₙ² - ψₙ₊₁ ⬝ ψₙ₋₁, and
• ωₙ := (ψ₂ₙ / ψₙ - ψₙ ⬝ (a₁φₙ + a₃ψₙ²)) / 2.

Note that ωₙ is always well-defined as a polynomial in R[X, Y]. As a start, it can be shown by induction that ψₙ always divides ψ₂ₙ in R[X, Y], so that ψ₂ₙ / ψₙ is always well-defined as a polynomial, while division by 2 is well-defined when R has characteristic different from 2. In general, it can be shown that 2 always divides the polynomial ψ₂ₙ / ψₙ - ψₙ ⬝ (a₁φₙ + a₃ψₙ²) in the characteristic 0 universal ring 𝓡[X, Y] := ℤ[A₁, A₂, A₃, A₄, A₆][X, Y] of W, where the Aᵢ are indeterminates. Then ωₙ can be equivalently defined as the image of this division under the associated universal morphism 𝓡[X, Y] → R[X, Y] mapping Aᵢ to aᵢ.

Now, in the coordinate ring R[W], note that ψ₂² is congruent to the polynomial Ψ₂Sq := 4X³ + b₂X² + 2b₄X + b₆ ∈ R[X]. As such, the recurrences of a normalised EDS show that ψₙ / ψ₂ are congruent to certain polynomials in R[W]. In particular, define preΨₙ ∈ R[X] as the auxiliary sequence for a normalised EDS with extra parameter Ψ₂Sq² and initial values

• preΨ₀ := 0,
• preΨ₁ := 1,
• preΨ₂ := 1,
• preΨ₃ := ψ₃, and
• preΨ₄ := ψ₄ / ψ₂.

The corresponding normalised EDS Ψₙ ∈ R[X, Y] is then given by

• Ψₙ := preΨₙ ⬝ ψ₂ if n is even, and
• Ψₙ := preΨₙ if n is odd.

Furthermore, define the associated sequences ΨSqₙ, Φₙ ∈ R[X] by

• ΨSqₙ := preΨₙ² ⬝ Ψ₂Sq if n is even,
• ΨSqₙ := preΨₙ² if n is odd,
• Φₙ := XΨSqₙ - preΨₙ₊₁ ⬝ preΨₙ₋₁ if n is even, and
• Φₙ := XΨSqₙ - preΨₙ₊₁ ⬝ preΨₙ₋₁ ⬝ Ψ₂Sq if n is odd.

With these definitions, ψₙ ∈ R[X, Y] and φₙ ∈ R[X, Y] are congruent in R[W] to Ψₙ ∈ R[X, Y] and Φₙ ∈ R[X] respectively, which are defined in terms of Ψ₂Sq ∈ R[X] and preΨₙ ∈ R[X].

Main definitions

• WeierstrassCurve.preΨ: the univariate polynomials preΨₙ.
• WeierstrassCurve.ΨSq: the univariate polynomials ΨSqₙ.
• WeierstrassCurve.Ψ: the bivariate polynomials Ψₙ.
• WeierstrassCurve.Φ: the univariate polynomials Φₙ.
• WeierstrassCurve.ψ: the bivariate n-division polynomials ψₙ.
• WeierstrassCurve.φ: the bivariate polynomials φₙ.
• TODO: the bivariate polynomials ωₙ.

Implementation notes

Analogously to Mathlib.NumberTheory.EllipticDivisibilitySequence, the bivariate polynomials Ψₙ are defined in terms of the univariate polynomials preΨₙ. This is done partially to avoid ring division, but more crucially to allow the definition of ΨSqₙ and Φₙ as univariate polynomials without needing to work under the coordinate ring, and to allow the computation of their leading terms without ambiguity. Furthermore, evaluating these polynomials at a rational point on W recovers their original definition up to linear combinations of the Weierstrass equation of W, hence also avoiding the need to work in the coordinate ring.

TODO: implementation notes for the definition of ωₙ.

References

J Silverman, The Arithmetic of Elliptic Curves

Tags

elliptic curve, division polynomial, torsion point

The univariate polynomial Ψ₂Sq

noncomputable def WeierstrassCurve.ψ₂ {R : Type r} [CommRing R] (W : WeierstrassCurve R) : Polynomial (Polynomial R)

The 2-division polynomial ψ₂ = Ψ₂.

Equations

• W.ψ₂ = W.toAffine.polynomialY

noncomputable def WeierstrassCurve.Ψ₂Sq {R : Type r} [CommRing R] (W : WeierstrassCurve R) : Polynomial R

The univariate polynomial Ψ₂Sq congruent to ψ₂².

Equations

• W.Ψ₂Sq = Polynomial.C 4 * Polynomial.X ^ 3 + Polynomial.C W.b₂ * Polynomial.X ^ 2 + Polynomial.C (2 * W.b₄) * Polynomial.X + Polynomial.C W.b₆

theorem WeierstrassCurve.C_Ψ₂Sq {R : Type r} [CommRing R] (W : WeierstrassCurve R) : Polynomial.C W.Ψ₂Sq = W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial

theorem WeierstrassCurve.ψ₂_sq {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.ψ₂ ^ 2 = Polynomial.C W.Ψ₂Sq + 4 * W.toAffine.polynomial

theorem WeierstrassCurve.Affine.CoordinateRing.mk_ψ₂_sq {R : Type r} [CommRing R] (W : WeierstrassCurve R) : (WeierstrassCurve.Affine.CoordinateRing.mk W) W.ψ₂ ^ 2 = (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C W.Ψ₂Sq)

theorem WeierstrassCurve.Ψ₂Sq_eq {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.Ψ₂Sq = W.twoTorsionPolynomial.toPoly

The univariate polynomials preΨₙ for n ∈ ℕ

noncomputable def WeierstrassCurve.Ψ₃ {R : Type r} [CommRing R] (W : WeierstrassCurve R) : Polynomial R

The 3-division polynomial ψ₃ = Ψ₃.

Equations

• W.Ψ₃ = 3 * Polynomial.X ^ 4 + Polynomial.C W.b₂ * Polynomial.X ^ 3 + 3 * Polynomial.C W.b₄ * Polynomial.X ^ 2 + 3 * Polynomial.C W.b₆ * Polynomial.X + Polynomial.C W.b₈

noncomputable def WeierstrassCurve.preΨ₄ {R : Type r} [CommRing R] (W : WeierstrassCurve R) : Polynomial R

The univariate polynomial preΨ₄, which is auxiliary to the 4-division polynomial ψ₄ = Ψ₄ = preΨ₄ψ₂.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def WeierstrassCurve.preΨ' {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℕ) : Polynomial R

The univariate polynomials preΨₙ for n ∈ ℕ, which are auxiliary to the bivariate polynomials Ψₙ congruent to the bivariate n-division polynomials ψₙ.

Equations

• W.preΨ' n = preNormEDS' (W.Ψ₂Sq ^ 2) W.Ψ₃ W.preΨ₄ n

@[simp]

theorem WeierstrassCurve.preΨ'_zero {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.preΨ' 0 = 0

@[simp]

theorem WeierstrassCurve.preΨ'_one {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.preΨ' 1 = 1

@[simp]

theorem WeierstrassCurve.preΨ'_two {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.preΨ' 2 = 1

@[simp]

theorem WeierstrassCurve.preΨ'_three {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.preΨ' 3 = W.Ψ₃

@[simp]

theorem WeierstrassCurve.preΨ'_four {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.preΨ' 4 = W.preΨ₄

theorem WeierstrassCurve.preΨ'_even {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℕ) : W.preΨ' (2 * (m + 3)) = W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) - W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2

theorem WeierstrassCurve.preΨ'_odd {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℕ) : W.preΨ' (2 * (m + 2) + 1) = (W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) - W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2

The univariate polynomials preΨₙ for n ∈ ℤ

noncomputable def WeierstrassCurve.preΨ {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : Polynomial R

The univariate polynomials preΨₙ for n ∈ ℤ, which are auxiliary to the bivariate polynomials Ψₙ congruent to the bivariate n-division polynomials ψₙ.

Equations

• W.preΨ n = preNormEDS (W.Ψ₂Sq ^ 2) W.Ψ₃ W.preΨ₄ n

@[simp]

theorem WeierstrassCurve.preΨ_ofNat {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℕ) : W.preΨ ↑n = W.preΨ' n

@[simp]

theorem WeierstrassCurve.preΨ_zero {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.preΨ 0 = 0

@[simp]

theorem WeierstrassCurve.preΨ_one {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.preΨ 1 = 1

@[simp]

theorem WeierstrassCurve.preΨ_two {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.preΨ 2 = 1

@[simp]

theorem WeierstrassCurve.preΨ_three {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.preΨ 3 = W.Ψ₃

@[simp]

theorem WeierstrassCurve.preΨ_four {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.preΨ 4 = W.preΨ₄

theorem WeierstrassCurve.preΨ_even_ofNat {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℕ) : W.preΨ (2 * (↑m + 3)) = W.preΨ (↑m + 2) ^ 2 * W.preΨ (↑m + 3) * W.preΨ (↑m + 5) - W.preΨ (↑m + 1) * W.preΨ (↑m + 3) * W.preΨ (↑m + 4) ^ 2

theorem WeierstrassCurve.preΨ_odd_ofNat {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℕ) : W.preΨ (2 * (↑m + 2) + 1) = (W.preΨ (↑m + 4) * W.preΨ (↑m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) - W.preΨ (↑m + 1) * W.preΨ (↑m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2

@[simp]

theorem WeierstrassCurve.preΨ_neg {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : W.preΨ (-n) = -W.preΨ n

theorem WeierstrassCurve.preΨ_even {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℤ) : W.preΨ (2 * m) = W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2

theorem WeierstrassCurve.preΨ_odd {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℤ) : W.preΨ (2 * m + 1) = (W.preΨ (m + 2) * W.preΨ m ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) - W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2

The univariate polynomials ΨSqₙ

noncomputable def WeierstrassCurve.ΨSq {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : Polynomial R

The univariate polynomials ΨSqₙ congruent to ψₙ².

Equations

• W.ΨSq n = W.preΨ n ^ 2 * if Even n then W.Ψ₂Sq else 1

@[simp]

theorem WeierstrassCurve.ΨSq_ofNat {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℕ) : W.ΨSq ↑n = W.preΨ' n ^ 2 * if Even n then W.Ψ₂Sq else 1

@[simp]

theorem WeierstrassCurve.ΨSq_zero {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.ΨSq 0 = 0

@[simp]

theorem WeierstrassCurve.ΨSq_one {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.ΨSq 1 = 1

@[simp]

theorem WeierstrassCurve.ΨSq_two {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.ΨSq 2 = W.Ψ₂Sq

@[simp]

theorem WeierstrassCurve.ΨSq_three {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.ΨSq 3 = W.Ψ₃ ^ 2

@[simp]

theorem WeierstrassCurve.ΨSq_four {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.ΨSq 4 = W.preΨ₄ ^ 2 * W.Ψ₂Sq

theorem WeierstrassCurve.ΨSq_even_ofNat {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℕ) : W.ΨSq (2 * (↑m + 3)) = (W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) - W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2) ^ 2 * W.Ψ₂Sq

theorem WeierstrassCurve.ΨSq_odd_ofNat {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℕ) : W.ΨSq (2 * (↑m + 2) + 1) = ((W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) - W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2) ^ 2

@[simp]

theorem WeierstrassCurve.ΨSq_neg {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : W.ΨSq (-n) = W.ΨSq n

theorem WeierstrassCurve.ΨSq_even {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℤ) : W.ΨSq (2 * m) = (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) ^ 2 * W.Ψ₂Sq

theorem WeierstrassCurve.ΨSq_odd {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℤ) : W.ΨSq (2 * m + 1) = ((W.preΨ (m + 2) * W.preΨ m ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) - W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2) ^ 2

The bivariate polynomials Ψₙ

noncomputable def WeierstrassCurve.Ψ {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : Polynomial (Polynomial R)

The bivariate polynomials Ψₙ congruent to the n-division polynomials ψₙ.

Equations

• W.Ψ n = Polynomial.C (W.preΨ n) * if Even n then W.ψ₂ else 1

@[simp]

theorem WeierstrassCurve.Ψ_ofNat {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℕ) : W.Ψ ↑n = Polynomial.C (W.preΨ' n) * if Even n then W.ψ₂ else 1

@[simp]

theorem WeierstrassCurve.Ψ_zero {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.Ψ 0 = 0

@[simp]

theorem WeierstrassCurve.Ψ_one {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.Ψ 1 = 1

@[simp]

theorem WeierstrassCurve.Ψ_two {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.Ψ 2 = W.ψ₂

@[simp]

theorem WeierstrassCurve.Ψ_three {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.Ψ 3 = Polynomial.C W.Ψ₃

@[simp]

theorem WeierstrassCurve.Ψ_four {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.Ψ 4 = Polynomial.C W.preΨ₄ * W.ψ₂

theorem WeierstrassCurve.Ψ_even_ofNat {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℕ) : W.Ψ (2 * (↑m + 3)) * W.ψ₂ = W.Ψ (↑m + 2) ^ 2 * W.Ψ (↑m + 3) * W.Ψ (↑m + 5) - W.Ψ (↑m + 1) * W.Ψ (↑m + 3) * W.Ψ (↑m + 4) ^ 2

theorem WeierstrassCurve.Ψ_odd_ofNat {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℕ) : W.Ψ (2 * (↑m + 2) + 1) = W.Ψ (↑m + 4) * W.Ψ (↑m + 2) ^ 3 - W.Ψ (↑m + 1) * W.Ψ (↑m + 3) ^ 3 + W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * Polynomial.C (if Even m then W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 else -W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3)

@[simp]

theorem WeierstrassCurve.Ψ_neg {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : W.Ψ (-n) = -W.Ψ n

theorem WeierstrassCurve.Ψ_even {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℤ) : W.Ψ (2 * m) * W.ψ₂ = W.Ψ (m - 1) ^ 2 * W.Ψ m * W.Ψ (m + 2) - W.Ψ (m - 2) * W.Ψ m * W.Ψ (m + 1) ^ 2

theorem WeierstrassCurve.Ψ_odd {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℤ) : W.Ψ (2 * m + 1) = W.Ψ (m + 2) * W.Ψ m ^ 3 - W.Ψ (m - 1) * W.Ψ (m + 1) ^ 3 + W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * Polynomial.C (if Even m then W.preΨ (m + 2) * W.preΨ m ^ 3 else -W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3)

theorem WeierstrassCurve.Affine.CoordinateRing.mk_Ψ_sq {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : (WeierstrassCurve.Affine.CoordinateRing.mk W) (W.Ψ n) ^ 2 = (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C (W.ΨSq n))

The univariate polynomials Φₙ

noncomputable def WeierstrassCurve.Φ {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : Polynomial R

The univariate polynomials Φₙ congruent to φₙ.

Equations

• W.Φ n = Polynomial.X * W.ΨSq n - W.preΨ (n + 1) * W.preΨ (n - 1) * if Even n then 1 else W.Ψ₂Sq

@[simp]

theorem WeierstrassCurve.Φ_ofNat {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℕ) : W.Φ (↑n + 1) = (Polynomial.X * W.preΨ' (n + 1) ^ 2 * if Even n then 1 else W.Ψ₂Sq) - W.preΨ' (n + 2) * W.preΨ' n * if Even n then W.Ψ₂Sq else 1

@[simp]

theorem WeierstrassCurve.Φ_zero {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.Φ 0 = 1

@[simp]

theorem WeierstrassCurve.Φ_one {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.Φ 1 = Polynomial.X

@[simp]

theorem WeierstrassCurve.Φ_two {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.Φ 2 = Polynomial.X ^ 4 - Polynomial.C W.b₄ * Polynomial.X ^ 2 - Polynomial.C (2 * W.b₆) * Polynomial.X - Polynomial.C W.b₈

@[simp]

theorem WeierstrassCurve.Φ_three {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.Φ 3 = Polynomial.X * W.Ψ₃ ^ 2 - W.preΨ₄ * W.Ψ₂Sq

@[simp]

theorem WeierstrassCurve.Φ_four {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.Φ 4 = Polynomial.X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)

@[simp]

theorem WeierstrassCurve.Φ_neg {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : W.Φ (-n) = W.Φ n

The bivariate polynomials ψₙ

noncomputable def WeierstrassCurve.ψ {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : Polynomial (Polynomial R)

The bivariate n-division polynomials ψₙ.

Equations

• W.ψ n = normEDS W.ψ₂ (Polynomial.C W.Ψ₃) (Polynomial.C W.preΨ₄) n

@[simp]

theorem WeierstrassCurve.ψ_zero {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.ψ 0 = 0

@[simp]

theorem WeierstrassCurve.ψ_one {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.ψ 1 = 1

@[simp]

theorem WeierstrassCurve.ψ_two {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.ψ 2 = W.ψ₂

@[simp]

theorem WeierstrassCurve.ψ_three {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.ψ 3 = Polynomial.C W.Ψ₃

@[simp]

theorem WeierstrassCurve.ψ_four {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.ψ 4 = Polynomial.C W.preΨ₄ * W.ψ₂

theorem WeierstrassCurve.ψ_even_ofNat {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℕ) : W.ψ (2 * (↑m + 3)) * W.ψ₂ = W.ψ (↑m + 2) ^ 2 * W.ψ (↑m + 3) * W.ψ (↑m + 5) - W.ψ (↑m + 1) * W.ψ (↑m + 3) * W.ψ (↑m + 4) ^ 2

theorem WeierstrassCurve.ψ_odd_ofNat {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℕ) : W.ψ (2 * (↑m + 2) + 1) = W.ψ (↑m + 4) * W.ψ (↑m + 2) ^ 3 - W.ψ (↑m + 1) * W.ψ (↑m + 3) ^ 3

@[simp]

theorem WeierstrassCurve.ψ_neg {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : W.ψ (-n) = -W.ψ n

theorem WeierstrassCurve.ψ_even {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℤ) : W.ψ (2 * m) * W.ψ₂ = W.ψ (m - 1) ^ 2 * W.ψ m * W.ψ (m + 2) - W.ψ (m - 2) * W.ψ m * W.ψ (m + 1) ^ 2

theorem WeierstrassCurve.ψ_odd {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ℤ) : W.ψ (2 * m + 1) = W.ψ (m + 2) * W.ψ m ^ 3 - W.ψ (m - 1) * W.ψ (m + 1) ^ 3

theorem WeierstrassCurve.Affine.CoordinateRing.mk_ψ {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : (WeierstrassCurve.Affine.CoordinateRing.mk W) (W.ψ n) = (WeierstrassCurve.Affine.CoordinateRing.mk W) (W.Ψ n)

The bivariate polynomials φₙ

noncomputable def WeierstrassCurve.φ {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : Polynomial (Polynomial R)

The bivariate polynomials φₙ.

Equations

• W.φ n = Polynomial.C Polynomial.X * W.ψ n ^ 2 - W.ψ (n + 1) * W.ψ (n - 1)

@[simp]

theorem WeierstrassCurve.φ_zero {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.φ 0 = 1

@[simp]

theorem WeierstrassCurve.φ_one {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.φ 1 = Polynomial.C Polynomial.X

@[simp]

theorem WeierstrassCurve.φ_two {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.φ 2 = Polynomial.C Polynomial.X * W.ψ₂ ^ 2 - Polynomial.C W.Ψ₃

@[simp]

theorem WeierstrassCurve.φ_three {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.φ 3 = Polynomial.C Polynomial.X * Polynomial.C W.Ψ₃ ^ 2 - Polynomial.C W.preΨ₄ * W.ψ₂ ^ 2

@[simp]

theorem WeierstrassCurve.φ_four {R : Type r} [CommRing R] (W : WeierstrassCurve R) : W.φ 4 = Polynomial.C Polynomial.X * Polynomial.C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - Polynomial.C W.preΨ₄ * W.ψ₂ ^ 4 * Polynomial.C W.Ψ₃ + Polynomial.C W.Ψ₃ ^ 4

@[simp]

theorem WeierstrassCurve.φ_neg {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : W.φ (-n) = W.φ n

theorem WeierstrassCurve.Affine.CoordinateRing.mk_φ {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : (WeierstrassCurve.Affine.CoordinateRing.mk W) (W.φ n) = (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C (W.Φ n))

Maps across ring homomorphisms

theorem WeierstrassCurve.map_ψ₂ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) : (W.map f).ψ₂ = Polynomial.map (Polynomial.mapRingHom f) W.ψ₂

theorem WeierstrassCurve.map_Ψ₂Sq {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) : (W.map f).Ψ₂Sq = Polynomial.map f W.Ψ₂Sq

theorem WeierstrassCurve.map_Ψ₃ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) : (W.map f).Ψ₃ = Polynomial.map f W.Ψ₃

theorem WeierstrassCurve.map_preΨ₄ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) : (W.map f).preΨ₄ = Polynomial.map f W.preΨ₄

theorem WeierstrassCurve.map_preΨ' {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℕ) : (W.map f).preΨ' n = Polynomial.map f (W.preΨ' n)

theorem WeierstrassCurve.map_preΨ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ) : (W.map f).preΨ n = Polynomial.map f (W.preΨ n)

theorem WeierstrassCurve.map_ΨSq {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ) : (W.map f).ΨSq n = Polynomial.map f (W.ΨSq n)

theorem WeierstrassCurve.map_Ψ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ) : (W.map f).Ψ n = Polynomial.map (Polynomial.mapRingHom f) (W.Ψ n)

theorem WeierstrassCurve.map_Φ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ) : (W.map f).Φ n = Polynomial.map f (W.Φ n)

theorem WeierstrassCurve.map_ψ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ) : (W.map f).ψ n = Polynomial.map (Polynomial.mapRingHom f) (W.ψ n)

theorem WeierstrassCurve.map_φ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ) : (W.map f).φ n = Polynomial.map (Polynomial.mapRingHom f) (W.φ n)

Base changes across algebra homomorphisms

theorem WeierstrassCurve.baseChange_ψ₂ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) : (W.baseChange B).ψ₂ = Polynomial.map (Polynomial.mapRingHom ↑f) (W.baseChange A).ψ₂

theorem WeierstrassCurve.baseChange_Ψ₂Sq {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) : (W.baseChange B).Ψ₂Sq = Polynomial.map (↑f) (W.baseChange A).Ψ₂Sq

theorem WeierstrassCurve.baseChange_Ψ₃ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) : (W.baseChange B).Ψ₃ = Polynomial.map (↑f) (W.baseChange A).Ψ₃

theorem WeierstrassCurve.baseChange_preΨ₄ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) : (W.baseChange B).preΨ₄ = Polynomial.map (↑f) (W.baseChange A).preΨ₄

theorem WeierstrassCurve.baseChange_preΨ' {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ℕ) : (W.baseChange B).preΨ' n = Polynomial.map (↑f) ((W.baseChange A).preΨ' n)

theorem WeierstrassCurve.baseChange_preΨ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ℤ) : (W.baseChange B).preΨ n = Polynomial.map (↑f) ((W.baseChange A).preΨ n)

theorem WeierstrassCurve.baseChange_ΨSq {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ℤ) : (W.baseChange B).ΨSq n = Polynomial.map (↑f) ((W.baseChange A).ΨSq n)

theorem WeierstrassCurve.baseChange_Ψ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ℤ) : (W.baseChange B).Ψ n = Polynomial.map (Polynomial.mapRingHom ↑f) ((W.baseChange A).Ψ n)

theorem WeierstrassCurve.baseChange_Φ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ℤ) : (W.baseChange B).Φ n = Polynomial.map (↑f) ((W.baseChange A).Φ n)

theorem WeierstrassCurve.baseChange_ψ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ℤ) : (W.baseChange B).ψ n = Polynomial.map (Polynomial.mapRingHom ↑f) ((W.baseChange A).ψ n)

theorem WeierstrassCurve.baseChange_φ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ℤ) : (W.baseChange B).φ n = Polynomial.map (Polynomial.mapRingHom ↑f) ((W.baseChange A).φ n)