theorem
IsPurelyInseparable.of_surjective
{F : Type u_1}
{E : Type u_2}
[CommRing F]
[CommRing E]
[Algebra F E]
(h : Function.Surjective ⇑(algebraMap F E))
:
theorem
exists_algebra_isPurelyInseparable_of_isSepClosure_of_isAlgClosure
(k : Type u_1)
[Field k]
(K : Type u_2)
[Field K]
[Algebra k K]
[IsSepClosure k K]
(L : Type u_3)
[Field L]
[Algebra k L]
[IsAlgClosure k L]
:
∃ (x : Algebra K L) (_ : IsScalarTower k K L), IsPurelyInseparable K L
If k is a field, K is a separable closure of k and L is an algebraic closure of k,
then there exists an embedding of K into L and L is a purely inseparable extension of K.