English
For a division ring D algebraic over its center k and not all of D equal to k, there exists x ∈ D \ k that is separable over k.
Русский
Для деления кольца D, алгебраически над своим центром k и D ≠ k, существует x ∈ D \ k сепарабельный над k.
LaTeX
$$$\\exists x\\in D\\setminus k:\\ IsSeparable\\ k\\ x$$$
Lean4
/-- If `D` is a purely inseparable extension of `k` of characteristic `p`,
then for every element `a` of `D \ k`, there exists a natural number `m`
greater than 0 such that `(a * x - x * a) ^ n = 0` (as linear maps) for
every `n` greater than `(p ^ m)`. -/
theorem exist_pow_eq_zero_of_le (p : ℕ) [hchar : ExpChar D p] {a : D} (ha : a ∉ k)
(hinsep : ∀ x : D, IsSeparable k x → x ∈ k) : ∃ m, 1 ≤ m ∧ ∀ n, p ^ m ≤ n → (ad k D a)^[n] = 0 :=
by
obtain ⟨m, hm⟩ := exists_pow_mem_center_of_inseparable' p ha hinsep
refine ⟨m, ⟨hm.1, fun n hn ↦ ?_⟩⟩
have inter : (ad k D a)^[p ^ m] = 0 := by
ext x
rw [ad_eq_lmul_left_sub_lmul_right, ← Module.End.pow_apply, Pi.sub_apply,
sub_pow_expChar_pow_of_commute p m (commute_mulLeft_right a a), sub_apply, pow_mulLeft, mulLeft_apply,
pow_mulRight, mulRight_apply, Pi.zero_apply, Subring.mem_center_iff.1 hm.2 x]
exact sub_eq_zero_of_eq rfl
rw [(Nat.sub_eq_iff_eq_add hn).1 rfl, Function.iterate_add, inter, Pi.comp_zero, iterate_map_zero,
Function.const_zero]
