The normal closure of a simple extension

Inside a normal extension, the normal closure of F⟮x⟯ is generated by the roots of minpoly F x. Thus it is a splitting field of that polynomial. This identifies the field used to study a simple extension with the field used to define its polynomial Galois group. The closure has finite degree, and is Galois when the minimal polynomial is separable.

When F⟮x⟯ is already all of E, this says that E itself is a splitting field of minpoly F x; if moreover E / F is Galois, the Galois group of minpoly F x has order [E : F].

theorem TauCeti.normalClosure_adjoin_simple_eq_adjoin_rootSet {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (x : E) : IntermediateField.normalClosure F (↥F⟮x⟯) E = IntermediateField.adjoin F ((minpoly F x).rootSet E)

The normal closure of a simple extension is generated by all the conjugates of its generator, equivalently by the roots of its minimal polynomial.

theorem TauCeti.isSplittingField_normalClosure_adjoin_simple {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (x : E) : Polynomial.IsSplittingField F (↥(IntermediateField.normalClosure F (↥F⟮x⟯) E)) (minpoly F x)

The normal closure of a simple extension is a splitting field of the generator's minimal polynomial. No separability hypothesis is needed.

theorem TauCeti.finiteDimensional_normalClosure_adjoin_simple {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] {x : E} (hx : IsIntegral F x) : FiniteDimensional F ↥(IntermediateField.normalClosure F (↥F⟮x⟯) E)

The normal closure of a simple algebraic extension has finite degree.

theorem TauCeti.isGalois_normalClosure_adjoin_simple {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (x : E) (hsep : (minpoly F x).Separable) : IsGalois F ↥(IntermediateField.normalClosure F (↥F⟮x⟯) E)

The normal closure of a simple extension is Galois if its minimal polynomial is separable.

theorem TauCeti.isSplittingField_minpoly_of_adjoin_simple_eq_top {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (x : E) (hgen : F⟮x⟯ = ⊤) : Polynomial.IsSplittingField F E (minpoly F x)

A normal simple extension splits the minimal polynomial of its generator and is generated by its roots.

theorem TauCeti.natCard_gal_minpoly_eq_finrank {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [IsGalois F E] (x : E) (hgen : F⟮x⟯ = ⊤) : Nat.card (minpoly F x).Gal = Module.finrank F E

In a Galois simple extension, the minimal polynomial of a generator has Galois-group order equal to the extension degree.