Algebraic extensions are determined by their sets of minimal polynomials up to isomorphism #
Main results #
Field.nonempty_algHom_of_exist_roots says if E/F and K/F are field extensions
with E/F algebraic, and if the minimal polynomial of every element of E over F has a root
in K, then there exists an F-embedding of E into K. If E/F and K/F have the same
set of minimal polynomials, then E and K are isomorphic as F-algebras. As a corollary:
IsAlgClosure.of_exist_roots: if E/F is algebraic and every monic irreducible polynomial
in F[X] has a root in E, then E is an algebraic closure of F.
Reference #
[Isa80] Roots of Polynomials in Algebraic Extensions of Fields, The American Mathematical Monthly
theorem
Field.nonempty_algHom_of_aeval_eq_zero_subset
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[Field F]
[Field E]
[Field K]
[Algebra F E]
[Algebra F K]
[alg : Algebra.IsAlgebraic F E]
(h :
{p : Polynomial F | ∃ (x : E), (Polynomial.aeval x) p = 0} ⊆ {p : Polynomial F | ∃ (y : K), (Polynomial.aeval y) p = 0})
:
theorem
Field.nonempty_algEquiv_of_aeval_eq_zero_eq
{F : Type u_1}
{E : Type u_2}
{K : Type u_3}
[Field F]
[Field E]
[Field K]
[Algebra F E]
[Algebra F K]
[alg : Algebra.IsAlgebraic F E]
[Algebra.IsAlgebraic F K]
(h :
{p : Polynomial F | ∃ (x : E), (Polynomial.aeval x) p = 0} = {p : Polynomial F | ∃ (y : K), (Polynomial.aeval y) p = 0})
:
theorem
IsAlgClosure.of_exist_roots
{F : Type u_1}
{E : Type u_2}
[Field F]
[Field E]
[Algebra F E]
[alg : Algebra.IsAlgebraic F E]
(h : ∀ (p : Polynomial F), p.Monic → Irreducible p → ∃ (x : E), (Polynomial.aeval x) p = 0)
:
IsAlgClosure F E