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 $\psi_n \in R[X, Y]$ of $W$ is the normalised EDS with initial values

• $\psi_0 := 0$,
• $\psi_1 := 1$,
• $\psi_2 := 2Y + a_1X + a_3$,
• $\psi_3 := 3X^4 + b_2X^3 + 3b_4X ^ 2 + 3b_6X + b_8$, and
• $\psi_4 := \psi_2 \cdot (2X^6 + b_2X^5 + 5b_4X^4 + 10b_6X^3 + 10b_8X^2 + (b_2b_8 - b_4b_6)X + (b_4b_8 - b_6^2))$.

Furthermore, define the associated sequences $\phi_n, \omega_n \in R[X, Y]$ by

• $\phi_n := X\psi_n^2 - \psi_{n + 1} \cdot \psi_{n - 1}$, and
• $\omega_n := (\psi_{2n} / \psi_n - \psi_n \cdot (a_1\phi_n + a_3\psi_n^2)) / 2$.

Note that $\omega_n$ is always well-defined as a polynomial in $R[X, Y]$. As a start, it can be shown by induction that $\psi_n$ always divides $\psi_{2n}$ in $R[X, Y]$, so that $\psi_{2n} / \psi_n$ 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 $\psi_{2n} / \psi_n - \psi_n \cdot (a_1\phi_n + a_3\psi_n^2)$ in the characteristic zero universal ring $\mathcal{R}[X, Y] := \mathbb{Z}[A_1, A_2, A_3, A_4, A_6][X, Y]$ of $W$, where the $A_i$ are indeterminates. Then $\omega_n$ can be equivalently defined as the image of this division under the associated universal morphism $\mathcal{R}[X, Y] \to R[X, Y]$ mapping $A_i$ to $a_i$.

Now, in the coordinate ring $R[W]$, note that $\psi_2^2$ is congruent to the polynomial $\Psi_2^{[2]} := 4X^3 + b_2X^2 + 2b_4X + b_6 \in R[X]$. As such, in $R[W]$, the recurrences associated to a normalised EDS show that $\psi_n / \psi_2$ are congruent to certain polynomials in $R[X]$. In particular, define $\tilde{\Psi}_n \in R[X]$ as the auxiliary sequence for a normalised EDS with extra parameter $(\Psi_2^{[2]})^2$ and initial values

• $\tilde{\Psi}_0 := 0$,
• $\tilde{\Psi}_1 := 1$,
• $\tilde{\Psi}_2 := 1$,
• $\tilde{\Psi}_3 := \psi_3$, and
• $\tilde{\Psi}_4 := \psi_4 / \psi_2$.

The corresponding normalised EDS $\Psi_n \in R[X, Y]$ is then given by

• $\Psi_n := \tilde{\Psi}_n \cdot \psi_2$ if $n$ is even, and
• $\Psi_n := \tilde{\Psi}_n$ if $n$ is odd.

Furthermore, define the associated sequences $\Psi_n^{[2]}, \Phi_n \in R[X]$ by

• $\Psi_n^{[2]} := \tilde{\Psi}_n^2 \cdot \Psi_2^{[2]}$ if $n$ is even,
• $\Psi_n^{[2]} := \tilde{\Psi}_n^2$ if $n$ is odd,
• $\Phi_n := X\Psi_n^{[2]} - \tilde{\Psi}_{n + 1} \cdot \tilde{\Psi}_{n - 1}$ if $n$ is even, and
• $\Phi_n := X\Psi_n^{[2]} - \tilde{\Psi}_{n + 1} \cdot \tilde{\Psi}_{n - 1} \cdot \Psi_2^{[2]}$ if $n$ is odd.

With these definitions in mind, $\psi_n \in R[X, Y]$ and $\phi_n \in R[X, Y]$ are congruent in $R[W]$ to $\Psi_n \in R[X, Y]$ and $\Phi_n \in R[X]$ respectively, which are defined in terms of $\Psi_2^{[2]} \in R[X]$ and $\tilde{\Psi}_n \in R[X]$.

Main definitions

• WeierstrassCurve.preΨ: the univariate polynomials $\tilde{\Psi}_n$.
• WeierstrassCurve.ΨSq: the univariate polynomials $\Psi_n^{[2]}$.
• WeierstrassCurve.Ψ: the bivariate polynomials $\Psi_n$.
• WeierstrassCurve.Φ: the univariate polynomials $\Phi_n$.
• WeierstrassCurve.ψ: the bivariate $n$-division polynomials $\psi_n$.
• WeierstrassCurve.φ: the bivariate polynomials $\phi_n$.
• TODO: the bivariate polynomials $\omega_n$.

Implementation notes

Analogously to Mathlib.NumberTheory.EllipticDivisibilitySequence, the bivariate polynomials $\Psi_n$ are defined in terms of the univariate polynomials $\tilde{\Psi}_n$. This is done partially to avoid ring division, but more crucially to allow the definition of $\Psi_n^{[2]}$ and $\Phi_n$ 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 $\omega_n$.

References

J Silverman, The Arithmetic of Elliptic Curves

Tags

elliptic curve, division polynomial, torsion point

The univariate polynomial $\Psi_2^{[2]}$

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

The $2$-division polynomial $\psi_2 = \Psi_2$.

Equations

• W.ψ₂ = W.toAffine.polynomialY

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

The univariate polynomial $\Psi_2^{[2]}$ congruent to $\psi_2^2$.

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 $\tilde{\Psi}_n$ for $n \in \mathbb{N}$

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

The $3$-division polynomial $\psi_3 = \Psi_3$.

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 $\tilde{\Psi}_4$, which is auxiliary to the $4$-division polynomial $\psi_4 = \Psi_4 = \tilde{\Psi}_4\psi_2$.

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 $\tilde{\Psi}_n$ for $n \in \mathbb{N}$, which are auxiliary to the bivariate polynomials $\Psi_n$ congruent to the bivariate $n$-division polynomials $\psi_n$.

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Ψ'_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

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

The univariate polynomials $\tilde{\Psi}_n$ for $n \in \mathbb{Z}$

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

The univariate polynomials $\tilde{\Psi}_n$ for $n \in \mathbb{Z}$, which are auxiliary to the bivariate polynomials $\Psi_n$ congruent to the bivariate $n$-division polynomials $\psi_n$.

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Ψ_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

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

@[simp]

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

The univariate polynomials $\Psi_n^{[2]}$

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

The univariate polynomials $\Psi_n^{[2]}$ congruent to $\psi_n^2$.

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_odd {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

theorem WeierstrassCurve.ΨSq_even {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

@[simp]

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

The bivariate polynomials $\Psi_n$

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

The bivariate polynomials $\Psi_n$ congruent to the $n$-division polynomials $\psi_n$.

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.Ψ_odd {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)

theorem WeierstrassCurve.Ψ_even {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

@[simp]

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

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 $\Phi_n$

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

The univariate polynomials $\Phi_n$ congruent to $\phi_n$.

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 $\psi_n$

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

The bivariate $n$-division polynomials $\psi_n$.

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.ψ_odd {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

theorem WeierstrassCurve.ψ_even {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

@[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) (W.Ψ n)

The bivariate polynomials $\phi_n$

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

The bivariate polynomials $\phi_n$.

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)