Selmer classes of radicals unramified outside S

Let R ⊆ B be Dedekind domains with fraction fields K ⊆ L, let S be a set of height-one primes of R and let a ∈ Kˣ have an n-th root α ∈ L. If a height-one prime w of B lying over v has ramification index one, then α ^ n = a read in the w-adic valuation gives v(a) = w(α) ^ n (IsDedekindDomain.HeightOneSpectrum.valuation_eq_pow_of_pow_eq), so the v-adic order of a is divisible by n. Consequently, if every prime v ∉ S has a prime of B above it with ramification index one, the class of a lies in the Selmer group K⟮S, n⟯ (IsDedekindDomain.selmerGroup.mk_mem_of_pow_eq).

When the classes of the primes in S generate the class group of R, every Selmer class comes from an S-unit (IsDedekindDomain.selmerGroup.exists_mul_pow_mem_unit), so a is an S-unit up to an n-th power of K. This is the half of Kummer theory over a Dedekind domain saying that a radical extension unramified outside S is generated by a radical of an S-unit.

Main results

• IsDedekindDomain.HeightOneSpectrum.valuation_eq_pow_of_pow_eq: at a prime of ramification index one, v(a) = w(α) ^ n when α ^ n = a.
• IsDedekindDomain.selmerGroup.mk_mem_of_pow_eq: an element of Kˣ with an n-th root in an extension in which every prime outside S has an unramified prime above it has its class in K⟮S, n⟯.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, §6 and the appendix on Kummer theory.

theorem IsDedekindDomain.HeightOneSpectrum.valuation_eq_pow_of_pow_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {L : Type u_3} [Field L] [Algebra K L] {B : Type u_4} [CommRing B] [IsDedekindDomain B] [Algebra R B] [Module.IsTorsionFree R B] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] (hw : w.asIdeal.ramificationIdx R = 1) {n : ℕ} {α : L} {a : K} (h : α ^ n = (algebraMap K L) a) : (valuation K v) a = (valuation L w) α ^ n

The valuation of a radicand at a prime of ramification index one. If α ^ n = a with a ∈ K and the prime w of B above v has ramification index one over R, then the v-adic valuation of a is the n-th power of the w-adic valuation of α.

theorem IsDedekindDomain.selmerGroup.mk_mem_of_pow_eq {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {L : Type u_3} [Field L] [Algebra K L] {B : Type u_4} [CommRing B] [IsDedekindDomain B] [Algebra R B] [Module.IsTorsionFree R B] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] {S : Set (HeightOneSpectrum R)} {n : ℕ} {α : L} {a : Kˣ} (h : α ^ n = (algebraMap K L) ↑a) (hS : ∀ v ∉ S, ∃ (w : HeightOneSpectrum B), w.asIdeal.LiesOver v.asIdeal ∧ w.asIdeal.ramificationIdx R = 1) : ↑a ∈ selmerGroup

A radical unramified outside S gives a Selmer class. If a ∈ Kˣ has an n-th root in L and every prime v ∉ S has a prime of B above it with ramification index one, then the class of a in Kˣ ⧸ (Kˣ)ⁿ lies in the Selmer group K⟮S, n⟯.