Galois descent for $E/2E$ : finiteness over $K$ implies finiteness over $\mathbb{Q}$

Proved

BSD.finiteIndex_nsmul_two_of_baseChange

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

bsdelliptic-curvesnumber-theory

Let $K/\mathbb{Q}$ be a finite Galois extension and let $W$ be any Weierstrass curve over $\mathbb{Q}$ . Write $E(\mathbb{Q})$ and $E(K)$ for the groups of nonsingular rational points of $W$ and of its base change to $K$ .

Claim. If $2E(K)$ has finite index in $E(K)$ , then $2E(\mathbb{Q})$ has finite index in $E(\mathbb{Q})$ .

Proof sketch (Silverman, AEC, Lemma VIII.1.1.1). Let $\iota : E(\mathbb{Q}) \hookrightarrow E(K)$ be the base-change map, and let $H = \iota^{-1}(2E(K))$ . The group $E(\mathbb{Q})/H$ injects into $E(K)/2E(K)$ , so it is finite. For $P \in H$ choose $Q \in E(K)$ with $2Q = \iota P$ , and define $c_P : \operatorname{Gal}(K/\mathbb{Q}) \to E(K)[2]$ by $c_P(\sigma) = \sigma Q - Q$ . If $c_P = c_{P'}$ , then $Q - Q'$ is Galois-invariant, hence equal to $\iota R$ for some $R \in E(\mathbb{Q})$ , and then $P - P' = 2R$ . Since $\operatorname{Gal}(K/\mathbb{Q})$ is finite and $E(K)[2]$ has at most $4$ elements, $H/2E(\mathbb{Q})$ is finite. The finiteness of $E(K)[2]$ holds for every Weierstrass curve in characteristic $0$ , because a 2-torsion affine point has $2y = -(a_1x + a_3)$ , which makes $x$ a root of a monic cubic.

Preamble

import Mathlib

Formal statement

namespace BSD
theorem finiteIndex_nsmul_two_of_baseChange (K : Type*) [Field K] [DecidableEq K] [Algebra ℚ K]
    [FiniteDimensional ℚ K] [IsGalois ℚ K] (W : WeierstrassCurve ℚ)
    (h : (nsmulAddMonoidHom 2 : (W.baseChange K).toAffine.Point →+
      (W.baseChange K).toAffine.Point).range.FiniteIndex) :
    (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

Galois descent for E/2EE/2EE/2E: finiteness over KKK implies finiteness over Q\mathbb{Q}Q

Galois descent for $E/2E$ : finiteness over $K$ implies finiteness over $\mathbb{Q}$