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.lean.

Mathematical background

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

• preΨₙ has leading coefficient n / 2 and degree (n² - 4) / 2 if n is even,
• preΨₙ has leading coefficient n and degree (n² - 1) / 2 if n is odd,
• ΨSqₙ has leading coefficient n² and degree n² - 1, and
• Φₙ has leading coefficient 1 and degree n².

In particular, when R is an integral domain of characteristic different from n, the univariate polynomials preΨₙ, ΨSqₙ, and Φₙ all have their expected leading terms.

Main statements

• WeierstrassCurve.natDegree_preΨ_le: the degree bound d of preΨₙ.
• WeierstrassCurve.coeff_preΨ: the d-th coefficient of preΨₙ.
• WeierstrassCurve.natDegree_preΨ: the degree of preΨₙ when n ≠ 0.
• WeierstrassCurve.leadingCoeff_preΨ: the leading coefficient of preΨₙ when n ≠ 0.
• WeierstrassCurve.natDegree_ΨSq_le: the degree bound d of ΨSqₙ.
• WeierstrassCurve.coeff_ΨSq: the d-th coefficient of ΨSqₙ.
• WeierstrassCurve.natDegree_ΨSq: the degree of ΨSqₙ when n ≠ 0.
• WeierstrassCurve.leadingCoeff_ΨSq: the leading coefficient of ΨSqₙ when n ≠ 0.
• WeierstrassCurve.natDegree_Φ_le: the degree bound d of Φₙ.
• WeierstrassCurve.coeff_Φ: the d-th coefficient of Φₙ.
• WeierstrassCurve.natDegree_Φ: the degree of Φₙ when n ≠ 0.
• WeierstrassCurve.leadingCoeff_Φ: the leading coefficient of Φₙ when n ≠ 0.

References

J Silverman, The Arithmetic of Elliptic Curves

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