The rational torsion of y² = x³ - x + 1 is trivial

Reduction modulo 3 and 5 gives point groups of orders 7 and 8. A prime factor of the order of a rational torsion point must therefore divide both 3 * 7 and 5 * 8, which are coprime. This proves that the rational point group is torsion-free, using only injectivity of reduction on torsion prime to the residue characteristic.

This is the torsion calculation needed to identify this Mordell–Weil group with ℤ once its rank is known to be one. The finite counts include the point at infinity and are evaluated by the Lean kernel. The comparison of the valuation residue fields with ZMod p is explicit.

Main results

• TauCeti.WorkedExamples.card_point_curveX3SubXAddOne_zmod_three and TauCeti.WorkedExamples.card_point_curveX3SubXAddOne_zmod_five: the finite point counts.
• TauCeti.WorkedExamples.torsion_curveX3SubXAddOne_eq_bot: rational torsion is trivial.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VII.3.1 and VIII.7.

Provenance

The reduction certificate uses Affine.Point.not_isOfFinAddOrder_of_coprime, whose provenance is Michael Stoll's EllipticCurves project (Apache-2.0, commit 3bfe124). Its InfiniteOrderExample.lean studies a point on the same equation at the same two primes; here we count the entire reduced groups to exclude every nonzero rational torsion point.

theorem TauCeti.WorkedExamples.card_point_curveX3SubXAddOne_zmod_three : Nat.card (curveX3SubXAddOne.map (Int.castRingHom (ZMod 3))).toAffine.Point = 7

The reduction of y² = x³ - x + 1 modulo 3 has 7 points, including infinity.

theorem TauCeti.WorkedExamples.card_point_curveX3SubXAddOne_zmod_five : Nat.card (curveX3SubXAddOne.map (Int.castRingHom (ZMod 5))).toAffine.Point = 8

The reduction of y² = x³ - x + 1 modulo 5 has 8 points, including infinity.

@[simp]

theorem TauCeti.WorkedExamples.torsion_curveX3SubXAddOne_eq_bot : AddCommGroup.torsion (curveX3SubXAddOne.baseChange ℚ).toAffine.Point = ⊥

The rational torsion of y² = x³ - x + 1 is trivial. The reduced groups at 3 and 5 have orders 7 and 8, and 3 * 7 and 5 * 8 are coprime.

instance TauCeti.WorkedExamples.instHasUniqueDivPointRatToAffineBaseChangeIntCurveX3SubXAddOne : HasUniqueDiv (curveX3SubXAddOne.baseChange ℚ).toAffine.Point

The rational point group of y² = x³ - x + 1 is torsion-free.