Weak Mordell–Weil with full rational 2-torsion over a number field

Open

BSD.weak_mordell_weil_of_splits

by korbonits · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

bsdelliptic-curvesnumber-theory

Let $K$ be a number field and let $E$ be an elliptic curve over $K$ , given by a Weierstrass equation $y^2 + a_1xy + a_3y = x^3 + a_2x^2 + a_4x + a_6$ with coefficients in $K$ and non-zero discriminant. Suppose the 2-torsion is fully $K$ -rational: the 2-torsion polynomial

\psi_2(X) = 4X^3 + b_2X^2 + 2b_4X + b_6

(Mathlib's twoTorsionPolynomial, whose roots are the $x$ -coordinates of the non-zero 2-torsion points) splits into linear factors over $K$ .

Claim. The subgroup $2E(K)$ has finite index in $E(K)$ , i.e. $E(K)/2E(K)$ is finite.

This is the full-2-torsion case of the weak Mordell–Weil theorem. Write $\psi_2(X) = 4(X-e_1)(X-e_2)(X-e_3)$ with distinct $e_i \in K$ (distinct because $\operatorname{disc}\psi_2 = 16\Delta \neq 0$ ). Let $S$ be the set of primes of $K$ dividing $2\Delta$ , together with enough primes to make the ring of $S$ -integers a PID, or else work with the Selmer group $K(S,2)$ . The Kummer map

\delta : E(K) \to (K^\times/K^{\times 2})^2, \qquad (x,y) \mapsto (x - e_1,\; x - e_2)

(with the usual modification at the 2-torsion points) is a homomorphism with kernel exactly $2E(K)$ . Its image lies in $K(S,2)^2$ , which is finite by finiteness of the class group and finite generation of the $S$ -units. See IsDedekindDomain.selmerGroup.finite_of_finite_classGroup_of_fg_units, which is already proved on the platform.

Preamble

import Mathlib

Formal statement

namespace BSD
theorem weak_mordell_weil_of_splits (K : Type*) [Field K] [DecidableEq K] [NumberField K]
    (W : WeierstrassCurve K) [W.IsElliptic] (hs : W.twoTorsionPolynomial.toPoly.Splits) :
    (nsmulAddMonoidHom 2 : W.toAffine.Point →+ W.toAffine.Point).range.FiniteIndex := by sorry
end BSD

Source

Silverman, The Arithmetic of Elliptic Curves (2nd ed.), Ch. VIII §1: Lemma VIII.1.1.1 (reduction to K ⊇ E[m]) and Prop. X.1.4 (explicit 2-descent); cf. Wiles, 'The Birch and Swinnerton-Dyer Conjecture' (Clay), p. 1.

View graph