English
The separable degree of the minimal polynomial of x is 1 if and only if there exists n such that the mapped minimal polynomial equals (X − C x)^{q^n}.
Русский
Степень сепарабельности минимального многочлена x равна единице тогда и только тогда существует n such that отображённый минимальный многочлен равняется (X − C x)^{q^n}.
LaTeX
$$$ (\minpoly F x).natSepDegree = 1 \iff \exists n : \mathbb{N}, (\minpoly F x).map (algebraMap F E) = (X - C x)^{q^{n}} $$$
Lean4
/-- The minimal polynomial of an element `x` of `E / F` of exponential characteristic `q` has
separable degree one if and only if the minimal polynomial is of the form
`(X - x) ^ (q ^ n)` for some `n : ℕ`. -/
theorem natSepDegree_eq_one_iff_eq_X_sub_C_pow :
(minpoly F x).natSepDegree = 1 ↔ ∃ n : ℕ, (minpoly F x).map (algebraMap F E) = (X - C x) ^ q ^ n :=
by
haveI := expChar_of_injective_algebraMap (algebraMap F E).injective q
haveI := expChar_of_injective_ringHom (C_injective (R := E)) q
refine ⟨fun h ↦ ?_, fun ⟨n, h⟩ ↦ (natSepDegree_eq_one_iff_pow_mem q).2 ?_⟩
· obtain ⟨n, y, h⟩ := (natSepDegree_eq_one_iff_eq_X_pow_sub_C q).1 h
have hx := congr_arg (Polynomial.aeval x) h.symm
rw [minpoly.aeval, map_sub, map_pow, aeval_X, aeval_C, sub_eq_zero, eq_comm] at hx
use n
rw [h, Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, hx, map_pow, ←
sub_pow_expChar_pow_of_commute _ _ (commute_X _)]
apply_fun constantCoeff at h
simp_rw [map_pow, map_sub, constantCoeff_apply, coeff_map, coeff_X_zero, coeff_C_zero] at h
rw [zero_sub, neg_pow, neg_one_pow_expChar_pow] at h
exact ⟨n, -(minpoly F x).coeff 0, by rw [map_neg, h, neg_mul, one_mul, neg_neg]⟩
