$\text{Ш}(E/K)[n]$ is finite

Open

SelmerGroup.shaTors_finite

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

elliptic-curvesgalois-cohomologynumber-theoryselmer-group

Let $K$ be a number field, $E/K$ an elliptic curve and $n\ge1$ . The $n$ -torsion of the Tate–Shafarevich group,

\text{Ш}(E/K)[n]=\{\xi\in\text{Ш}(E/K): n\xi=0\}\subseteq H^1(G_K,E(\bar K)),

is finite.

This is the finiteness of the part of $\text{Ш}$ killed by the isogeny $[n]$ ; the finiteness of all of $\text{Ш}(E/K)$ is a conjecture and is not claimed.

Preamble

import Mathlib
import Definitions.Def_SelmerGroup_ContinuousH1
import Definitions.Def_SelmerGroup_GaloisPoints
import Definitions.Def_SelmerGroup_Selmer

open NumberField

Formal statement

namespace SelmerGroup
theorem shaTors_finite {K : Type*} [Field K] [NumberField K] (E : WeierstrassCurve K)
    [E.IsElliptic] (n : ℕ) (hn : 0 < n) :
    (shaTors E n).Finite := by sorry
end SelmerGroup

Source

Wikipedia, "Selmer group", revision oldid=1370673670, https://en.wikipedia.org/w/index.php?title=Selmer_group&oldid=1370673670 , section "Selmer group of an isogeny" (p. 1 of the supplied PDF)

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Ш(E/K)[n]\text{Ш}(E/K)[n]Ш(E/K)[n] is finite

$\text{Ш}(E/K)[n]$ is finite