Radical extensions over a field with enough roots of unity

Let K be a field containing a primitive n-th root of unity ζ, and let L = K(s) with sⁿ = b for some b ∈ K (for b = 0 the extension is trivial). The binomial Xⁿ - b need not be irreducible, so Mathlib's autEquivRootsOfUnity, which identifies Gal(L/K) with μₙ(K) for an irreducible binomial, does not apply. This file records what remains true in general: L/K is the splitting field of Xⁿ - b, hence Galois, the degree d = [L : K] divides n, and Gal(L/K) is cyclic of order d, generated by the automorphism s ↦ ζ ^ (n / d) • s.

This explicit generator is the one for which the Kummer character of b, read through ζ, sends g ^ i to (n / d) · i for 0 ≤ i < d; it is how the carry cocycle of a cyclic extension is compared with the cup product of Kummer classes.

The degree is controlled by the radicand: s ^ d lies in K, so b = (s ^ d) ^ (n / d) is an (n / d)-th power in K. Hence if b is not a p-th power in K for any prime p dividing n, then [L : K] = n and Xⁿ - b is irreducible. Mathlib proves this irreducibility criterion for odd n without roots of unity (X_pow_sub_C_irreducible_iff_forall_prime_of_odd); for even n it fails in general (X⁴ + 4 is reducible over ℚ), and a primitive n-th root of unity in K is what restores it. Together with Mathlib's autEquivZmod, this makes L/K cyclic of order n with Gal(L/K) acting on s through the n-th roots of unity: Kummer extensions in the sense of Stichtenoth, Proposition 3.7.3.

Main results

• TauCeti.isSplittingField_X_pow_sub_C_of_adjoin_eq_top: L = K(s) is a splitting field of Xⁿ - b.
• TauCeti.isGalois_of_pow_eq_of_adjoin_eq_top: L/K is Galois.
• TauCeti.exists_forall_mem_zpowers_apply_eq: [L : K] divides n, and some g generating Gal(L/K) satisfies g s = ζ ^ (n / [L : K]) • s.
• TauCeti.isCyclic_of_pow_eq_of_adjoin_eq_top: Gal(L/K) is cyclic.
• TauCeti.exists_pow_finrank_eq_algebraMap: s ^ [L : K] is some c ∈ K with c ^ (n / [L : K]) = b.
• TauCeti.finrank_eq_of_pow_eq_of_adjoin_eq_top: [L : K] = n when b is not a p-th power for any prime p ∣ n.
• TauCeti.X_pow_sub_C_irreducible_of_isPrimitiveRoot: Xⁿ - b is then irreducible, and TauCeti.X_pow_sub_C_irreducible_iff_forall_prime_of_isPrimitiveRoot, TauCeti.X_pow_sub_C_irreducible_iff_of_isPrimitiveRoot are the resulting criteria.

References

• S. Lang, Algebra, Graduate Texts in Mathematics 211, Springer (2002), Chapter VI, §6 and §9, Theorem 9.1.
• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Proposition 3.7.3.

theorem TauCeti.neZero_of_forall_prime_pow_ne {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {n : ℕ} {b : K} {s : L} (hb : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (c : K), c ^ p ≠ b) (hs : s ^ n = (algebraMap K L) b) : NeZero n

If sⁿ = b and b is not a p-th power in K for any prime p dividing n, then n ≠ 0: for n = 0 the radicand b = s ^ 0 = 1 would be a square.

theorem TauCeti.isSplittingField_X_pow_sub_C_of_adjoin_eq_top {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {n : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ n) {b : K} {s : L} [NeZero n] (hs : s ^ n = (algebraMap K L) b) (hgen : K⟮s⟯ = ⊤) : Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C b)

A root of Xⁿ - b generating L makes L a splitting field of Xⁿ - b, when K contains a primitive n-th root of unity: the other roots are ζ ^ i • s. Mathlib's isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top is the case n = [L : K].

theorem TauCeti.isGalois_of_pow_eq_of_adjoin_eq_top {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {n : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ n) {b : K} {s : L} [NeZero n] (hs : s ^ n = (algebraMap K L) b) (hgen : K⟮s⟯ = ⊤) : IsGalois K L

A radical extension K(ⁿ√b) is Galois when K contains a primitive n-th root of unity: it is the splitting field of the binomial Xⁿ - b, which is separable for b ≠ 0; for b = 0 the extension is trivial.

theorem TauCeti.exists_forall_mem_zpowers_apply_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {n : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ n) {b : K} {s : L} [NeZero n] (hs : s ^ n = (algebraMap K L) b) (hgen : K⟮s⟯ = ⊤) : ∃ (g : Gal(L/K)), (∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) ∧ Module.finrank K L ∣ n ∧ g s = (algebraMap K L) (ζ ^ (n / Module.finrank K L)) * s

The canonical generator of a radical extension. Let L = K(s) with sⁿ = b, and let ζ ∈ K be a primitive n-th root of unity. Then [L : K] divides n, and Gal(L/K) is generated by an automorphism g with g s = ζ ^ (n / [L : K]) · s. (For b = 0 the extension is trivial and g = 1.)

theorem TauCeti.isCyclic_of_pow_eq_of_adjoin_eq_top {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {n : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ n) {b : K} {s : L} [NeZero n] (hs : s ^ n = (algebraMap K L) b) (hgen : K⟮s⟯ = ⊤) : IsCyclic Gal(L/K)

A radical extension K(ⁿ√b) is cyclic when K contains a primitive n-th root of unity, whether or not Xⁿ - b is irreducible.

theorem TauCeti.exists_pow_finrank_eq_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {n : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ n) {b : K} {s : L} [NeZero n] (hs : s ^ n = (algebraMap K L) b) (hgen : K⟮s⟯ = ⊤) : ∃ (c : K), s ^ Module.finrank K L = (algebraMap K L) c ∧ c ^ (n / Module.finrank K L) = b

The [L : K]-th power of a Kummer generator lies in K. Let L = K(s) with sⁿ = b, where K contains a primitive n-th root of unity. Then s ^ [L : K] is some c ∈ K with c ^ (n / [L : K]) = b, an (n / [L : K])-th root of b in K.

theorem TauCeti.finrank_eq_of_pow_eq_of_adjoin_eq_top {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {n : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ n) {b : K} {s : L} (hb : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (c : K), c ^ p ≠ b) (hs : s ^ n = (algebraMap K L) b) (hgen : K⟮s⟯ = ⊤) : Module.finrank K L = n

A nondegenerate radical extension has full degree. Let L = K(s) with sⁿ = b, where K contains a primitive n-th root of unity. If b is not a p-th power in K for any prime p dividing n, then [L : K] = n.

theorem TauCeti.X_pow_sub_C_irreducible_of_isPrimitiveRoot {K : Type u_1} [Field K] {n : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ n) {b : K} [NeZero n] (hb : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (c : K), c ^ p ≠ b) : Irreducible (Polynomial.X ^ n - Polynomial.C b)

Irreducibility of Xⁿ - b with roots of unity: if K contains a primitive n-th root of unity and b is not a p-th power in K for any prime p dividing n, then Xⁿ - b is irreducible over K. Unlike Mathlib's irreducible_X_pow_sub_C_of_odd, n may be even.

theorem TauCeti.X_pow_sub_C_irreducible_iff_forall_prime_of_isPrimitiveRoot {K : Type u_1} [Field K] {n : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ n) {b : K} [NeZero n] : Irreducible (Polynomial.X ^ n - Polynomial.C b) ↔ ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (c : K), c ^ p ≠ b

When K contains a primitive n-th root of unity, Xⁿ - b is irreducible exactly when b is not a p-th power in K for any prime p dividing n.

theorem TauCeti.X_pow_sub_C_irreducible_iff_of_isPrimitiveRoot {K : Type u_1} [Field K] {n : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ n) {b : K} [NeZero n] : Irreducible (Polynomial.X ^ n - Polynomial.C b) ↔ ∀ (d : ℕ), d ∣ n → d ≠ 1 → ∀ (c : K), c ^ d ≠ b

When K contains a primitive n-th root of unity, Xⁿ - b is irreducible exactly when b is not a d-th power in K for any divisor d ≠ 1 of n.