Polynomial Galois groups and normal closures

For an element x in a normal extension E / F, the splitting field of minpoly F x is isomorphic to the normal closure of F⟮x⟯ inside E. Conjugation by that field isomorphism identifies the polynomial Galois group with the automorphism group of the normal closure.

The comparison respects the intrinsic action on roots: a point stabilizer maps to the subgroup fixing the field generated by the corresponding root. For a separable minimal polynomial, this subgroup has index [F(x) : F]. Thus the group together with a point stabilizer recovers the simple extension inside its normal closure.

No ordering of roots is chosen.

noncomputable def TauCeti.splittingFieldEquivNormalClosure {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (x : E) : (minpoly F x).SplittingField ≃ₐ[F] ↥(IntermediateField.normalClosure F (↥F⟮x⟯) E)

The splitting field of the minimal polynomial of x is isomorphic to the normal closure of the simple extension generated by x.

Equations

• TauCeti.splittingFieldEquivNormalClosure x = (Polynomial.IsSplittingField.algEquiv (↥(IntermediateField.normalClosure F (↥F⟮x⟯) E)) (minpoly F x)).symm

noncomputable def TauCeti.galEquivNormalClosure {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (x : E) : (minpoly F x).Gal ≃* Gal(↥(IntermediateField.normalClosure F (↥F⟮x⟯) E)/F)

The Galois group of a minimal polynomial is the automorphism group of the normal closure of the simple extension, via conjugation by the field comparison.

Equations

• TauCeti.galEquivNormalClosure x = (TauCeti.splittingFieldEquivNormalClosure x).autCongr

@[simp]

theorem TauCeti.galEquivNormalClosure_apply {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (x : E) (σ : (minpoly F x).Gal) (y : (minpoly F x).SplittingField) : ((galEquivNormalClosure x) σ) ((splittingFieldEquivNormalClosure x) y) = (splittingFieldEquivNormalClosure x) (σ y)

The group comparison intertwines evaluation with the field comparison.

theorem TauCeti.map_stabilizer_galEquivNormalClosure {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (x : E) (y : ↑((minpoly F x).rootSet (minpoly F x).SplittingField)) : Subgroup.map (galEquivNormalClosure x).toMonoidHom (MulAction.stabilizer (minpoly F x).Gal y) = F⟮(splittingFieldEquivNormalClosure x) ↑y⟯.fixingSubgroup

A point stabilizer corresponds to the subgroup fixing the simple field generated by the corresponding root in the normal closure. The action on the source is the intrinsic action on the roots in the splitting field.

theorem TauCeti.exists_root_map_stabilizer_eq_fixingSubgroup {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [Normal F E] (x : E) : ∃ (y : ↑((minpoly F x).rootSet (minpoly F x).SplittingField)), ↑((splittingFieldEquivNormalClosure x) ↑y) = x ∧ Subgroup.map (galEquivNormalClosure x).toMonoidHom (MulAction.stabilizer (minpoly F x).Gal y) = (IntermediateField.restrict ⋯).fixingSubgroup

There is a root corresponding to the original generator x, and its stabilizer maps to the subgroup fixing the original simple extension inside its normal closure. In particular, the comparison identifies this field, rather than only an unspecified conjugate of it.

theorem TauCeti.index_map_stabilizer_galEquivNormalClosure {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) (y : ↑((minpoly F x).rootSet (minpoly F x).SplittingField)) : (Subgroup.map (galEquivNormalClosure x).toMonoidHom (MulAction.stabilizer (minpoly F x).Gal y)).index = Module.finrank F ↥F⟮x⟯

When the minimal polynomial is separable, the image of a point stabilizer has index equal to the degree of the original simple extension.