nonempty_algEquiv_of_aeval_eq_zero_eq

English

If the sets of polynomials with roots in E and K are equal, there exists a K-algebra isomorphism between E and K.

Русский

Если множества полиномов, имеющих корни в E и K, совпадают, существует K-алгебрический эквивалент между E и K.

LaTeX

$$$\\{p:\\,F[X]\\mid \\exists x\\in E, aeval x p = 0\\} = \\{p:\\,F[X]\\mid \\exists y\\in K, aeval y p = 0\\} \\Rightarrow \\exists \\sigma: E \\simeq_F K$$$

Lean4

theorem nonempty_algEquiv_of_aeval_eq_zero_eq [Algebra.IsAlgebraic F K]
    (h : {p : F[X] | ∃ x : E, aeval x p = 0} = {p | ∃ y : K, aeval y p = 0}) : Nonempty (E ≃ₐ[F] K) :=
  have ⟨σ⟩ := nonempty_algHom_of_aeval_eq_zero_subset h.le
  have ⟨τ⟩ := nonempty_algHom_of_aeval_eq_zero_subset h.ge
  ⟨.ofBijective _ (Algebra.IsAlgebraic.algHom_bijective₂ σ τ).1⟩

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