English
Let F and E be as above. The separable degree of minpoly F x is 1 if and only if x^{q^n} lies in the image of F under the embedding E, for some n.
Русский
Пусть F и E соответствуют условиям. Разделительная степень minpoly F x равна единице тогда и только тогда, когда для некоторого n число x^{q^n} лежит в образе F в E через вложение.
LaTeX
$$$ (\minpoly F x).natSepDegree = 1 \iff \exists n : \mathbb{N}, x^{q^{n}} \in (algebraMap F E).range $$$
Lean4
/-- The minimal polynomial of an element `x` of `E / F` of exponential characteristic `q` has
separable degree one if and only if `x ^ (q ^ n) ∈ F` for some `n : ℕ`. -/
theorem natSepDegree_eq_one_iff_pow_mem :
(minpoly F x).natSepDegree = 1 ↔ ∃ n : ℕ, x ^ q ^ n ∈ (algebraMap F E).range :=
by
convert_to _ ↔ ∃ (n : ℕ) (y : F), Polynomial.aeval x (X ^ q ^ n - C y) = 0
· simp_rw [RingHom.mem_range, map_sub, map_pow, aeval_C, aeval_X, sub_eq_zero, eq_comm]
refine ⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩
· obtain ⟨n, y, hx⟩ := (minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C q).1 h
exact ⟨n, y, hx ▸ aeval F x⟩
have hnezero := X_pow_sub_C_ne_zero (expChar_pow_pos F q n) y
refine
((natSepDegree_le_of_dvd _ _ (minpoly.dvd F x h) hnezero).trans_eq <|
natSepDegree_X_pow_char_pow_sub_C q n y).antisymm
?_
rw [Nat.one_le_iff_ne_zero, natSepDegree_ne_zero_iff, ← Nat.one_le_iff_ne_zero]
exact minpoly.natDegree_pos <| IsAlgebraic.isIntegral ⟨_, hnezero, h⟩
