The Mordell–Weil group of y² = x³ - x + 1 is ℤ

The rational points of the elliptic curve E : y² = x³ - x + 1 over ℚ form a free abelian group of rank one, so E(ℚ) ≅ ℤ. The rank is computed by explicit 2-descent through the étale algebra of the cubic x³ - x + 1, following the worked example of Stoll's EllipticCurves project (see Provenance); Silverman X.1 is general background on descent.

• Rank at least one. The rational point P = (1, 1) is nonzero, and E(ℚ) is torsion-free (TauCeti.WorkedExamples.torsion_curveX3SubXAddOne_eq_bot), so P has infinite order.
• Rank at most one. The cubic f = x³ - x + 1 is irreducible over ℚ, so the étale algebra ℚ[X] ⧸ (f) of the descent is a single cubic field L, generated by a root of f. Its discriminant disc f = -23 is squarefree, so at no finite prime does disc f vanish to order two or more, and -1 is not a square in ℚ. The descent bound WeierstrassCurve.Affine.pow_rank_add_one_le_prod therefore reads 2 ^ (rank E(ℚ) + 1) · #E(ℚ)[2] ≤ 2 ^ (r + 1) · #Cl[2], with r the unit rank and Cl the class group of the ring of integers of L. Here #E(ℚ)[2] = 1, and L is the cubic field of discriminant -23, which has unit rank 1 and class number 1 (TauCeti.NumberField.Cubic23.units_rank_eq_one, TauCeti.NumberField.Cubic23.classNumber_eq_one). So 2 ^ (rank E(ℚ) + 1) ≤ 4.

Since E(ℚ) is finitely generated (the Mordell–Weil theorem) and torsion-free, rank one makes it isomorphic to ℤ. The isomorphism is not made explicit here: identifying a generator, for instance showing that P itself generates, needs the canonical height.

Main definitions

• TauCeti.WorkedExamples.curveX3SubXAddOnePoint: the rational point (1, 1).

Main results

• TauCeti.WorkedExamples.not_isOfFinAddOrder_curveX3SubXAddOnePoint: (1, 1) has infinite order.
• TauCeti.WorkedExamples.finrank_point_curveX3SubXAddOne: the rank of E(ℚ) is one.
• TauCeti.WorkedExamples.nonempty_addEquiv_int_point_curveX3SubXAddOne: E(ℚ) ≅ ℤ.

Provenance

The curve y² = x³ - x + 1 is the worked example of explicit 2-descent in Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, commit 66889eada51a), on whose descent formalisation the bound WeierstrassCurve.Affine.pow_rank_add_one_le_prod builds; see the provenance of its file. Here the arithmetic of the cubic field is not recomputed: it is read off the cubic field of discriminant -23 through the reciprocal generator of TauCeti.NumberField.Cubic23.exists_minpoly_eq_and_adjoin_eq_top_of_root.

References

• J. Silverman, The Arithmetic of Elliptic Curves, X.1.

The point (1, 1)

def TauCeti.WorkedExamples.curveX3SubXAddOnePoint : (curveX3SubXAddOne.baseChange ℚ).toAffine.Point

The rational point (1, 1) of y² = x³ - x + 1.

@[simp]

theorem TauCeti.WorkedExamples.curveX3SubXAddOnePoint_def : curveX3SubXAddOnePoint = WeierstrassCurve.Affine.Point.some 1 1 ⋯

curveX3SubXAddOnePoint is the point (1, 1).

theorem TauCeti.WorkedExamples.not_isOfFinAddOrder_curveX3SubXAddOnePoint : ¬IsOfFinAddOrder curveX3SubXAddOnePoint

(1, 1) has infinite order.

The descent bound

theorem TauCeti.WorkedExamples.finrank_point_curveX3SubXAddOne : Module.finrank ℤ (curveX3SubXAddOne.baseChange ℚ).toAffine.Point = 1

The rank of y² = x³ - x + 1 over ℚ is one.

theorem TauCeti.WorkedExamples.nonempty_addEquiv_int_point_curveX3SubXAddOne : Nonempty ((curveX3SubXAddOne.baseChange ℚ).toAffine.Point ≃+ ℤ)

The Mordell–Weil group of y² = x³ - x + 1 over ℚ is ℤ. It is finitely generated, torsion-free and of rank one.