A torsion point's x-coordinate is integral over the base field

ΨSqₙ is a nonzero polynomial over the base field whenever n ≠ 0 and the curve is nonsingular, and a torsion point is a root of it. So the x-coordinate of an affine point killed by a nonzero n is integral over the base, with no hypothesis on the extension.

Over an algebraically closed base that integrality becomes rationality; that is Torsion/AlgClosed.lean, which is the only place algebraic closedness is used.

Main results

• WeierstrassCurve.isIntegral_x_of_zsmul_eq_zero: the x-coordinate of an affine point killed by a nonzero n is integral over the base field.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.6.

theorem WeierstrassCurve.isIntegral_x_of_zsmul_eq_zero {F : Type u_1} [Field 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) : IsIntegral F x

The x-coordinate of a point killed by a nonzero n is integral over the base field: it is a root of ΨSqₙ, which is a nonzero polynomial there. The nonvanishing hypothesis is on n, not on the point.