Finite generation of the group of rational points #
The descent is complete: the weak Mordell–Weil theorem gives that E(K)/2E(K) is finite, the
naïve height satisfies the approximate parallelogram law and the Northcott property, and Mathlib's
descent engine AddCommGroup.fg_of_descent' turns those two into finite generation of E(K).
Finiteness of the torsion subgroup comes out of the same two inputs and is Mathlib's
WeierstrassCurve.Affine.finite_torsion.
The statements are named for their conclusions, per the roadmap: no declaration is called
mordellWeil, and the classical name appears in docstrings only.
Main results #
WeierstrassCurve.Affine.fg_point:E(K)is finitely generated, for a curve in the normal formy² = f(x)over the fraction field of a Dedekind domain, under per-factor class-group and unit-group finiteness.WeierstrassCurve.Affine.fg_point_of_variableChange: the same for an arbitrary Weierstrass curve, transferred along an admissible change of variables.WeierstrassCurve.Affine.fg_point_of_numberField: the Mordell–Weil theorem —E(K)is finitely generated for an elliptic curve over a number field.
Two divergences from the source, both forced by what is already on main #
Unit groups are Monoid.FG, not Group.FG. The source states fg_point with
Group.FG (ringOfIntegersFactor R p)ˣ, but main's weak Mordell–Weil theorem
(finiteIndex_range_nsmulAddMonoidHom_two) takes Monoid.FG. Matching main avoids an
impedance mismatch at the one place the hypothesis is used; Group.fg_iff_monoid_fg converts,
and fg_point_of_numberField does exactly that when discharging it from Dirichlet's theorem.
The finiteness inputs are TauCeti's. NumberField.finite_classGroup_integralClosure and
NumberField.fg_units_integralClosure are in
TauCeti.NumberTheory.NumberField.IntegralClosure, since they are general number theory and
mention no curve.
References #
- M. Stoll, EllipticCurves, commit
66889eada51a74c2f5dfb7fb5909b0b5a0a2d96e,EllipticCurves/MordellWeil.lean(:350,:371,:390,:416), Apache-2.0. The proofs are that file's.
The Mordell–Weil theorem, general version: E(K) is finitely generated, for an elliptic
curve E given by an equation y² = f(x) with a monic cubic f (a₁ = a₃ = 0) over a field K
such that K has admissible absolute values with the Northcott property, K is the fraction
field of a Dedekind domain R, and for each irreducible factor p of f the integral closure of
R in K[X] ⧸ (p) has finite class group and finitely generated unit group.
For K a number field all of these hold; see fg_point_of_numberField.
The per-factor hypotheses cannot be replaced by the corresponding hypotheses on R itself: by a
theorem of Claborn, refined by Leedham-Green and by Clark, every abelian group is the class
group of the integral closure of a PID in a separable quadratic extension, so
Finite (ClassGroup R) gives no control over the class groups of the factors.
The Mordell–Weil theorem for an arbitrary Weierstrass curve: E(K) is finitely generated,
given an admissible change of variables C bringing E into the normal form y² = f(x),
together with the finiteness hypotheses of fg_point for the model C • E. The result transfers
along the isomorphism of point groups Point.addEquivVariableChange.
Such a C exists whenever 2 is invertible in K, by completing the square.
The Mordell–Weil theorem: the group E(K) of K-rational points of an elliptic curve E
over a number field K is finitely generated.
The square on the left-hand side is completed by an admissible change of variables, possible since
K has characteristic zero, and the finiteness hypotheses of fg_point for the resulting model
are the class number theorem and Dirichlet's unit theorem.