Torsion points over a separably closed field are already rational

An n-torsion point of W with coordinates in an extension of a separably closed F already has them in F, provided n is invertible in F. Its abscissa is integral over F with separable minimal polynomial, and the ordinate then solves a quadratic whose other root is its negative.

Invertibility of n is what the separability rests on, and it cannot be dropped. Over the separable closure K of 𝔽₂(t) the curve y² + xy = x³ + t has discriminant t, so it is elliptic, and its nonzero 2-torsion point is (0, √t): the geometric 2-torsion is nontrivial while the 2-torsion over K itself is not.

Main results

• WeierstrassCurve.mem_range_x_of_zsmul_eq_zero_of_isSepClosed: the abscissa of an n-torsion point over an extension of a separably closed field, with n invertible, is already rational.
• WeierstrassCurve.mem_range_baseChange_of_zsmul_eq_zero_of_isSepClosed: the whole torsion point is the base change of one over the separably closed field.

References

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

theorem WeierstrassCurve.mem_range_x_of_zsmul_eq_zero_of_isSepClosed {F : Type u_1} [Field F] [IsSepClosed 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) : x ∈ Set.range ⇑(algebraMap F Ω)

The abscissa of a torsion point is rational over a separably closed field in which the index is invertible: it is integral over the base field and its minimal polynomial is separable, so a separably closed field already contains it.

theorem WeierstrassCurve.mem_range_baseChange_of_zsmul_eq_zero_of_isSepClosed {F : Type u_1} [Field F] [IsSepClosed F] (W : WeierstrassCurve F) [W.IsElliptic] {Ω : Type u_2} [Field Ω] [Algebra F Ω] [DecidableEq F] [DecidableEq Ω] {n : ℤ} (hchar : ↑n ≠ 0) {P : (W.baseChange Ω).toAffine.Point} (h : n • P = 0) : P ∈ Set.range ⇑(Affine.Point.baseChange F Ω)

A torsion point over an extension of a separably closed field is already rational when its index is invertible there: both of its coordinates are separable over the base field.