Point stabilizers of the Galois action on the roots #

Let p be a polynomial over a field F and let L = p.SplittingField. The Galois group Polynomial.Gal p acts on p.rootSet L, and this file identifies the stabilizer of a root x with a relative Galois group: it is the subgroup of p.Gal fixing the simple extension F⟮x⟯ pointwise. The fixed-field and endpoint readings of the action against the Galois correspondence go through that identification.

The identification itself needs no hypothesis on p. Recovering the fixed field and the two ends of the Galois correspondence needs IsGalois F L. The index, however, is an orbit-stabilizer calculation: it only needs the minimal polynomial of the chosen root to be separable, and for irreducible p this follows from p.Separable.

Main results #

TauCeti.stabilizer_eq_fixingSubgroup_adjoin_simple: the stabilizer of a root is the fixing subgroup of the field the root generates.
TauCeti.isGaloisGroup_stabilizer: when the splitting field is Galois, the stabilizer of a root is a Galois group for the splitting field over the field the root generates.
TauCeti.isPretransitive_rootSet_of_irreducible: in a normal extension the Galois group acts transitively on the roots of an irreducible polynomial.
TauCeti.index_stabilizer_eq_natDegree_minpoly, TauCeti.index_stabilizer_eq_natDegree: the index of the stabilizer is the degree of the minimal polynomial of the root, so for irreducible separable p it is p.natDegree.
TauCeti.stabilizer_eq_bot_iff_adjoin_simple_eq_top, TauCeti.stabilizer_eq_top_iff_adjoin_simple_eq_bot: the two ends of the correspondence, a root that generates the whole splitting field and a root that lies in the base field.
TauCeti.coe_rootSet_eq_orbit_of_irreducible, TauCeti.rootSetEquivQuotientStabilizer: for the action of Gal(M/F) on the roots in a normal extension M / F of an irreducible polynomial, the roots form one orbit and are identified equivariantly with the cosets of the stabilizer of a chosen root α, the coset of ρ corresponding to the root ρ • α.

Implementation notes #

The action used here is Mathlib's Polynomial.Gal.galActionAux, the intrinsic action on p.rootSet p.SplittingField, for which ↑(g • x) is literally g ↑x. Mathlib also has Polynomial.Gal.galAction on p.rootSet E for a splitting extension E, but its instance for E = p.SplittingField is the transport of galActionAux along Polynomial.Gal.rootsEquivRoots, which goes through the Algebra p.SplittingField p.SplittingField instance built from IsSplittingField.lift rather than through the identity. The two actions are isomorphic but not the same instance, and only the intrinsic one has stabilizers that the Galois correspondence reads directly. No Fact instance is introduced below, so galActionAux is the only candidate and no ambiguity arises.

The stabilizer of a root #

source

theorem TauCeti.stabilizer_eq_fixingSubgroup_adjoin_simple {F : Type u_1} [Field F] {p : Polynomial F} (x : ↑(p.rootSet p.SplittingField)) :

MulAction.stabilizer p.Gal x = F⟮↑x⟯.fixingSubgroup

The stabilizer of a root is a relative Galois group. An automorphism of the splitting field fixes a root x exactly when it fixes the subfield F⟮x⟯ pointwise, so the point stabilizer of the root action is the fixing subgroup of that subfield.

No hypothesis on p is needed: the statement is about one root and the field it generates, not about the polynomial.

source

instance TauCeti.isGaloisGroup_stabilizer {F : Type u_1} [Field F] {p : Polynomial F} [IsGalois F p.SplittingField] (x : ↑(p.rootSet p.SplittingField)) :

IsGaloisGroup (↥(MulAction.stabilizer p.Gal x)) (↥F⟮↑x⟯) p.SplittingField

The stabilizer of a root is the Galois group over the field the root generates. When the splitting field is Galois over F, the stabilizer of a root x is a Galois group for the splitting field over F⟮x⟯.

This is the IsGaloisGroup form of TauCeti.stabilizer_eq_fixingSubgroup_adjoin_simple; through IsGaloisGroup.mulEquivCongr it identifies the stabilizer with Gal(p.SplittingField/F⟮x⟯).

The index of a point stabilizer #

source

theorem TauCeti.index_stabilizer_eq_natDegree_minpoly {F : Type u_1} [Field F] {p : Polynomial F} (x : ↑(p.rootSet p.SplittingField)) (hsep : (minpoly F ↑x).Separable) :

(MulAction.stabilizer p.Gal x).index = (minpoly F ↑x).natDegree

The index of a point stabilizer is the degree of the minimal polynomial of the point. The orbit of x consists of all roots of its minimal polynomial in the normal splitting field, and separability makes their number its degree, so this is orbit-stabilizer applied to TauCeti.natCard_orbit_eq_natDegree_minpoly_splittingField.

source

theorem TauCeti.index_stabilizer_eq_natDegree {F : Type u_1} [Field F] {p : Polynomial F} (hp : Irreducible p) (hsep : p.Separable) (x : ↑(p.rootSet p.SplittingField)) :

(MulAction.stabilizer p.Gal x).index = p.natDegree

For an irreducible separable polynomial every point stabilizer has index the degree. This is the form the permutation representation uses: a transitive subgroup of degree n has point stabilizers of index n.

Separability cannot be dropped: an inseparable irreducible polynomial has fewer roots than its degree.

The two ends of the correspondence #

source

theorem TauCeti.stabilizer_eq_bot_iff_adjoin_simple_eq_top {F : Type u_1} [Field F] {p : Polynomial F} [IsGalois F p.SplittingField] (x : ↑(p.rootSet p.SplittingField)) :

MulAction.stabilizer p.Gal x = ⊥ ↔ F⟮↑x⟯ = ⊤

A root with trivial stabilizer is a primitive element, and conversely. Together with TauCeti.stabilizer_eq_top_iff_adjoin_simple_eq_bot this pins the orientation of the correspondence: the stabilizer shrinks as the field the root generates grows.

source

theorem TauCeti.stabilizer_eq_top_iff_adjoin_simple_eq_bot {F : Type u_1} [Field F] {p : Polynomial F} [IsGalois F p.SplittingField] (x : ↑(p.rootSet p.SplittingField)) :

MulAction.stabilizer p.Gal x = ⊤ ↔ F⟮↑x⟯ = ⊥

A root fixed by the whole Galois group lies in the base field, and conversely. The splitting field being Galois over F is what makes the fixed field of the whole group F itself; over an inseparable extension a root outside F can be fixed by every automorphism.

The roots of an irreducible polynomial in a normal extension #

source

theorem TauCeti.coe_rootSet_eq_orbit_of_irreducible {F : Type u_1} [Field F] {M : Type u_2} [Field M] [Algebra F M] [Normal F M] {q : Polynomial F} (hq : Irreducible q) {α : M} (hα : α ∈ q.rootSet M) :

q.rootSet M = MulAction.orbit Gal(M/F) α

In a normal extension M / F, the roots in M of an irreducible polynomial over F form one orbit of Gal(M/F): the orbit of any of them.

source

theorem TauCeti.isPretransitive_rootSet_of_irreducible {F : Type u_1} [Field F] {M : Type u_2} [Field M] [Algebra F M] [Normal F M] {q : Polynomial F} (hq : Irreducible q) :

MulAction.IsPretransitive Gal(M/F) ↑(q.rootSet M)

In a normal extension M / F, Gal(M/F) acts transitively on the roots in M of an irreducible polynomial over F.

source

theorem TauCeti.stabilizer_rootSet_mk {F : Type u_1} [Field F] {M : Type u_2} [Field M] [Algebra F M] {q : Polynomial F} {α : M} (hα : α ∈ q.rootSet M) :

MulAction.stabilizer Gal(M/F) ⟨α, hα⟩ = MulAction.stabilizer Gal(M/F) α

The stabilizer of a root, as a point of the root set, is its stabilizer as an element of the field.

source

noncomputable def TauCeti.rootSetEquivQuotientStabilizer {F : Type u_1} [Field F] {M : Type u_2} [Field M] [Algebra F M] [Normal F M] {q : Polynomial F} (hq : Irreducible q) {α : M} (hα : α ∈ q.rootSet M) :

↑(q.rootSet M) ≃ Gal(M/F) ⧸ MulAction.stabilizer Gal(M/F) α

The roots in a normal extension M / F of an irreducible polynomial over F, as the cosets of the stabilizer in Gal(M/F) of a chosen root: the transitive-action identification TauCeti.quotientStabilizerEquiv, transported along TauCeti.stabilizer_rootSet_mk.

Equations