English
If K over F is purely inseparable and E is an intermediate field with F ≤ E ≤ K, then E is purely inseparable over F.
Русский
Если K/F чисто безразделимо, и E является промежуточным полем между F и K, то E/ F тоже чисто безразделимо.
LaTeX
$$$ [Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F K] \Rightarrow IsPurelyInseparable F E $$$
Lean4
/-- If `K / E / F` is a field extension tower such that `K / F` is purely inseparable,
then `E / F` is also purely inseparable. -/
theorem tower_bot [Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F K] : IsPurelyInseparable F E :=
by
refine ⟨⟨fun x ↦ (isIntegral' F (algebraMap E K x)).tower_bot_of_field⟩, fun x h ↦ ?_⟩
rw [IsSeparable, ← minpoly.algebraMap_eq (algebraMap E K).injective] at h
obtain ⟨y, h⟩ := inseparable F _ h
exact ⟨y, (algebraMap E K).injective (h.symm ▸ (IsScalarTower.algebraMap_apply F E K y).symm)⟩
