English
Let L be an intermediate field of E over F, and f: L →_F K an F-algebra homomorphism. If a generating set S ⊆ E consists of elements that are integral over L and whose minimal polynomials over L split in K via f, then f extends to an F-algebra homomorphism φ: E →_F K with φ restricted to L equal to f.
Русский
Пусть L ⊆ E и f: L →_F K является F-симметричным гомоморфизмом. Если существует множество S ⊆ E, состоящее из элементов, каждый из которых целиком интегрирован над L и чьи минимальныеpolynomial над L раскладываются в K через f, то f можно продолжить до гомоморфизма φ: E →_F K такая что φ ограничен в L совпадает с f.
LaTeX
$$$\forall f : L \to_F K\,\big(\,\forall s \in S,\ IsIntegral_L(s) \wedge (minpoly_L(s)).Splits(f) \big) \Rightarrow \exists \varphi : E \to_F K, \ \varphi|_L = f \,$$$
Lean4
theorem exists_algHom_of_splits' (hK : ∀ s : E, IsIntegral L s ∧ (minpoly L s).Splits f.toRingHom) :
∃ φ : E →ₐ[F] K, φ.restrictDomain L = f :=
exists_algHom_of_adjoin_splits' f (fun x _ ↦ hK x) (adjoin_univ L E)
