Kummer fields of local powers have local degree one

Let K be a number field containing the n-th roots of unity, Δ a subgroup of Kˣ with finite image in Kˣ ⧸ (Kˣ)ⁿ, and M = K(Δ^{1/n}) its Kummer field. If every element of Δ is an n-th power in the completion K_v at a place v, finite or infinite, then every completion M_w above v is K_v itself: the place v splits completely in M.

Indeed M is generated by n-th roots y of elements a ∈ Δ. If a = cⁿ in K_v, then the images of y and c in M_w have the same n-th power, so they differ by an n-th root of unity, which comes from K (TauCeti.mem_range_algebraMap_of_pow_eq). So M is generated by elements whose images in M_w come from K_v (TauCeti.adjoin_pow_eq_algebraMap_kummerField_eq_top), and the decomposition group of w is trivial (IsDedekindDomain.HeightOneSpectrum.finrank_adicCompletion_eq_one_of_adjoin_eq_top and NumberField.InfinitePlace.finrank_completion_eq_one_of_adjoin_eq_top).

This is the splitting half of Kummer theory over a number field, used in the Kummer-theoretic steps of global class field theory: the Kummer extension generated by S-units that are local n-th powers at the places of S and at the infinite places splits completely there.

Main results

• TauCeti.NumberField.finrank_adicCompletion_kummerField_eq_one: if every element of Δ is an n-th power in K_v at a finite place v, every completion of K(Δ^{1/n}) above v has degree one over K_v.
• TauCeti.NumberField.finrank_completion_kummerField_eq_one: the same at an infinite place.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, §§6 and 9, where these fields are used.
• J. Neukirch, Algebraic Number Theory, Chapter II, §9, for decomposition groups and completions.

theorem TauCeti.NumberField.finrank_adicCompletion_kummerField_eq_one {K : Type u_1} {E : Type u_2} [Field K] [NumberField K] [Field E] [Algebra K E] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity K n] {Δ : Subgroup Kˣ} [(powMonoidHom n).range.IsFiniteRelIndex Δ] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hv : ∀ a ∈ Δ, ∃ (c : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v), c ^ n = (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ↑a) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ↥(kummerField E n Δ))) [w.asIdeal.LiesOver v.asIdeal] : Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion (↥(kummerField E n Δ)) w) = 1

Local powers split completely in the Kummer field: finite places. If every element of Δ is an n-th power in the completion K_v at a finite place v, then every completion of K(Δ^{1/n}) above v has degree one over K_v.

theorem TauCeti.NumberField.finrank_completion_kummerField_eq_one {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra K E] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity K n] {Δ : Subgroup Kˣ} {v : NumberField.InfinitePlace K} (hv : ∀ a ∈ Δ, ∃ (c : v.Completion), c ^ n = (algebraMap K v.Completion) ↑a) (w : NumberField.InfinitePlace ↥(kummerField E n Δ)) [w.LiesOver v] : Module.finrank v.Completion w.Completion = 1

Local powers split completely in the Kummer field: infinite places. If every element of Δ is an n-th power in the completion K_v at an infinite place v, then every completion of K(Δ^{1/n}) above v has degree one over K_v.