English
For algebraic E/F, the separable closure is the smallest subfield containing F over which E is purely inseparable.
Русский
Для алгебраического E/F сепарабельное замыкание есть минимальное подполе, над которым E чисто бесприводно.
LaTeX
$$$\mathrm{separableClosure}(F,E) \le L \ \text{iff} \text{IsPurelyInseparable } L E$$$
Lean4
/-- If `E / F` is algebraic, then an intermediate field of `E / F` contains the
separable closure of `F` in `E` if and only if `E` is purely inseparable over it. -/
theorem separableClosure_le_iff [Algebra.IsAlgebraic F E] (L : IntermediateField F E) :
separableClosure F E ≤ L ↔ IsPurelyInseparable L E :=
by
refine ⟨fun h ↦ ?_, fun _ ↦ separableClosure_le F E L⟩
letI := (inclusion h).toAlgebra
letI : SMul (separableClosure F E) L := Algebra.toSMul
haveI : IsScalarTower (separableClosure F E) L E := IsScalarTower.of_algebraMap_eq (congrFun rfl)
exact IsPurelyInseparable.tower_top (separableClosure F E) L E
