English
If L is algebraically closed and the map f ↦ f ∘ algebraMap F E is injective, then E/F is purely inseparable.
Русский
Если L алгебраически замкнуто, и отображение f ↦ f ∘ алгебра карта F,E инъективно, то E/F чисто бесприводно.
LaTeX
$$$\forall L\, [\text{Field } L]\ [\text{IsAlgClosed } L]\ [\text{Nonempty }(E \to_{+}^* L)],\; (f \mapsto f \circ (\mathrm{algebraMap}_{F E})) \text{ инъективно} \Rightarrow \text{IsPurelyInseparable } F E$$$
Lean4
/-- If `L` is an algebraically closed field containing `E`, such that the map
`(E →+* L) → (F →+* L)` induced by `algebraMap F E` is injective, then `E / F` is
purely inseparable. As a corollary, epimorphisms in the category of fields must be
purely inseparable extensions. -/
theorem of_injective_comp_algebraMap (L : Type w) [Field L] [IsAlgClosed L] [Nonempty (E →+* L)]
(h : Function.Injective fun f : E →+* L ↦ f.comp (algebraMap F E)) : IsPurelyInseparable F E :=
by
rw [isPurelyInseparable_iff_finSepDegree_eq_one, finSepDegree, Nat.card_eq_one_iff_unique]
letI := (Classical.arbitrary (E →+* L)).toAlgebra
let j : AlgebraicClosure E →ₐ[E] L := IsAlgClosed.lift
exact
⟨⟨fun f g ↦
DFunLike.ext' <|
j.injective.comp_left (congr_arg (⇑) <| @h (j.toRingHom.comp f) (j.toRingHom.comp g) (by ext; simp))⟩,
inferInstance⟩
