Adjoining roots of unity as an intermediate field

Adjoining one primitive m-th root of unity to K inside M gives the same intermediate field as adjoining all the m-th roots of unity, and that intermediate field K(ζ) is an m-th cyclotomic extension of K.

Mathlib proves the corresponding statements for Algebra.adjoin, in IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic, IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots and IsPrimitiveRoot.adjoin_isCyclotomicExtension. This file carries them across IntermediateField.adjoin_toSubalgebra to the IntermediateField lattice, which is where the Galois correspondence needs them. Neither result asks anything of the ambient extension M / K, since a root of unity is algebraic over K on its own.

Main results

• IsPrimitiveRoot.adjoin_singleton_eq_adjoin_nth_roots: K(ζ) = K(μ_m).
• IsPrimitiveRoot.isCyclotomicExtension_adjoin_singleton: K(ζ) / K is an m-th cyclotomic extension.

theorem IsPrimitiveRoot.adjoin_singleton_eq_adjoin_nth_roots {K : Type u_1} {M : Type u_2} [Field K] [Field M] [Algebra K M] {m : ℕ} [NeZero m] {ζ : M} (hζ : IsPrimitiveRoot ζ m) : K⟮ζ⟯ = IntermediateField.adjoin K {b : M | b ^ m = 1}

Adjoining one primitive m-th root adjoins them all. K(ζ) = K(μ_m) inside any extension of K containing a primitive m-th root of unity ζ.

No algebraicity of the ambient extension is needed: each m-th root of unity is algebraic on its own, being a root of the nonzero polynomial X ^ m - 1.

theorem IsPrimitiveRoot.isCyclotomicExtension_adjoin_singleton {K : Type u_1} {M : Type u_2} [Field K] [Field M] [Algebra K M] {m : ℕ} [NeZero m] {ζ : M} (hζ : IsPrimitiveRoot ζ m) : IsCyclotomicExtension {m} K ↥K⟮ζ⟯

K(ζ) is an m-th cyclotomic extension of K. Mathlib's IsPrimitiveRoot.intermediateField_adjoin_isCyclotomicExtension asks the whole ambient extension M / K to be integral; only ζ needs to be, and a root of unity always is, being a root of X ^ m - 1.