Torsion points over an algebraically closed field are already rational

Over an algebraically closed F, a torsion point of W with coordinates in an extension Ω has its coordinates in F: the extension buys no new torsion. No condition on the index is needed, because an algebraically closed field also extracts the inseparable roots that a torsion point of an index divisible by the characteristic has; the companion statements over a merely separably closed field ask for an invertible index in exchange.

Main results

• WeierstrassCurve.mem_range_x_of_zsmul_eq_zero_of_isAlgClosed: over an algebraically closed F, the x-coordinate of an n-torsion point of W over an extension lies in the image of F.
• WeierstrassCurve.mem_range_baseChange_of_zsmul_eq_zero_of_isAlgClosed: such an n-torsion point is therefore the base change of one over F.

References

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

theorem WeierstrassCurve.mem_range_x_of_zsmul_eq_zero_of_isAlgClosed {F : Type u_1} [Field F] [IsAlgClosed F] (W : WeierstrassCurve F) [W.IsElliptic] {Ω : Type u_2} [Field Ω] [Algebra F Ω] {n : ℤ} (hn : 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 x-coordinate of a torsion point is rational when the base field is algebraically closed: integrality then puts it in the image of F.

theorem WeierstrassCurve.mem_range_baseChange_of_zsmul_eq_zero_of_isAlgClosed {F : Type u_1} [Field F] [IsAlgClosed F] (W : WeierstrassCurve F) [W.IsElliptic] {Ω : Type u_2} [Field Ω] [Algebra F Ω] [DecidableEq F] [DecidableEq Ω] {n : ℤ} (hn : 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 an algebraically closed field is already rational. No field extension of an algebraically closed F buys new torsion: the coordinates of a torsion point are integral over F, hence already in it. So the n-torsion of W over Ω is the base change of the n-torsion over F, for every extension Ω and not only an algebraic one.