The $x - e$ Kummer image over a number field is finite

Open

BSD.finite_kummer_image

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

bsdelliptic-curvesnumber-theory

Let $K$ be a number field, let $E/K$ be an elliptic curve, and let $e \in K$ be a root of the 2-torsion polynomial $\psi_2$ . Then the set of classes $(x - e) \bmod (K^\times)^2$ , as $(x, y)$ ranges over the affine points of $E(K)$ with $x \neq e$ , is finite.

Proof idea: if $\mathfrak p$ is a prime of good reduction not dividing 2, then $v_{\mathfrak p}(x - e)$ is even. So every such class lies in the Selmer-type group $K(S, 2)$ of classes that are unramified outside a finite set $S$ of primes. That group is finite because the class group is finite and the $S$ -units are finitely generated.

Preamble

import Mathlib

Formal statement

namespace BSD
theorem finite_kummer_image (K : Type*) [Field K] [NumberField K]
    (W : WeierstrassCurve K) [W.IsElliptic] (e : K) (he : W.twoTorsionPolynomial.toPoly.IsRoot e) :
    {c : Kˣ ⧸ (powMonoidHom 2 : Kˣ →* Kˣ).range |
      ∃ x y : K, W.toAffine.Nonsingular x y ∧
        ∃ hx : x - e ≠ 0, c = QuotientGroup.mk (Units.mk0 (x - e) hx)}.Finite := by sorry
end BSD

Source

Silverman, The Arithmetic of Elliptic Curves (2nd ed.), Ch. X, Prop. 1.4 and Ch. VIII, Prop. 1.5–1.6 (proof of the weak Mordell–Weil theorem via the Kummer pairing, full 2-torsion case)

View graph

The x−ex - ex−e Kummer image over a number field is finite

The $x - e$ Kummer image over a number field is finite