English
A field extension E/F with exponential characteristic q is purely inseparable iff every element x ∈ E has some n with x^{q^n} ∈ F.
Русский
Расширение полей E/F с экспоненциальной характеристикой q чисто безразделимо тогда и только тогда, когда для каждого x ∈ E существует n, такое что x^{q^n} ∈ F.
LaTeX
$$$ IsPurelyInseparable F E \iff \forall x\in E, \exists n\in\mathbb{N}, x^{q^n} \in (\mathrm{algebraMap} F E).\mathrm{range} $$$
Lean4
/-- A field extension `E / F` of exponential characteristic `q` is purely inseparable
if and only if for every element `x` of `E`, there exists a natural number `n` such that
`x ^ (q ^ n)` is contained in `F`. -/
@[stacks 09HE]
theorem isPurelyInseparable_iff_pow_mem :
IsPurelyInseparable F E ↔ ∀ x : E, ∃ n : ℕ, x ^ q ^ n ∈ (algebraMap F E).range :=
by
rw [isPurelyInseparable_iff]
refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩
· obtain ⟨g, h1, n, h2⟩ := (minpoly.irreducible (h x).1).hasSeparableContraction q
exact
⟨n,
(h _).2 <|
h1.of_dvd <| minpoly.dvd F _ <| by simpa only [expand_aeval, minpoly.aeval] using congr_arg (aeval x) h2⟩
have hdeg := (minpoly.natSepDegree_eq_one_iff_pow_mem q).2 (h x)
have halg : IsIntegral F x :=
by_contra fun h' ↦ by simp only [minpoly.eq_zero h', natSepDegree_zero, zero_ne_one] at hdeg
refine ⟨halg, fun hsep ↦ ?_⟩
rwa [hsep.natSepDegree_eq_natDegree, minpoly.natDegree_eq_one_iff] at hdeg
