The roots of ΨSqₙ are the abscissae of the nonzero n-torsion

ΨSqₙ is the square of the n-division polynomial, pushed down to a polynomial in x alone. Its roots are exactly the x-coordinates of the affine points killed by n: one direction holds over any field, the other needs the base field algebraically closed, so that the y completing a root to a point exists.

This is the dictionary the n-torsion is counted through — the kernel of [n] maps to the roots of ΨSqₙ two-to-one away from the 2-torsion, which is what matches #ker [n] = n ² against deg preΨₙ.

Main results

• WeierstrassCurve.eval_ΨSq_eq_zero_iff_exists_zsmul_eq_zero: over an algebraically closed field, the roots of ΨSqₙ are exactly the abscissae of the n-torsion points. The pointwise form, for a supplied y, is eval_ΨSq_eq_zero_iff_zsmul_eq_zero in DivisionPolynomial/ZSMul.lean; only the existence of y needs the closure assumption.
• WeierstrassCurve.torsionBy_eq_bot_iff_forall_eval_ΨSq_ne_zero: over an algebraically closed field, the n-torsion subgroup is trivial exactly when ΨSqₙ has no root.
• WeierstrassCurve.torsionBy_two_eq_bot_iff_of_char_two and WeierstrassCurve.torsionBy_three_eq_bot_iff_of_char_three: over an algebraically closed field of characteristic 2, respectively 3, the 2-torsion is trivial exactly when a₁ = 0, and the 3-torsion exactly when b₂ = 0.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.6.4(b).

theorem WeierstrassCurve.eval_ΨSq_eq_zero_iff_exists_zsmul_eq_zero {F : Type u_1} [Field F] (W : WeierstrassCurve F) [IsAlgClosed F] [W.IsElliptic] {n : ℤ} {x : F} : Polynomial.eval x (W.ΨSq n) = 0 ↔ ∃ (y : F) (hns : W.toAffine.Nonsingular x y), n • Jacobian.Point.fromAffine (Affine.Point.some x y hns) = 0

Over an algebraically closed field the roots of ΨSqₙ are exactly the abscissae of the n-torsion points. Solving the Weierstrass equation for y gives a point over a root, and ΨSqₙ(x) = 0 makes ψₙ vanish there, which annihilates it; the converse needs no closure, since the y is supplied.

theorem WeierstrassCurve.torsionBy_eq_bot_iff_forall_eval_ΨSq_ne_zero {F : Type u_1} [Field F] (W : WeierstrassCurve F) [IsAlgClosed F] [W.IsElliptic] [DecidableEq F] {n : ℤ} : AddSubgroup.torsionBy W.toAffine.Point n = ⊥ ↔ ∀ (x : F), Polynomial.eval x (W.ΨSq n) ≠ 0

Over an algebraically closed field the n-torsion is trivial exactly when ΨSqₙ has no root: a root is the abscissa of a nonzero affine n-torsion point, and the point at infinity is the only point with no abscissa.

Characteristic two and three

theorem WeierstrassCurve.torsionBy_two_eq_bot_iff_of_char_two {F : Type u_1} [Field F] (W : WeierstrassCurve F) [IsAlgClosed F] [W.IsElliptic] [DecidableEq F] [CharP F 2] : AddSubgroup.torsionBy W.toAffine.Point 2 = ⊥ ↔ W.a₁ = 0

In characteristic 2 the 2-torsion of an elliptic curve over an algebraically closed field is trivial exactly when a₁ = 0: then ΨSq₂ = a₃² is a nonzero constant, and otherwise x = a₃ / a₁ is a root of ΨSq₂ = a₁² x² + a₃².

theorem WeierstrassCurve.torsionBy_three_eq_bot_iff_of_char_three {F : Type u_1} [Field F] (W : WeierstrassCurve F) [IsAlgClosed F] [W.IsElliptic] [DecidableEq F] [CharP F 3] : AddSubgroup.torsionBy W.toAffine.Point 3 = ⊥ ↔ W.b₂ = 0

In characteristic 3 the 3-torsion of an elliptic curve over an algebraically closed field is trivial exactly when b₂ = 0: there ψ₃ = b₂ x³ + b₈, whose constant term b₈ cannot vanish together with b₂, and which has a root as soon as b₂ ≠ 0.