Radical extensions of number fields are unramified away from n a

Let L = K(α) be an extension of number fields generated by an n-th root α of a ∈ K. A finite place v of K at which both n and a are units is unramified in L. When α is integral, the radical generator puts n a in the different of L/K (TauCeti.natCast_mul_mem_differentIdeal_of_pow_eq), and a prime ramified over K divides the different, so it contains n a. A v-unit a is reduced to the integral case by a denominator prime to v. A field generated by several such radicals is the compositum of the fields generated by each, and is unramified at v as well. That statement is made inside a Galois extension M/K, where ramification of a compositum is read off inertia groups; this costs nothing, since the normal closure of a field generated by n-th roots of elements of K is generated by n-th roots of the same elements.

This is the ramification statement of Kummer theory over a number field (Milne, VII, A.5): if S is a finite set of finite places containing those above n, the field generated by the n-th roots of the S-units is unramified at every finite place outside S. No roots of unity are needed for this.

The two conditions are needed separately; asking only that n a be a v-unit is not enough. Over ℚ, n = p and a = 1 / p make n a = 1, yet ℚ(p^{-1/p}) = ℚ(p^{1/p}) is totally ramified at p.

Main results

• TauCeti.NumberField.isUnramifiedIn_of_pow_eq: if L = K(α) with α ∈ 𝓞 L, αⁿ = a ∈ 𝓞 K, and n a ∉ p, then p is unramified in L.
• TauCeti.NumberField.isUnramifiedIn_of_pow_eq_of_valuation_eq_one: if L = K(α) with αⁿ = a ∈ K, n ∉ v and v(a) = 1, then v is unramified in L.
• TauCeti.NumberField.isUnramifiedIn_adjoin_of_pow_eq_of_valuation_eq_one: inside a Galois extension M/K, a field K(s) generated by n-th roots of v-units is unramified at v when n ∉ v.

References

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

theorem TauCeti.NumberField.isUnramifiedIn_of_pow_eq {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] {α : NumberField.RingOfIntegers L} (hα : K⟮↑α⟯ = ⊤) {n : ℕ} {a : NumberField.RingOfIntegers K} (hαa : α ^ n = (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) a) {p : Ideal (NumberField.RingOfIntegers K)} (hp : ↑n * a ∉ p) : Algebra.IsUnramifiedIn (NumberField.RingOfIntegers L) p

A radical extension is unramified away from n a. If L = K(α) for an integral α with αⁿ = a ∈ 𝓞 K, then every prime p of 𝓞 K not containing n a is unramified in L.

theorem TauCeti.NumberField.isUnramifiedIn_of_pow_eq_of_valuation_eq_one {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] {α : L} (hα : K⟮α⟯ = ⊤) {n : ℕ} {a : K} (hαa : α ^ n = (algebraMap K L) a) {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hn : ↑n ∉ v.asIdeal) (ha : (IsDedekindDomain.HeightOneSpectrum.valuation K v) a = 1) : Algebra.IsUnramifiedIn (NumberField.RingOfIntegers L) v.asIdeal

A radical of a v-unit is unramified at v (Milne, Class Field Theory, VII, A.5). If L = K(α) with αⁿ = a ∈ K, and n and a are units at the finite place v of K, then v is unramified in L.

theorem TauCeti.NumberField.isUnramifiedIn_adjoin_of_pow_eq_of_valuation_eq_one {K : Type u_1} [Field K] [NumberField K] {M : Type u_3} [Field M] [NumberField M] [Algebra K M] [IsGalois K M] {n : ℕ} {s : Set M} {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (hs : ∀ α ∈ s, ∃ (a : K), α ^ n = (algebraMap K M) a ∧ (IsDedekindDomain.HeightOneSpectrum.valuation K v) a = 1) (hn : ↑n ∉ v.asIdeal) : Algebra.IsUnramifiedIn (NumberField.RingOfIntegers ↥(IntermediateField.adjoin K s)) v.asIdeal

A field generated by radicals of v-units is unramified at v (Milne, Class Field Theory, VII, A.5). Let M/K be a Galois extension of number fields and s a set of elements of M, each an n-th root of a v-unit of K, for a finite place v of K not dividing n. Then v is unramified in the intermediate field K(s).