Kummer classes unramified outside S and the Selmer group K(S, n)

Let R be a Dedekind domain with finite residue fields and fraction field K, let n be a natural number invertible in K, and let S be a set of height-one primes of R containing every prime that divides n. For each prime v fix a K-embedding τ v : Kˢ → K_vˢ of separable closures, along which a class of H¹(G_K, μₙ) restricts to a class of H¹(G_{K_v}, μₙ). A class is unramified outside S when, for every v ∉ S, its restriction to K_v vanishes on the inertia subgroup of K_v (TauCeti.unramifiedOutsideKummerCohomology).

Under the Kummer isomorphism Kˣ ⧸ (Kˣ)ⁿ ≃ H¹(G_K, μₙ) these are exactly the classes of the Selmer group K(S, n), the power classes whose v-adic valuation is divisible by n at every v ∉ S (TauCeti.kummerMap_mem_unramifiedOutsideKummerCohomology_iff). Indeed restriction to K_v carries the Kummer class of a ∈ Kˣ to the Kummer class of its image in K_v (TauCeti.explicitMap1_kummerMap), which is unramified exactly when n divides the normalized valuation of a at v (TauCeti.explicitRes1_kummerMap_eq_zero_iff, using that v does not divide n). In particular, under these hypotheses the condition does not depend on the chosen embeddings τ.

Over a number field, the finiteness of K(S, n) turns this into the finiteness of the classes unramified outside a finite S; see TauCeti/NumberTheory/NumberField/Kummer/SelmerGroup.lean.

Main definitions

• TauCeti.unramifiedOutsideKummerCohomology τ S n: the classes of H¹(G_K, μₙ) whose restriction to every K_v with v ∉ S vanishes on inertia.

Main results

• TauCeti.kummerMap_mem_unramifiedOutsideKummerCohomology_iff: the Kummer class of a ∈ Kˣ is unramified outside S exactly when the power class of a lies in K(S, n).
• TauCeti.mem_unramifiedOutsideKummerCohomology_iff_exists: the classes unramified outside S are exactly the Kummer classes of the elements of K(S, n).

References

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

noncomputable def TauCeti.unramifiedOutsideKummerCohomology {R : Type u_1} [CommRing R] [IsDedekindDomain R] [∀ (v : IsDedekindDomain.HeightOneSpectrum R), Finite (R ⧸ v.asIdeal)] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (τ : (v : IsDedekindDomain.HeightOneSpectrum R) → SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (n : ℕ) : AddSubgroup (ContCohomology.H1 (AbsoluteGaloisGroup K) (KummerCoeff K n))

The Kummer classes unramified outside S: the classes of H¹(G_K, μₙ) whose restriction to the completion K_v along τ v, for every prime v ∉ S, vanishes on the inertia subgroup of K_v.

theorem TauCeti.mem_unramifiedOutsideKummerCohomology_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] [∀ (v : IsDedekindDomain.HeightOneSpectrum R), Finite (R ⧸ v.asIdeal)] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {τ : (v : IsDedekindDomain.HeightOneSpectrum R) → SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {S : Set (IsDedekindDomain.HeightOneSpectrum R)} {n : ℕ} {c : ContCohomology.H1 (AbsoluteGaloisGroup K) (KummerCoeff K n)} : c ∈ unramifiedOutsideKummerCohomology τ S n ↔ ∀ v ∉ S, (ContCohomology.explicitRes1 (AbsoluteGaloisGroup (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (KummerCoeff (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) n) (Subgroup.map (absoluteGaloisGroupRestrictEquiv (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).toMonoidHom (inertiaSubgroup (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)))) ((ContCohomology.explicitMap1 (AbsoluteGaloisGroup K) (KummerCoeff K n) (AbsoluteGaloisGroup (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (KummerCoeff (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) n) (absoluteGaloisGroupMap (τ v)) (kummerCoeffBaseChange n (τ v)) ⋯ ⋯) c) = 0

A class is unramified outside S exactly when, at every v ∉ S, its restriction to K_v vanishes on inertia.

theorem TauCeti.kummerMap_mem_unramifiedOutsideKummerCohomology_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] [∀ (v : IsDedekindDomain.HeightOneSpectrum R), Finite (R ⧸ v.asIdeal)] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {τ : (v : IsDedekindDomain.HeightOneSpectrum R) → SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {S : Set (IsDedekindDomain.HeightOneSpectrum R)} {n : ℕ} (hn : IsUnit ↑n) (hS : ∀ v ∉ S, ↑n ∉ v.asIdeal) (a : Kˣ) : Multiplicative.toAdd ((kummerMap K n hn) a) ∈ unramifiedOutsideKummerCohomology τ S n ↔ ↑a ∈ IsDedekindDomain.selmerGroup

Kummer classes unramified outside S are the Selmer group K(S, n). If n is invertible in K and no prime outside S divides n, the Kummer class of a ∈ Kˣ is unramified outside S exactly when the power class of a lies in K(S, n), that is, when n divides the v-adic valuation of a at every v ∉ S.

theorem TauCeti.mem_unramifiedOutsideKummerCohomology_iff_exists {R : Type u_1} [CommRing R] [IsDedekindDomain R] [∀ (v : IsDedekindDomain.HeightOneSpectrum R), Finite (R ⧸ v.asIdeal)] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {τ : (v : IsDedekindDomain.HeightOneSpectrum R) → SeparableClosure K →ₐ[K] SeparableClosure (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)} {S : Set (IsDedekindDomain.HeightOneSpectrum R)} {n : ℕ} (hn : IsUnit ↑n) (hS : ∀ v ∉ S, ↑n ∉ v.asIdeal) {c : ContCohomology.H1 (AbsoluteGaloisGroup K) (KummerCoeff K n)} : c ∈ unramifiedOutsideKummerCohomology τ S n ↔ ∃ (a : Kˣ), ↑a ∈ IsDedekindDomain.selmerGroup ∧ Multiplicative.toAdd ((kummerMap K n hn) a) = c

The classes unramified outside S are the Kummer classes of K(S, n). If n is invertible in K and no prime outside S divides n, a class of H¹(G_K, μₙ) is unramified outside S exactly when it is the Kummer class of an element of Kˣ whose power class lies in K(S, n).