English
For prime p, X^p − C a irreducible if no p-th power equals a; the result is classic.
Русский
Для простого p, ирр X^p − C a иррeдно тогда, когда нет p-й степени, равной a; это классический факт.
LaTeX
$$$\text{X^p - C a irreducible if no } b^p = a$$$
Lean4
/-- Let `p` be a prime number. Let `K` be a field.
Let `t ∈ K` be an element which does not have a `p`th root in `K`.
Then the polynomial `x ^ p - t` is irreducible over `K`. -/
@[stacks 09HF "We proved the result without the condition that `K` is char p in 09HF."]
theorem X_pow_sub_C_irreducible_of_prime {p : ℕ} (hp : p.Prime) {a : K} (ha : ∀ b : K, b ^ p ≠ a) :
Irreducible (X ^ p - C a) := by
-- First of all, We may find an irreducible factor `g` of `X ^ p - C a`.
have : ¬IsUnit (X ^ p - C a) :=
by
rw [Polynomial.isUnit_iff_degree_eq_zero, degree_X_pow_sub_C hp.pos, Nat.cast_eq_zero]
exact hp.ne_zero
have ⟨g, hg, hg'⟩ :=
WfDvdMonoid.exists_irreducible_factor this
(X_pow_sub_C_ne_zero hp.pos a)
-- It suffices to show that `deg g = p`.
suffices natDegree g = p from
(associated_of_dvd_of_natDegree_le hg' (X_pow_sub_C_ne_zero hp.pos a)
(this.trans natDegree_X_pow_sub_C.symm).ge).irreducible
hg
by_contra h
have key : (Algebra.norm K (AdjoinRoot.root g)) ^ p = a ^ g.natDegree :=
by
have := eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hg' (AdjoinRoot.eval₂_root g)
rw [eval₂_sub, eval₂_pow, eval₂_C, eval₂_X, sub_eq_zero] at this
rw [← map_pow, this, ← AdjoinRoot.algebraMap_eq, Algebra.norm_algebraMap, (powerBasis hg.ne_zero).finrank,
powerBasis_dim hg.ne_zero]
-- Since `a ^ (deg g)` is a `p`-power, and `p` is coprime to `deg g`, we conclude that `a` is
-- also a `p`-power, contradicting the hypothesis
have : p.Coprime (natDegree g) :=
hp.coprime_iff_not_dvd.mpr
(fun e ↦
h
(((natDegree_le_of_dvd hg' (X_pow_sub_C_ne_zero hp.pos a)).trans_eq natDegree_X_pow_sub_C).antisymm
(Nat.le_of_dvd (natDegree_pos_iff_degree_pos.mpr <| Polynomial.degree_pos_of_irreducible hg) e)))
exact ha _ ((pow_mem_range_pow_of_coprime this.symm a).mp ⟨_, key⟩).choose_spec
