Finiteness of Selmer groups of elliptic curves

For an elliptic curve W over a number field K and a nonzero natural number m, the m-Selmer group of W is finite (Silverman X.4.2). Here the local conditions are taken at the completions of K at its finite places.

The proof passes to the division field L = K(E[m]). Restriction to L has finite kernel, and the local condition over each completion L_w lies over the condition at the completion K_v below it. Over L, every m-torsion point is rational, so the Weil pairing embeds the classes unramified outside a finite set into finitely many copies of the finite Kummer group L(S, m).

Main result

• WeierstrassCurve.finite_selmerGroup: the m-Selmer group of an elliptic curve over a number field is finite for m ≠ 0.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VIII.1 and X.4.2.

theorem WeierstrassCurve.finite_selmerGroup {K : Type u_1} [Field K] [NumberField K] (W : WeierstrassCurve K) [W.IsElliptic] (m : ℕ) [NeZero m] (τ : (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) : Finite ↥(W.selmerGroup τ m)

The m-Selmer group of an elliptic curve over a number field is finite (Silverman X.4.2). The local conditions are the images of the Kummer maps over the completions at all finite places. The conclusion holds for every nonzero natural number m.