The Selmer group of a number field is finite

The finiteness proved in TauCeti.RingTheory.DedekindDomain.SInteger.SelmerGroup.Basic asks its Dedekind domain for a finite class group and a finitely generated unit group. For the ring of integers of a number field both are theorems of Mathlib -- the class number theorem and Dirichlet's unit theorem -- so there the Selmer group K(S, n) is finite with no hypothesis beyond the finiteness of S.

Main results

• IsDedekindDomain.finite_selmerGroup_of_numberField: K(S, n) is finite for every finite S and every n with NeZero n.

References

Adapted from Michael Stoll's elliptic-curves formalisation (github.com/MichaelStollBayreuth/EllipticCurves, EllipticCurves/Mathlib/SelmerGroup.lean at the EllipticCurves roadmap's pin 66889eada51a, Apache 2.0, by Michael Stoll), where the same specialisation is drawn from the general finiteness statement.

theorem IsDedekindDomain.finite_selmerGroup_of_numberField (F : Type u_1) [Field F] [NumberField F] (S : Set (HeightOneSpectrum (NumberField.RingOfIntegers F))) (n : ℕ) [NeZero n] (hS : S.Finite) : Finite ↥selmerGroup

The Selmer group K(S, n) of a number field is finite for S finite and n with NeZero n.