Capelli's theorem: irreducibility of Xⁿ - a over an arbitrary field

Let K be a field of any characteristic, n ≠ 0 and a ∈ K. Capelli's theorem says that Xⁿ - a is irreducible over K if and only if a is not a p-th power in K for any prime p ∣ n, and a ∉ -4K⁴ when 4 ∣ n. Mathlib proves the odd case (X_pow_sub_C_irreducible_iff_forall_prime_of_odd); the extra condition for 4 ∣ n is needed because of Sophie Germain's identity X⁴ + 4b⁴ = (X² - 2bX + 2b²)(X² + 2bX + 2b²), so for instance X⁴ + 4 is reducible over ℚ although -4 is not a square there.

Main results

• TauCeti.X_pow_two_pow_sub_C_irreducible: X^(2ᵏ) - a is irreducible when a is not a square and, for k ≥ 2, a ∉ -4K⁴.
• TauCeti.neg_four_mul_pow_four_ne_of_irreducible_X_pow_sub_C: if Xⁿ - a is irreducible and 4 ∣ n, then a ∉ -4K⁴.
• TauCeti.X_pow_sub_C_irreducible_of_forall_prime: the sufficiency half of Capelli's theorem.
• TauCeti.X_pow_sub_C_irreducible_iff_forall_prime: Capelli's theorem.

Implementation notes

The heart of the proof is the two-power case n = 2ᵏ. Let β be a root of the irreducible X² - a and L = K(β). Writing an element of L as x + yβ, a fourth root γ of a in L satisfies γ² = ±β, which forces x² + ay² = 0 and 2xy = ±1, hence a = -4x⁴. So if a ∉ -4K⁴, then β is neither a square nor in -4L⁴, and induction over L applies. In characteristic 2 the equation 2xy = ±1 has no solution, so no case split is needed. For a general n = 2ᵏm with m odd one adjoins a root α of Xᵐ - a and transports the hypotheses to α with the norm, whose value at α is a because m is odd; this reduction follows the proof of Mathlib's irreducible_X_pow_sub_C_of_odd.

References

• S. Lang, Algebra, Chapter VI, Theorem 9.1.
• F. Szechtman, On the degree of repeated radical extensions, Section 1, criterion (C).
• B. Koley and A. S. Reddy, Irreducibility of xⁿ − a, Lemma 10 and Theorem 1.

theorem TauCeti.X_pow_two_pow_sub_C_irreducible {K : Type u_1} [Field K] (k : ℕ) {a : K} (ha : ∀ (b : K), b ^ 2 ≠ a) (ha' : 2 ≤ k → ∀ (b : K), -4 * b ^ 4 ≠ a) : Irreducible (Polynomial.X ^ 2 ^ k - Polynomial.C a)

The two-power case of Capelli's theorem. Over any field K, if a is not a square in K and, when k ≥ 2, a is not of the form -4b⁴, then X^(2ᵏ) - a is irreducible. The second condition cannot be dropped: X⁴ + 4 is reducible over ℚ.

theorem TauCeti.neg_four_mul_pow_four_ne_of_irreducible_X_pow_sub_C {K : Type u_1} [Field K] {n : ℕ} {a : K} (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (hn : 4 ∣ n) (b : K) : -4 * b ^ 4 ≠ a

If Xⁿ - a is irreducible and 4 ∣ n, then a is not of the form -4b⁴: otherwise Sophie Germain's identity factors Xⁿ - a into two polynomials of degree n / 2. This is the companion of Mathlib's pow_ne_of_irreducible_X_pow_sub_C.

theorem TauCeti.X_pow_sub_C_irreducible_of_forall_prime {K : Type u_1} [Field K] {n : ℕ} (hn : n ≠ 0) {a : K} (ha : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) (ha' : 4 ∣ n → ∀ (b : K), -4 * b ^ 4 ≠ a) : Irreducible (Polynomial.X ^ n - Polynomial.C a)

Capelli's theorem, sufficiency: over any field K, if n ≠ 0, a is not a p-th power for any prime p ∣ n, and a is not of the form -4b⁴ when 4 ∣ n, then Xⁿ - a is irreducible.

theorem TauCeti.X_pow_sub_C_irreducible_iff_forall_prime {K : Type u_1} [Field K] {n : ℕ} (hn : n ≠ 0) {a : K} : Irreducible (Polynomial.X ^ n - Polynomial.C a) ↔ (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) ∧ (4 ∣ n → ∀ (b : K), -4 * b ^ 4 ≠ a)

Capelli's theorem. Over any field K and for n ≠ 0, the binomial Xⁿ - a is irreducible if and only if a is not a p-th power for any prime p ∣ n and, when 4 ∣ n, a is not of the form -4b⁴. For odd n this is Mathlib's X_pow_sub_C_irreducible_iff_forall_prime_of_odd.