Division polynomials of Weierstrass curves

This file computes the leading terms of certain polynomials associated to division polynomials of Weierstrass curves defined in Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic.

Mathematical background

Let $W$ be a Weierstrass curve over a commutative ring $R$. By strong induction,

• $\tilde{\Psi}_n = \tfrac{n}{2}X^{\tfrac{n^2 - 4}{2}} + \dots$ if $n$ is even,
• $\tilde{\Psi}_n = nX^{\tfrac{n^2 - 1}{2}} + \dots$ if $n$ is odd,
• $\Psi_n^{[2]} = n^2X^{n^2 - 1} + \dots$, and
• $\Phi_n = X^{n^2} + \dots$.

In particular, when $R$ is an integral domain of characteristic different from $n$, the univariate polynomials $\tilde{\Psi}_n$, $\Psi_n^{[2]}$, and $\Phi_n$ all have their expected leading terms.

Main statements

• WeierstrassCurve.natDegree_preΨ_le: the expected degree of $\tilde{\Psi}_n$.
• WeierstrassCurve.coeff_preΨ: the expected leading coefficient of $\tilde{\Psi}_n$.
• WeierstrassCurve.natDegree_preΨ: the degree of $\tilde{\Psi}_n$ when $n \ne 0$.
• WeierstrassCurve.leadingCoeff_preΨ: the leading coefficient of $\tilde{\Psi}_n$ when $n \ne 0$.
• WeierstrassCurve.natDegree_ΨSq_le: the expected degree of $\Psi_n^{[2]}$.
• WeierstrassCurve.coeff_ΨSq: the expected leading coefficient of $\Psi_n^{[2]}$.
• WeierstrassCurve.natDegree_ΨSq: the degree of $\Psi_n^{[2]}$ when $n \ne 0$.
• WeierstrassCurve.leadingCoeff_ΨSq: the leading coefficient of $\Psi_n^{[2]}$ when $n \ne 0$.
• WeierstrassCurve.natDegree_Φ_le: the expected degree of $\Phi_n$.
• WeierstrassCurve.coeff_Φ: the expected leading coefficient of $\Phi_n$.
• WeierstrassCurve.natDegree_Φ: the degree of $\Phi_n$ when $n \ne 0$.
• WeierstrassCurve.leadingCoeff_Φ: the leading coefficient of $\Phi_n$ when $n \ne 0$.

References

[J Silverman, The Arithmetic of Elliptic Curves][silverman2009]

Tags

elliptic curve, division polynomial, torsion point

theorem WeierstrassCurve.natDegree_Ψ₂Sq_le {R : Type u} [CommRing R] (W : WeierstrassCurve R) : W.Ψ₂Sq.natDegree ≤ 3

@[simp]

theorem WeierstrassCurve.coeff_Ψ₂Sq {R : Type u} [CommRing R] (W : WeierstrassCurve R) : W.Ψ₂Sq.coeff 3 = 4

theorem WeierstrassCurve.coeff_Ψ₂Sq_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) (h : 4 ≠ 0) : W.Ψ₂Sq.coeff 3 ≠ 0

@[simp]

theorem WeierstrassCurve.natDegree_Ψ₂Sq {R : Type u} [CommRing R] (W : WeierstrassCurve R) (h : 4 ≠ 0) : W.Ψ₂Sq.natDegree = 3

theorem WeierstrassCurve.natDegree_Ψ₂Sq_pos {R : Type u} [CommRing R] (W : WeierstrassCurve R) (h : 4 ≠ 0) : 0 < W.Ψ₂Sq.natDegree

@[simp]

theorem WeierstrassCurve.leadingCoeff_Ψ₂Sq {R : Type u} [CommRing R] (W : WeierstrassCurve R) (h : 4 ≠ 0) : W.Ψ₂Sq.leadingCoeff = 4

theorem WeierstrassCurve.Ψ₂Sq_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) (h : 4 ≠ 0) : W.Ψ₂Sq ≠ 0

theorem WeierstrassCurve.natDegree_Ψ₃_le {R : Type u} [CommRing R] (W : WeierstrassCurve R) : W.Ψ₃.natDegree ≤ 4

@[simp]

theorem WeierstrassCurve.coeff_Ψ₃ {R : Type u} [CommRing R] (W : WeierstrassCurve R) : W.Ψ₃.coeff 4 = 3

theorem WeierstrassCurve.coeff_Ψ₃_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) (h : 3 ≠ 0) : W.Ψ₃.coeff 4 ≠ 0

@[simp]

theorem WeierstrassCurve.natDegree_Ψ₃ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (h : 3 ≠ 0) : W.Ψ₃.natDegree = 4

theorem WeierstrassCurve.natDegree_Ψ₃_pos {R : Type u} [CommRing R] (W : WeierstrassCurve R) (h : 3 ≠ 0) : 0 < W.Ψ₃.natDegree

@[simp]

theorem WeierstrassCurve.leadingCoeff_Ψ₃ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (h : 3 ≠ 0) : W.Ψ₃.leadingCoeff = 3

theorem WeierstrassCurve.Ψ₃_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) (h : 3 ≠ 0) : W.Ψ₃ ≠ 0

theorem WeierstrassCurve.natDegree_preΨ₄_le {R : Type u} [CommRing R] (W : WeierstrassCurve R) : W.preΨ₄.natDegree ≤ 6

@[simp]

theorem WeierstrassCurve.coeff_preΨ₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) : W.preΨ₄.coeff 6 = 2

theorem WeierstrassCurve.coeff_preΨ₄_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) (h : 2 ≠ 0) : W.preΨ₄.coeff 6 ≠ 0

@[simp]

theorem WeierstrassCurve.natDegree_preΨ₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (h : 2 ≠ 0) : W.preΨ₄.natDegree = 6

theorem WeierstrassCurve.natDegree_preΨ₄_pos {R : Type u} [CommRing R] (W : WeierstrassCurve R) (h : 2 ≠ 0) : 0 < W.preΨ₄.natDegree

@[simp]

theorem WeierstrassCurve.leadingCoeff_preΨ₄ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (h : 2 ≠ 0) : W.preΨ₄.leadingCoeff = 2

theorem WeierstrassCurve.preΨ₄_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) (h : 2 ≠ 0) : W.preΨ₄ ≠ 0

theorem WeierstrassCurve.natDegree_preΨ'_le {R : Type u} [CommRing R] (W : WeierstrassCurve R) (n : ℕ) : (W.preΨ' n).natDegree ≤ (n ^ 2 - if Even n then 4 else 1) / 2

@[simp]

theorem WeierstrassCurve.coeff_preΨ' {R : Type u} [CommRing R] (W : WeierstrassCurve R) (n : ℕ) : (W.preΨ' n).coeff ((n ^ 2 - if Even n then 4 else 1) / 2) = ↑(if Even n then n / 2 else n)

theorem WeierstrassCurve.coeff_preΨ'_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) {n : ℕ} (h : ↑n ≠ 0) : (W.preΨ' n).coeff ((n ^ 2 - if Even n then 4 else 1) / 2) ≠ 0

@[simp]

theorem WeierstrassCurve.natDegree_preΨ' {R : Type u} [CommRing R] (W : WeierstrassCurve R) {n : ℕ} (h : ↑n ≠ 0) : (W.preΨ' n).natDegree = (n ^ 2 - if Even n then 4 else 1) / 2

theorem WeierstrassCurve.natDegree_preΨ'_pos {R : Type u} [CommRing R] (W : WeierstrassCurve R) {n : ℕ} (hn : 2 < n) (h : ↑n ≠ 0) : 0 < (W.preΨ' n).natDegree

@[simp]

theorem WeierstrassCurve.leadingCoeff_preΨ' {R : Type u} [CommRing R] (W : WeierstrassCurve R) {n : ℕ} (h : ↑n ≠ 0) : (W.preΨ' n).leadingCoeff = ↑(if Even n then n / 2 else n)

theorem WeierstrassCurve.preΨ'_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) [Nontrivial R] {n : ℕ} (h : ↑n ≠ 0) : W.preΨ' n ≠ 0

theorem WeierstrassCurve.natDegree_preΨ_le {R : Type u} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : (W.preΨ n).natDegree ≤ (n.natAbs ^ 2 - if Even n then 4 else 1) / 2

@[simp]

theorem WeierstrassCurve.coeff_preΨ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : (W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) = ↑(if Even n then n / 2 else n)

theorem WeierstrassCurve.coeff_preΨ_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) {n : ℤ} (h : ↑n ≠ 0) : (W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) ≠ 0

@[simp]

theorem WeierstrassCurve.natDegree_preΨ {R : Type u} [CommRing R] (W : WeierstrassCurve R) {n : ℤ} (h : ↑n ≠ 0) : (W.preΨ n).natDegree = (n.natAbs ^ 2 - if Even n then 4 else 1) / 2

theorem WeierstrassCurve.natDegree_preΨ_pos {R : Type u} [CommRing R] (W : WeierstrassCurve R) {n : ℤ} (hn : 2 < n.natAbs) (h : ↑n ≠ 0) : 0 < (W.preΨ n).natDegree

@[simp]

theorem WeierstrassCurve.leadingCoeff_preΨ {R : Type u} [CommRing R] (W : WeierstrassCurve R) {n : ℤ} (h : ↑n ≠ 0) : (W.preΨ n).leadingCoeff = ↑(if Even n then n / 2 else n)

theorem WeierstrassCurve.preΨ_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) [Nontrivial R] {n : ℤ} (h : ↑n ≠ 0) : W.preΨ n ≠ 0

theorem WeierstrassCurve.natDegree_ΨSq_le {R : Type u} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : (W.ΨSq n).natDegree ≤ n.natAbs ^ 2 - 1

@[simp]

theorem WeierstrassCurve.coeff_ΨSq {R : Type u} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : (W.ΨSq n).coeff (n.natAbs ^ 2 - 1) = ↑n ^ 2

theorem WeierstrassCurve.coeff_ΨSq_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) [NoZeroDivisors R] {n : ℤ} (h : ↑n ≠ 0) : (W.ΨSq n).coeff (n.natAbs ^ 2 - 1) ≠ 0

@[simp]

theorem WeierstrassCurve.natDegree_ΨSq {R : Type u} [CommRing R] (W : WeierstrassCurve R) [NoZeroDivisors R] {n : ℤ} (h : ↑n ≠ 0) : (W.ΨSq n).natDegree = n.natAbs ^ 2 - 1

theorem WeierstrassCurve.natDegree_ΨSq_pos {R : Type u} [CommRing R] (W : WeierstrassCurve R) [NoZeroDivisors R] {n : ℤ} (hn : 1 < n.natAbs) (h : ↑n ≠ 0) : 0 < (W.ΨSq n).natDegree

@[simp]

theorem WeierstrassCurve.leadingCoeff_ΨSq {R : Type u} [CommRing R] (W : WeierstrassCurve R) [NoZeroDivisors R] {n : ℤ} (h : ↑n ≠ 0) : (W.ΨSq n).leadingCoeff = ↑n ^ 2

theorem WeierstrassCurve.ΨSq_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) [NoZeroDivisors R] {n : ℤ} (h : ↑n ≠ 0) : W.ΨSq n ≠ 0

theorem WeierstrassCurve.natDegree_Φ_le {R : Type u} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : (W.Φ n).natDegree ≤ n.natAbs ^ 2

@[simp]

theorem WeierstrassCurve.coeff_Φ {R : Type u} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : (W.Φ n).coeff (n.natAbs ^ 2) = 1

theorem WeierstrassCurve.coeff_Φ_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) [Nontrivial R] (n : ℤ) : (W.Φ n).coeff (n.natAbs ^ 2) ≠ 0

@[simp]

theorem WeierstrassCurve.natDegree_Φ {R : Type u} [CommRing R] (W : WeierstrassCurve R) [Nontrivial R] (n : ℤ) : (W.Φ n).natDegree = n.natAbs ^ 2

theorem WeierstrassCurve.natDegree_Φ_pos {R : Type u} [CommRing R] (W : WeierstrassCurve R) [Nontrivial R] {n : ℤ} (hn : n ≠ 0) : 0 < (W.Φ n).natDegree

@[simp]

theorem WeierstrassCurve.leadingCoeff_Φ {R : Type u} [CommRing R] (W : WeierstrassCurve R) [Nontrivial R] (n : ℤ) : (W.Φ n).leadingCoeff = 1

theorem WeierstrassCurve.Φ_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) [Nontrivial R] (n : ℤ) : W.Φ n ≠ 0