nonempty_algHom_of_aeval_eq_zero_subset

English

If the set of polynomials with a root in E is contained in the set with a root in K, then there exists a K-algebra homomorphism E → K.

Русский

Если множество полиномов с корнем в E содержится во множестве полиномов с корнем в K, то существует гомоморф по K из E в K.

LaTeX

$$$\\text{set of } p: F[X] \\text{ with } \\exists x\\in E, aeval(x)p=0 \\subseteq \\text{set of } p: F[X] \\text{ with } \\exists y\\in K, aeval(y)p=0 \\Rightarrow \\exists \\varphi: E \\to_F K$$$

Lean4

theorem nonempty_algHom_of_aeval_eq_zero_subset
    (h : {p : F[X] | ∃ x : E, aeval x p = 0} ⊆ {p | ∃ y : K, aeval y p = 0}) : Nonempty (E →ₐ[F] K) :=
  nonempty_algHom_of_minpoly_eq fun x ↦
    have ⟨y, hy⟩ := h ⟨_, minpoly.aeval F x⟩
    ⟨y, (minpoly.eq_iff_aeval_minpoly_eq_zero <| (alg.isIntegral).1 x).mpr hy⟩

Похожие утверждения