English
If x ∈ E and y ∈ K satisfy that y is a root of minpoly_F(x) via aeval map, then there is φ: E →_F K with φ(x) = y extending some existing map.
Русский
Если x ∈ E и y ∈ K удовлетворяют, что y является корнем минимального многочлена x над F через отображение aeval, то существует φ: E →_F K, удовлетворяющий φ(x)=y.
LaTeX
$$$\exists φ : E \to_F K, φ(x) = y$ под условием $\operatorname{aeval}(y, \minpoly_F(x)) = 0$$$
Lean4
theorem exists_algHom_adjoin_of_splits_of_aeval : ∃ φ : adjoin F S →ₐ[F] K, φ ⟨x, hx⟩ = y :=
by
have := isAlgebraic_adjoin (fun s hs ↦ (hK s hs).1)
have ix : IsAlgebraic F _ := Algebra.IsAlgebraic.isAlgebraic (⟨x, hx⟩ : adjoin F S)
rw [isAlgebraic_iff_isIntegral, isIntegral_iff] at ix
obtain ⟨φ, hφ⟩ :=
exists_algHom_adjoin_of_splits hK
((algHomAdjoinIntegralEquiv F ix).symm ⟨y, mem_aroots.mpr ⟨minpoly.ne_zero ix, hy⟩⟩) (adjoin_simple_le_iff.mpr hx)
exact ⟨φ, (DFunLike.congr_fun hφ <| AdjoinSimple.gen F x).trans <| algHomAdjoinIntegralEquiv_symm_apply_gen F ix _⟩
