Division polynomials are separable when n is invertible

preΨₙ has degree (n ² - 1) / 2 for odd n and (n ² - 4) / 2 for even n, and its roots are the abscissae of the nonzero n-torsion points that are not 2-torsion. Over an algebraically closed field there are n ² - 1 of the former and at most three of the latter, and the abscissa map is two-to-one, so the roots are as numerous as the degree allows: preΨₙ has no repeated root. The same count against deg ΨSq₂ = 3 separates Ψ₂Sq, whose three roots are the abscissae of the 2-torsion and are distinct because those points are their own negatives.

Separability is insensitive to base change, so both statements descend from the algebraic closure to an arbitrary field in which n is invertible.

The consequence the torsion theory wants is the last one: the minimal polynomial of the abscissa of an n-torsion point is separable. ΨSqₙ itself need not be — it carries the factor preΨₙ ², which is repeated as soon as preΨₙ is not a unit — but a minimal polynomial is irreducible, so it divides one of the two factors and inherits that factor's separability.

Main results

• WeierstrassCurve.separable_preΨ: preΨₙ is separable when n is invertible.
• WeierstrassCurve.separable_Ψ₂Sq: Ψ₂Sq is separable when 2 is invertible.
• WeierstrassCurve.separable_minpoly_of_aeval_ΨSq_eq_zero: the minimal polynomial of a root of ΨSqₙ is separable when n is invertible.
• WeierstrassCurve.separable_minpoly_of_zsmul_eq_zero: hence so is that of the x-coordinate of an n-torsion point.

References

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

theorem WeierstrassCurve.separable_preΨ {F : Type u_1} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] {n : ℤ} (hchar : ↑n ≠ 0) : (W.preΨ n).Separable

preΨₙ is separable over any field in which n is invertible. Separability is insensitive to base change, so it descends from the algebraic closure, where the roots can be counted against the points of ker [n].

theorem WeierstrassCurve.separable_Ψ₂Sq {F : Type u_1} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] (hchar : ↑2 ≠ 0) : W.Ψ₂Sq.Separable

Ψ₂Sq is separable over any field in which 2 is invertible: its roots are the abscissae of the three nonzero 2-torsion points, which are distinct.

theorem WeierstrassCurve.separable_minpoly_of_aeval_ΨSq_eq_zero {F : Type u_1} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] {Ω : Type u_2} [Ring Ω] [IsDomain Ω] [Algebra F Ω] {n : ℤ} (hchar : ↑n ≠ 0) {x : Ω} (hroot : (Polynomial.aeval x) (W.ΨSq n) = 0) : (minpoly F x).Separable

The minimal polynomial of a root of ΨSqₙ is separable when n is invertible. ΨSqₙ itself need not be separable — it is preΨₙ ² times Ψ₂Sq at even n, so it carries a repeated factor once preΨₙ is not a unit — but a minimal polynomial is irreducible, so it divides one of those two factors and inherits that factor's separability.

theorem WeierstrassCurve.separable_minpoly_of_zsmul_eq_zero {F : Type u_1} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] {Ω : Type u_2} [Field Ω] [Algebra F Ω] {n : ℤ} (hchar : ↑n ≠ 0) {x y : Ω} (hns : (W.baseChange Ω).toAffine.Nonsingular x y) (htors : n • Jacobian.Point.fromAffine (Affine.Point.some x y hns) = 0) : (minpoly F x).Separable

The minimal polynomial of the abscissa of an n-torsion point is separable when n is invertible: such an abscissa is a root of ΨSqₙ.