English
Let E be normal over F and suppose there are isomorphisms f: F ≃ M and g: E ≃ N with the compatibility (algebraMap M N) ∘ f = g ∘ (algebraMap F E). Then M and N form a normal extension, i.e. Normal M N.
Русский
Пусть E над F нормальное расширение. Существуют изоморфизмы f: F ≃ M и g: E ≃ N, удовлетворяющие совместимости (algebraMap M N) ∘ f = g ∘ (algebraMap F E). Тогда пара M ⊂ N образует нормальное расширение: Normal M N.
LaTeX
$$$\text{Если } E/F \text{ нормально, и существуют кольцевые изоморфизмы } f:F\cong M,\ g:E\cong N\text{ такие, что } (\alpha_{M,N}\circ f)=(g\circ \alpha_{F,E}),\\text{то } Normal(M,N).$$$
Lean4
theorem of_equiv_equiv {M N : Type*} [Field N] [Field M] [Algebra M N] [Algebra.IsAlgebraic F E] [h : Normal F E]
{f : F ≃+* M} {g : E ≃+* N} (hcomp : (algebraMap M N).comp f = (g : E →+* N).comp (algebraMap F E)) : Normal M N :=
by
rw [normal_iff] at h ⊢
intro x
rw [← g.apply_symm_apply x]
refine ⟨(h (g.symm x)).1.map_of_comp_eq _ _ hcomp, ?_⟩
rw [← minpoly.map_eq_of_equiv_equiv hcomp, Polynomial.splits_map_iff, hcomp]
exact Polynomial.splits_comp_of_splits _ _ (h (g.symm x)).2
