English
If L is algebraically closed and the restricted-algebra-map composition map is injective, then E/F is purely inseparable.
Русский
Если L алгебраически замкнуто и композиция (f ∘ algebraMap) инъективна, то E/F чисто бесприводно.
LaTeX
$$$\big(\exists L\,[\IsAlgClosed L]\,\wedge\, \text{Nonempty }(E \to^+_* L) \wedge \text{Injective}(f \mapsto f \circ (\mathrm{algebraMap}_F E))\big) \Rightarrow \text{IsPurelyInseparable } F E$$$
Lean4
/-- If `E / F` is algebraic, then `E` is purely inseparable over the
separable closure of `F` in `E`. -/
@[stacks 030K "$E/E_{sep}$ is purely inseparable."]
instance isPurelyInseparable [Algebra.IsAlgebraic F E] : IsPurelyInseparable (separableClosure F E) E :=
isPurelyInseparable_iff.2 fun x ↦ by
set L := separableClosure F E
refine ⟨(IsAlgebraic.tower_top L (Algebra.IsAlgebraic.isAlgebraic (R := F) x)).isIntegral, fun h ↦ ?_⟩
haveI := (isSeparable_adjoin_simple_iff_isSeparable L E).2 h
haveI : Algebra.IsSeparable F (restrictScalars F L⟮x⟯) := Algebra.IsSeparable.trans F L L⟮x⟯
have hx : x ∈ restrictScalars F L⟮x⟯ := mem_adjoin_simple_self _ x
exact ⟨⟨x, mem_separableClosure_iff.2 <| isSeparable_of_mem_isSeparable F E hx⟩, rfl⟩
