English
Purely inseparableity over a base field is preserved under isomorphisms of algebras. If K is purely inseparable over F and there is an F-algebra isomorphism e: K ≃_F E, then E is purely inseparable over F.
Русский
Чисто безразделимое расширение над основанием F сохраняется при изоморфизма F-алгебр. Если K чисто безразделимо над F и существует F-алгебраический изоморфизм e: K ≃_F E, то E тоже является чисто безразделимым над F.
LaTeX
$$$ \forall F,E,K \, [\text{CommRing } F] [\text{Ring } E] [\text{Algebra } F E] [\text{Ring } K] [\text{Algebra } F K] (e: K \cong_F E),\ IsPurelyInseparable(F,K) \Rightarrow IsPurelyInseparable(F,E). $$$
Lean4
/-- Transfer `IsPurelyInseparable` across an `AlgEquiv`. -/
theorem isPurelyInseparable (e : K ≃ₐ[F] E) [IsPurelyInseparable F K] : IsPurelyInseparable F E :=
by
refine ⟨⟨fun _ ↦ by rw [← isIntegral_algEquiv e.symm]; exact IsPurelyInseparable.isIntegral' F _⟩, fun x h ↦ ?_⟩
rw [IsSeparable, ← minpoly.algEquiv_eq e.symm] at h
simpa only [RingHom.mem_range, algebraMap_eq_apply] using IsPurelyInseparable.inseparable F _ h
