Unramified primes in Kummer fields

The finite Kummer field generated by roots of a subgroup of local units is unramified at every prime avoiding the exponent. The ambient field containing the roots need not itself be a number field: in particular, it can be the separable closure. This gives the ramification input for norm computations in extensions generated by roots of S-units.

In particular, ramifiedSupport_kummerField_sUnits_subset shows that the field generated by n-th roots of the S-units has its ramified support contained in S, when S contains the primes dividing n. This is the ramification hypothesis in the placewise proof that Kummer ideles are norms from that field.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, Appendix, Proposition A.5, and §9, Lemma 9.3.
• J. Neukirch, Algebraic Number Theory, Chapter III, §2.

instance TauCeti.NumberField.instNumberFieldSubtypeMemIntermediateFieldKummerField {K : Type u_1} {E : Type u_2} [Field K] [NumberField K] [Field E] [Algebra K E] {n : ℕ} [NeZero n] {Δ : Subgroup Kˣ} [(powMonoidHom n).range.IsFiniteRelIndex Δ] : NumberField ↥(kummerField E n Δ)

A finite Kummer extension of a number field is a number field, even when its ambient field is infinite over the base. The base need not contain the n-th roots of unity.

theorem TauCeti.NumberField.isUnramifiedIn_kummerField_of_valuation_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)} (hn : ↑n ∉ v.asIdeal) (hΔ : ∀ a ∈ Δ, (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑a = 1) : Algebra.IsUnramifiedIn (NumberField.RingOfIntegers ↥(kummerField E n Δ)) v.asIdeal

A finite Kummer field generated by roots of v-units is unramified at v, provided v does not divide the exponent. The ambient field E may be infinite over K.

theorem TauCeti.NumberField.ramifiedSupport_kummerField_subset {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 Δ] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), ↑n ∈ v.asIdeal → v ∈ S) (hΔ : Δ ≤ (↑S).unit K) : ramifiedSupport K ↥(kummerField E n Δ) ⊆ S

The ramified support of a finite Kummer field of a subgroup of the S-units is contained in S, when S contains the primes dividing the exponent.

theorem TauCeti.NumberField.ramifiedSupport_kummerField_sUnits_subset {K : Type u_1} {E : Type u_2} [Field K] [NumberField K] [Field E] [Algebra K E] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity K n] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), ↑n ∈ v.asIdeal → v ∈ S) : ramifiedSupport K ↥(kummerField E n ((↑S).unit K)) ⊆ S

The field generated by the n-th roots of the S-units is unramified outside S, provided S contains every prime dividing n. The roots may be taken in the separable closure.

theorem TauCeti.NumberField.isUnramifiedAt_kummerField_sUnits_of_notMem {K : Type u_1} {E : Type u_2} [Field K] [NumberField K] [Field E] [Algebra K E] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity K n] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), ↑n ∈ v.asIdeal → v ∈ S) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (hv : v ∉ S) (Q : Ideal (NumberField.RingOfIntegers ↥(kummerField E n ((↑S).unit K)))) [Q.IsPrime] [Q.LiesOver v.asIdeal] : Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q

The Kummer field of the S-units is unramified at every place outside S, when S contains the places above n.