Radical extensions unramified outside S are generated by radicals of S-units

Let K be a number field and S a set of finite places of K whose classes generate the ideal class group. Inside a field E containing K, let F be a number field over K in which every finite place outside S has an unramified place above it. If α ∈ F has α ^ n = a ∈ K, then a is an S-unit up to an n-th power of K: the v-adic order of a is divisible by n at every v ∉ S (IsDedekindDomain.selmerGroup.mk_mem_of_pow_eq), and since S generates the class group every such class comes from an S-unit (IsDedekindDomain.selmerGroup.exists_mul_pow_mem_unit). Rescaling α by an element of K makes it an n-th root of an S-unit, so α lies in the Kummer field K(U_S^{1/n}) of the S-units (TauCeti.NumberField.mem_kummerField_sUnits_of_pow_eq).

If K contains the n-th roots of unity, a cyclic extension F/K of degree dividing n is generated by one such radical (Mathlib's exists_root_adjoin_eq_top_of_isCyclic), so it lies in K(U_S^{1/n}) (TauCeti.NumberField.le_kummerField_sUnits_of_isCyclic). This is the inclusion L ⊆ K(U_S^{1/p}) with which the Kummer-theoretic proof of the second fundamental inequality compares a cyclic extension L/K of prime degree p with the Kummer extension of the S-units. Together with the fact that K(U_S^{1/n}) is itself unramified outside S when S contains the places above n (Milne, VII, A.5), it identifies K(U_S^{1/n}) as the largest such extension among those generated by n-th roots.

Main results

• TauCeti.NumberField.mem_kummerField_sUnits_of_pow_eq: an n-th root of an element of K lying in an extension unramified outside S lies in K(U_S^{1/n}).
• TauCeti.NumberField.le_kummerField_sUnits_of_isCyclic: a cyclic extension of degree dividing n, unramified outside S, lies in K(U_S^{1/n}) when K contains the n-th roots of unity.

References

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

theorem TauCeti.NumberField.mem_kummerField_sUnits_of_pow_eq {K : Type u_1} {E : Type u_2} [Field K] [NumberField K] [Field E] [Algebra K E] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hS : Subgroup.closure (IsDedekindDomain.HeightOneSpectrum.classGroupMk '' S) = ⊤) {F : IntermediateField K E} [NumberField ↥F] (hF : ∀ v ∉ S, ∃ (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ↥F)), w.asIdeal.LiesOver v.asIdeal ∧ Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) w.asIdeal) {n : ℕ} {α : E} (hαF : α ∈ F) {a : K} (h : α ^ n = (algebraMap K E) a) : α ∈ kummerField E n (S.unit K)

A radical unramified outside S is a radical of an S-unit. Let the classes of the places in S generate the class group of K, and let F be an intermediate field of E/K that is a number field in which every finite place of K outside S has an unramified place above it. If α ∈ F and α ^ n ∈ K, then α lies in the Kummer field K(U_S^{1/n}) of the S-units.

theorem TauCeti.NumberField.le_kummerField_sUnits_of_isCyclic {K : Type u_1} {E : Type u_2} [Field K] [NumberField K] [Field E] [Algebra K E] {S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))} (hS : Subgroup.closure (IsDedekindDomain.HeightOneSpectrum.classGroupMk '' S) = ⊤) {n : ℕ} [HasEnoughRootsOfUnity K n] {F : IntermediateField K E} [NumberField ↥F] [IsGalois K ↥F] [IsCyclic Gal(↥F/K)] (hFn : Module.finrank K ↥F ∣ n) (hF : ∀ v ∉ S, ∃ (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ↥F)), w.asIdeal.LiesOver v.asIdeal ∧ Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) w.asIdeal) : F ≤ kummerField E n (S.unit K)

A cyclic extension unramified outside S lies in K(U_S^{1/n}). Let K contain the n-th roots of unity and let the classes of the places in S generate the class group of K. Then every cyclic Galois intermediate field F of E/K of degree dividing n, in which every finite place of K outside S has an unramified place above it, lies in the Kummer field K(U_S^{1/n}) of the S-units.