English
There is a canonical equivalence between F-algebra homs from K to the normal closure and those to L, illustrating how normal closure encodes all K-embeddings into L.
Русский
Существует каноническое эквивалентное соответствие между F-алгебраическими гомоморфизмами из K в нормальное замыкание и в L, демонстрирующее, как нормальное замыкание кодирует все вложения K в L.
LaTeX
$$$\text{equiv}: (K\to_F\text{normalClosure}(F,K,L)) \simeq (K\to_F L)$$$
Lean4
/-- Normal closures of `K/F` are unique up to F-algebra isomorphisms. -/
noncomputable def equiv {L'} [Field L'] [Algebra F L'] [h : IsNormalClosure F K L] [h' : IsNormalClosure F K L'] :
L ≃ₐ[F] L' :=
have := h.normal
AlgEquiv.ofBijective _ <|
And.left <|
Normal.toIsAlgebraic.algHom_bijective₂ (IsNormalClosure.lift fun _ : K ↦ h'.splits _)
(IsNormalClosure.lift fun _ : K ↦ h.splits _)
