English
Normal closures of K/F are unique up to F-algebra isomorphisms: if L and L' are normal closures, there is an F-algebra equivalence between L and L'.
Русский
Нормальные замыкания K/F уникальны по отношению к F-алгебраическому изоморфизму: между любыми двумя нормальными замыканиями существует F-алгебраическое эквиналие.
LaTeX
$$$IsNormalClosure\ F\ K\ L \Rightarrow \exists \text{AlgEquiv }F\ L\ L'\;\text{(equivalence of normal closures)}$$$
Lean4
/-- A normal closure of `K/F` embeds into any `L/F`
where the minimal polynomials of `K/F` splits. -/
noncomputable def lift [h : IsNormalClosure F K L] {L'} [Field L'] [Algebra F L']
(splits : ∀ x : K, (minpoly F x).Splits (algebraMap F L')) : L →ₐ[F] L' :=
by
have := h.adjoin_rootSet; rw [← gc.l_iSup] at this
refine
Nonempty.some <|
nonempty_algHom_of_adjoin_splits (fun x hx ↦ ⟨isAlgebraic_iff_isIntegral.mp ((h.normal).isAlgebraic x), ?_⟩) this
obtain ⟨y, hx⟩ := Set.mem_iUnion.mp hx
by_cases iy : IsIntegral F y
· exact splits_of_splits_of_dvd _ (minpoly.ne_zero iy) (splits y) (minpoly.dvd F x (mem_rootSet.mp hx).2)
· simp [minpoly.eq_zero iy] at hx
