English
An algebraic extension is purely inseparable iff all its finite-dimensional subextensions are purely inseparable.
Русский
Алгебраическое расширение чисто бесприводно тогда и только тогда, когда все его конечнодимensional подрасширения являются чисто бесприводными.
LaTeX
$$$\text{IsPurelyInseparable } F E \iff \forall L : \text{IntermediateField } F E, \, \text{FiniteDimensional } F L \to \text{IsPurelyInseparable } F L$$$
Lean4
/-- An algebraic extension is purely inseparable if and only if all of its finite-dimensional
subextensions are purely inseparable. -/
theorem isPurelyInseparable_iff_fd_isPurelyInseparable [Algebra.IsAlgebraic F E] :
IsPurelyInseparable F E ↔ ∀ L : IntermediateField F E, FiniteDimensional F L → IsPurelyInseparable F L :=
by
refine ⟨fun _ _ _ ↦ IsPurelyInseparable.tower_bot F _ E, fun h ↦ isPurelyInseparable_iff.2 fun x ↦ ?_⟩
have hx : IsIntegral F x := Algebra.IsIntegral.isIntegral x
refine ⟨hx, fun _ ↦ ?_⟩
obtain ⟨y, h⟩ :=
(h _ (adjoin.finiteDimensional hx)).inseparable' _ <|
show Separable (minpoly F (AdjoinSimple.gen F x)) by rwa [minpoly_eq]
exact ⟨y, congr_arg (algebraMap _ E) h⟩
