nonempty_algHom_of_range_minpoly_subset

English

If the set of polynomials that occur as minpolys of elements of E is contained in the set that occur as minpolys of elements of K, then there exists a K-algebra homomorphism E → K.

Русский

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

LaTeX

$$$\\text{range}(minpoly\\ F)\\restriction_E \\subseteq \\text{range}(minpoly\\ F)\\restriction_K \\Rightarrow \\exists \\varphi: E \\to_F K$$$

Lean4

theorem nonempty_algHom_of_range_minpoly_subset (h : Set.range (@minpoly F E _ _ _) ⊆ Set.range (@minpoly F K _ _ _)) :
    Nonempty (E →ₐ[F] K) :=
  nonempty_algHom_of_minpoly_eq fun x ↦
    have ⟨y, hy⟩ := h ⟨x, rfl⟩;
    ⟨y, hy.symm⟩

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