English
If D is a purely inseparable extension of k in characteristic p, then for every a ∈ D \ k there exists n > 0 such that a^(p^n) ∈ k.
Русский
Если D есть чисто инsepрабельное расширение над k в характере p, то для каждого a ∈ D \ k существует n > 0 такое, что a^(p^n) ∈ k.
LaTeX
$$$\\exists n, 1 \\le n \\text{ and } a^{p^n} \\in k$$$
Lean4
/-- If `D` is a purely inseparable extension of `k` with characteristic `p`,
then for every element `a` of `D`, there exists a natural number `n`
such that `a ^ (p ^ n)` is contained in `k`. -/
theorem exists_pow_mem_center_of_inseparable (p : ℕ) [hchar : ExpChar D p] (a : D)
(hinsep : ∀ x : D, IsSeparable k x → x ∈ k) : ∃ n, a ^ (p ^ n) ∈ k :=
by
have := (@isPurelyInseparable_iff_pow_mem k D _ _ _ _ p (ExpChar.expChar_center_iff.2 hchar)).1
have pure : IsPurelyInseparable k D :=
⟨Algebra.IsAlgebraic.isIntegral, fun x hx ↦
by
rw [RingHom.mem_range, Subtype.exists]
exact ⟨x, ⟨hinsep x hx, rfl⟩⟩⟩
obtain ⟨n, ⟨m, hm⟩⟩ := this pure a
have := Subalgebra.range_subset (R := k) ⟨(k).toSubsemiring, fun r ↦ r.2⟩
exact ⟨n, Set.mem_of_subset_of_mem this <| Set.mem_range.2 ⟨m, hm⟩⟩
