English
If K over F is purely inseparable and E is an intermediate field with F ≤ E ≤ K, then K over E is purely inseparable.
Русский
Если K/F чисто безразделимо и E находится между F и K, то K/E также чисто безразделимо.
LaTeX
$$$ [Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F K] \Rightarrow IsPurelyInseparable E K $$$
Lean4
/-- If `K / E / F` is a field extension tower such that `K / F` is purely inseparable,
then `K / E` is also purely inseparable. -/
theorem tower_top [Algebra E K] [IsScalarTower F E K] [h : IsPurelyInseparable F K] : IsPurelyInseparable E K :=
by
obtain ⟨q, _⟩ := ExpChar.exists F
haveI := expChar_of_injective_algebraMap (algebraMap F E).injective q
rw [isPurelyInseparable_iff_pow_mem _ q] at h ⊢
intro x
obtain ⟨n, y, h⟩ := h x
exact ⟨n, (algebraMap F E) y, h.symm ▸ (IsScalarTower.algebraMap_apply F E K y).symm⟩
