Finiteness of the Kummer classes unramified outside S

Over a Dedekind domain with finite residue fields, the classes of H¹(G_K, μₙ) unramified outside S are the Kummer classes of the Selmer group K(S, n) once S contains the primes dividing n (TauCeti.mem_unramifiedOutsideKummerCohomology_iff_exists). For a number field K and a finite S, the group K(S, n) is finite by the finiteness of the class group and Dirichlet's unit theorem (IsDedekindDomain.finite_selmerGroup_of_numberField), so the classes of H¹(G_K, μₙ) unramified outside S form a finite group (TauCeti.finite_unramifiedOutsideKummerCohomology). This is the Kummer-theoretic step in the finiteness of the Selmer groups of an elliptic curve over a number field: over a field containing the n-torsion, the Weil pairing reduces H¹(G_K, E[n]) to copies of H¹(G_K, μₙ), and the Selmer classes land in the classes unramified outside the primes of bad reduction and those dividing n.

Main results

• TauCeti.finite_unramifiedOutsideKummerCohomology: over a number field and for finite S, there are finitely many classes unramified outside S.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VIII.1, the proof of Proposition VIII.1.6, and X.4.

theorem TauCeti.finite_unramifiedOutsideKummerCohomology {K : Type u_1} [Field K] [NumberField K] {τ : (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} {n : ℕ} (hSf : S.Finite) (hn : IsUnit ↑n) : Finite ↥(unramifiedOutsideKummerCohomology τ S n)

Finiteness of the Kummer classes unramified outside S. Over a number field K, if n is invertible in K and S is a finite set of finite places, only finitely many classes of H¹(G_K, μₙ) are unramified outside S. This follows by enlarging S by the finitely many places dividing n, where the classes are the Kummer classes of the finite group K(S, n).