English
There is an embedding of F-algebra homs from K to the normalClosure into F-algebra homs from K to L, reflecting how normalClosure controls all K-embeddings.
Русский
Существуют вложения F-алгебраических гомоморфизмов из K в normalClosure в гомоморфизмы из K в L, отражающие контроль над вложениями K.
LaTeX
$$$\text{AlgHomEmbeddingOfSplits}((F,K,L),h)(K\to_F\text{normalClosure}(F,K,L)) \hookrightarrow (K\to_F L)$$$
Lean4
/-- All `F`-`AlgHom`s from `K` to `L` factor through the normal closure of `K/F` in `L/F`. -/
noncomputable def algHomEquiv : (K →ₐ[F] normalClosure F K L) ≃ (K →ₐ[F] L)
where
toFun := (normalClosure F K L).val.comp
invFun f := f.codRestrict _ fun x ↦ f.fieldRange_le_normalClosure ⟨x, rfl⟩
