English
For a given element x in an extension E/F, the natSepDegree of its minimal polynomial equals the number of distinct embeddings/separable degree of the element and is characterized by expansions X-related representations.
Русский
Для элемента x в расширении E/F natSepDegree минимального многочлена равна числу различимых вложений/разделяемой степени элемента и характеризуется expansions.
LaTeX
$$$ (minpoly\ F x).natSepDegree = 1 \iff \exists n\, \exists y\ (minpoly\ F x = \expand F (q^n) (X - C y)) $$$
Lean4
/-- If a monic polynomial over a field `F` of exponential characteristic `q` has separable degree
one, then it is of the form `(X ^ (q ^ n) - C y) ^ m` for some non-zero natural number `m`,
some natural number `n`, and some element `y` of `F`, such that either `n = 0` or `y` has no
`q`-th root in `F`. -/
theorem eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one (q : ℕ) [ExpChar F q] (hm : f.Monic)
(h : f.natSepDegree = 1) :
∃ (m n : ℕ) (y : F), m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m :=
by
obtain ⟨p, hM, hI, hf⟩ :=
exists_monic_irreducible_factor _ <|
not_isUnit_of_natDegree_pos _ <| Nat.pos_of_ne_zero <| (natSepDegree_ne_zero_iff _).1 (h.symm ▸ Nat.one_ne_zero)
have hD :=
(h ▸ natSepDegree_le_of_dvd p f hf hm.ne_zero).antisymm <|
Nat.pos_of_ne_zero <| (natSepDegree_ne_zero_iff _).2 hI.natDegree_pos.ne'
obtain ⟨n, y, H, hp⟩ := hM.eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible q hI hD
have hF := finiteMultiplicity_of_degree_pos_of_monic (degree_pos_of_irreducible hI) hM hm.ne_zero
classical
have hne := (multiplicity_pos_of_dvd hf).ne'
refine ⟨_, n, y, hne, H, ?_⟩
obtain ⟨c, hf, H⟩ := hF.exists_eq_pow_mul_and_not_dvd
rw [hf, natSepDegree_mul_of_isCoprime _ c <| IsCoprime.pow_left <| (hI.isCoprime_or_dvd c).resolve_right H,
natSepDegree_pow_of_ne_zero _ hne, hD, add_eq_left, natSepDegree_eq_zero_iff] at h
simpa only [eq_one_of_monic_natDegree_zero ((hM.pow _).of_mul_monic_left (hf ▸ hm)) h, mul_one, ← hp] using hf
