Algebraic extensions are determined by their sets of minimal polynomials up to isomorphism #
Main results #
Field.nonempty_algHom_of_exists_root 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_exists_root: 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.
References #
[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_exists_root {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