$0\to E(K)/nE(K)\to\mathrm{Sel}^{(n)}(E/K)\to\text{Ш}(E/K)[n]\to0$

Open

SelmerGroup.selmer_exact_sequence

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$ . There is an injective homomorphism

\delta: E(K)/nE(K)\hookrightarrow H^1(G_K,E(\bar K)[n])

such that

$\delta$ is the Kummer map: for every $P\in E(K)$ the class $\delta(P\bmod nE(K))$ is represented by $\sigma\mapsto\sigma Q-Q$ for some $Q\in E(\bar K)$ with $nQ=P$ ;
the image of $\delta$ is $\{\xi\in\mathrm{Sel}^{(n)}(E/K): j(\xi)=0\}$ , where $j:H^1(G_K,E[n])\to H^1(G_K,E)$ is induced by inclusion;
$j$ maps $\mathrm{Sel}^{(n)}(E/K)$ onto $\text{Ш}(E/K)[n]$ .

Equivalently, the sequence $0\to E(K)/nE(K)\xrightarrow{\delta}\mathrm{Sel}^{(n)}(E/K)\xrightarrow{j}\text{Ш}(E/K)[n]\to0$ is exact.

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 selmer_exact_sequence {K : Type*} [Field K] [NumberField K] (E : WeierstrassCurve K)
    [E.IsElliptic] (n : ℕ) (hn : 0 < n) :
    ∃ δ : Pts E K ⧸ (nsmulAddMonoidHom n : Pts E K →+ Pts E K).range →+ H1 (absTorsAct E K n),
      Function.Injective δ ∧
      (∀ P : Pts E K, ∃ c : cocycles (absTorsAct E K n),
        H1.mk (absTorsAct E K n) c = δ (QuotientAddGroup.mk P) ∧
        ∃ Q : Pts E (AlgebraicClosure K),
          n • Q = ptsMap E (IsScalarTower.toAlgHom K K (AlgebraicClosure K)) P ∧
          ∀ σ, (c.1 σ : Pts E (AlgebraicClosure K)) = absAct E K σ Q - Q) ∧
      Set.range δ = {ξ | ξ ∈ selmerGroup E n ∧ torsInclH1 E K n ξ = 0} ∧
      torsInclH1 E K n '' selmerGroup E n = shaTors E n := 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

0→E(K)/nE(K)→Sel(n)(E/K)→Ш(E/K)[n]→00\to E(K)/nE(K)\to\mathrm{Sel}^{(n)}(E/K)\to\text{Ш}(E/K)[n]\to00→E(K)/nE(K)→Sel(n)(E/K)→Ш(E/K)[n]→0

$0\to E(K)/nE(K)\to\mathrm{Sel}^{(n)}(E/K)\to\text{Ш}(E/K)[n]\to0$