English
Let hK and hK' state that every element of S is integral over F and its minimal polynomial splits in K via the canonical map F → K. If L is an intermediate field with L ≤ adjoin_F S and f: L →_F K, then there exists an algebra hom φ from adjoin_F S to K such that φ composed with the inclusion of L into adjoin_F S equals f.
Русский
Пусть все s ∈ S целочисленны над F и их минполином над F раскладывается в K через алгебраическое отображение F → K. Пусть L ≤ adjoin_F S и f: L →_F K. Тогда существует алгебр-гомоморфизм φ: adjoin_F S →_F K с φ ∘ включение = f.
LaTeX
$$$\big(\forall s \in S,\ IsIntegral_F(s) \wedge (minpoly_F(s)).Splits( algebraMap F K)\big) \Rightarrow ∃ φ : adjoin F S →_F K, φ \circ inclusion(hL) = f$$$
Lean4
theorem exists_algHom_adjoin_of_splits : ∃ φ : adjoin F S →ₐ[F] K, φ.comp (inclusion hL) = f :=
by
obtain ⟨φ, hfφ, hφ⟩ := zorn_le_nonempty_Ici₀ _ (fun c _ hc _ _ ↦ Lifts.exists_upper_bound c hc) ⟨L, f⟩ le_rfl
refine ⟨φ.emb.comp (inclusion <| adjoin_le_iff.mpr fun s hs ↦ ?_), ?_⟩
· rcases φ.exists_lift_of_splits (hK s hs).1 (hK s hs).2 with ⟨y, h1, h2⟩
exact (hφ h1).1 h2
· ext; apply hfφ.2
