Local Kummer sequence: $H^1(G_{K_v},E[n])/\mathrm{im}\,\kappa_v\cong H^1(G_{K_v},E)[n]$

Open

SelmerGroup.local_kummer_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, $n\ge1$ , and $L$ any field containing $K$ (for instance a completion $K_v$ ). Let $j_L:H^1(G_L,E(\bar L)[n])\to H^1(G_L,E(\bar L))$ be induced by inclusion and $\mathrm{im}\,\kappa_L$ the image of the Kummer map. Then

for every $\xi\in H^1(G_L,E[n])$ : $\ j_L(\xi)=0 \iff \xi\in\mathrm{im}\,\kappa_L$ ;
the image of $j_L$ is exactly the $n$ -torsion:

j_L\big(H^1(G_L,E[n])\big)=H^1(G_L,E)[n].

Together these say $H^1(G_L,E[n])/\mathrm{im}\,\kappa_L\cong H^1(G_L,E)[n]$ , which the source notes for $L=K_v$ .

Formalization Note The statement is made for an arbitrary field $L$ over $K$ (hence of characteristic $0$ ), which covers every completion $K_v$ .

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 local_kummer_sequence {K : Type*} [Field K] [NumberField K] (E : WeierstrassCurve K)
    [E.IsElliptic] (n : ℕ) (hn : 0 < n) (L : Type*) [Field L] [Algebra K L] :
    (∀ ξ : H1 (absTorsAct E L n), torsInclH1 E L n ξ = 0 ↔ ξ ∈ kummerImage E L n) ∧
    Set.range (torsInclH1 E L n) = {η : H1 (absAct E L) | n • η = 0} := 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

Local Kummer sequence: H1(GKv,E[n])/im κv≅H1(GKv,E)[n]H^1(G_{K_v},E[n])/\mathrm{im}\,\kappa_v\cong H^1(G_{K_v},E)[n]H1(GKv​​,E[n])/imκv​≅H1(GKv​​,E)[n]

Local Kummer sequence: $H^1(G_{K_v},E[n])/\mathrm{im}\,\kappa_v\cong H^1(G_{K_v},E)[n]$