Galois orbits on the roots of a polynomial

Let p be a polynomial over a field F and let E be an extension in which p splits. The Galois group Polynomial.Gal p acts on p.rootSet E, and this file identifies the orbits of that action with the monic irreducible factors of p.

The invariant that separates the orbits is the minimal polynomial: two roots lie in the same orbit exactly when they have the same minimal polynomial over F, so the orbit of a root is the whole root set of its minimal polynomial. When p is nonzero, passing to the orbit quotient turns this into a bijection with the distinct monic irreducible factors of p, that is, with the members of Polynomial.Factors p.

The dictionary also identifies transitivity of the root action with irreducibility for a separable polynomial of positive degree, together with its relative form: inside a normal extension, irreducibility over an intermediate field is transitivity of the subgroup fixing that field. It records the same descriptions for the action inside the splitting field itself, where an irreducible polynomial acts transitively.

For the intrinsic action, this file also records the evaluation rule on the splitting field and the instances identifying Polynomial.Gal p as a Galois group for that field over the base.

Main results

• Polynomial.Gal.galActionHom_eq_permCongr: the root permutations in two splitting extensions correspond under Polynomial.Gal.rootsEquivRoots.
• TauCeti.mem_orbit_iff_minpoly_eq: two roots of p are in the same Galois orbit exactly when their minimal polynomials agree.
• TauCeti.image_val_orbit_eq_rootSet_minpoly: read inside E, the orbit of a root is the root set of its minimal polynomial.
• TauCeti.natCard_orbit_eq_natDegree_minpoly: when the corresponding minimal polynomial is separable, an orbit has as many elements as its degree.
• TauCeti.isPretransitive_iff_irreducible: for separable p of positive degree, transitivity of the root action is equivalent to irreducibility of p.
• TauCeti.isPretransitive_range_galActionHom: the Galois image of an irreducible polynomial, as a group of permutations of the roots, is transitive.
• TauCeti.isPretransitive_gal_rootSet_of_isPretransitive_algEquiv: in any splitting extension E, if the automorphism group Gal(E/F) is transitive on the roots, then so is p.Gal.
• TauCeti.isPretransitive_algEquiv_rootSet_iff_gal: in a normal splitting extension E, the automorphism group Gal(E/F) is transitive on the roots exactly when p.Gal is.
• TauCeti.irreducible_map_iff_isPretransitive_fixingSubgroup: in a normal splitting extension E, a separable p stays irreducible over an intermediate field K exactly when the automorphisms fixing K act transitively on the roots.
• TauCeti.mem_orbit_iff_minpoly_eq_splittingField, TauCeti.image_val_orbit_eq_rootSet_minpoly_splittingField, TauCeti.natCard_orbit_eq_natDegree_minpoly_splittingField: the same three descriptions of an orbit for the intrinsic action on the roots in the splitting field.
• Polynomial.Gal.galActionAux_isPretransitive: inside the splitting field, an irreducible polynomial has a transitive root action.
• Polynomial.Gal.galActionAux_isPretransitive_of_dvd_pow: the same for every divisor of a power of an irreducible polynomial, separable or not.
• Polynomial.Gal.smul_eq_apply: the action on the splitting field is evaluation.
• TauCeti.galIsGaloisGroup: Polynomial.Gal p is a Galois group for its splitting field.
• TauCeti.orbitQuotientEquivFactors: the orbit quotient is in bijection with the monic irreducible factors of p, the orbit of a root going to its minimal polynomial.
• TauCeti.natCard_orbit_eq_natDegree_factor: along that bijection, a separable factor has as many roots in the matching orbit as its degree.

The minimal polynomial as an invariant of a root

@[simp]

theorem TauCeti.minpoly_rootsEquivRoots {F : Type u} [Field F] {p : Polynomial F} (E : Type v) [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) p).Splits] (E' : Type w) [Field E'] [Algebra F E'] [Fact (Polynomial.map (algebraMap F E') p).Splits] (x : ↑(p.rootSet E)) : minpoly F ↑((Polynomial.Gal.rootsEquivRoots p E E') x) = minpoly F ↑x

The minimal polynomial of a root of p does not depend on the splitting extension in which the root is read: it is preserved by the Galois-equivariant comparison of two root sets.

theorem Polynomial.Gal.galActionHom_eq_permCongr {F : Type u} [Field F] (p : Polynomial F) (E : Type v) [Field E] [Algebra F E] [Fact (map (algebraMap F E) p).Splits] (E' : Type w) [Field E'] [Algebra F E'] [Fact (map (algebraMap F E') p).Splits] (g : p.Gal) : (galActionHom p E') g = (rootsEquivRoots p E E').permCongr ((galActionHom p E) g)

The permutation of the roots in one splitting extension induced by a Galois automorphism is the transport, along Polynomial.Gal.rootsEquivRoots, of the permutation it induces in another. So any invariant of permutations that is preserved by relabelling, such as the cycle type, does not depend on the splitting extension in which the roots are read.

@[simp]

theorem TauCeti.mem_orbit_iff_minpoly_eq {F : Type u} [Field F] {p : Polynomial F} (E : Type v) [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) p).Splits] {x y : ↑(p.rootSet E)} : x ∈ MulAction.orbit p.Gal y ↔ minpoly F ↑x = minpoly F ↑y

Two roots of p lie in the same Galois orbit exactly when their minimal polynomials over the base field agree.

The orbit of a root

theorem TauCeti.orbit_eq_preimage_rootSet_minpoly {F : Type u} [Field F] {p : Polynomial F} (E : Type v) [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) p).Splits] (x : ↑(p.rootSet E)) : MulAction.orbit p.Gal x = Subtype.val ⁻¹' (minpoly F ↑x).rootSet E

The orbit of a root of p consists of the roots of its minimal polynomial.

@[simp]

theorem TauCeti.image_val_orbit_eq_rootSet_minpoly {F : Type u} [Field F] {p : Polynomial F} (E : Type v) [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) p).Splits] (x : ↑(p.rootSet E)) : Subtype.val '' MulAction.orbit p.Gal x = (minpoly F ↑x).rootSet E

Read inside the ambient field, the orbit of a root of p is exactly the root set of its minimal polynomial.

theorem TauCeti.natCard_orbit_eq_natDegree_minpoly {F : Type u} [Field F] {p : Polynomial F} (E : Type v) [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) p).Splits] (x : ↑(p.rootSet E)) (hsep : (minpoly F ↑x).Separable) : Nat.card ↑(MulAction.orbit p.Gal x) = (minpoly F ↑x).natDegree

When the minimal polynomial of a root is separable, its orbit has as many elements as the degree of that minimal polynomial.

Transitivity and irreducibility

theorem TauCeti.isPretransitive_iff_irreducible {F : Type u} [Field F] {p : Polynomial F} (E : Type v) [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) p).Splits] (hsep : p.Separable) (hdeg : 0 < p.natDegree) : MulAction.IsPretransitive p.Gal ↑(p.rootSet E) ↔ Irreducible p

For a separable polynomial of positive degree, the Galois action on the roots in a splitting extension is transitive exactly when the polynomial is irreducible.

Separability cannot be dropped: over ℚ the polynomial (X ^ 2 - 2) ^ 2 is reducible, yet its Galois group acts transitively on its two distinct roots (TauCeti.isPretransitive_gal_X_sq_sub_two_sq). Without separability the forward implication only says that p is a unit times a power of one irreducible polynomial.

theorem TauCeti.isPretransitive_range_galActionHom {F : Type u} [Field F] {p : Polynomial F} (E : Type v) [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) p).Splits] (hp : Irreducible p) : MulAction.IsPretransitive ↥(Polynomial.Gal.galActionHom p E).range ↑(p.rootSet E)

The Galois image of an irreducible polynomial, as a group of permutations of its roots in a splitting extension, acts transitively.

theorem TauCeti.isPretransitive_gal_rootSet_of_isPretransitive_algEquiv {F : Type u} [Field F] {p : Polynomial F} (E : Type v) [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) p).Splits] (h : MulAction.IsPretransitive Gal(E/F) ↑(p.rootSet E)) : MulAction.IsPretransitive p.Gal ↑(p.rootSet E)

If the automorphism group Gal(E/F) of an extension E in which p splits acts transitively on the roots of p in E, then so does the Galois group p.Gal. No normality is needed, since the action of Gal(E/F) factors through the restriction Polynomial.Gal.restrict p E. For the converse, which needs E normal, see TauCeti.isPretransitive_algEquiv_rootSet_iff_gal.

theorem TauCeti.isPretransitive_algEquiv_rootSet_iff_gal {F : Type u} [Field F] {p : Polynomial F} (E : Type v) [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) p).Splits] [Normal F E] : MulAction.IsPretransitive Gal(E/F) ↑(p.rootSet E) ↔ MulAction.IsPretransitive p.Gal ↑(p.rootSet E)

In a normal extension E in which p splits, the automorphism group Gal(E/F) acts transitively on the roots of p in E exactly when the Galois group p.Gal does. This lets transitivity criteria stated for p.Gal, such as TauCeti.isPretransitive_iff_irreducible, be used for Gal(E/F). The forward implication holds without normality; it is TauCeti.isPretransitive_gal_rootSet_of_isPretransitive_algEquiv.

Normality cannot be dropped: for p = X ^ 2 - 2 over ℚ and E = ℚ(α) with α the real fourth root of 2, both automorphisms of E fix α ^ 2 = √2, so Gal(E/ℚ) fixes each root of p, whereas p.Gal swaps them.

theorem TauCeti.irreducible_map_iff_isPretransitive_fixingSubgroup {F : Type u} [Field F] {p : Polynomial F} (E : Type v) [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) p).Splits] [Normal F E] (K : IntermediateField F E) (hsep : p.Separable) (hdeg : 0 < p.natDegree) : Irreducible (Polynomial.map (algebraMap F ↥K) p) ↔ MulAction.IsPretransitive ↥K.fixingSubgroup ↑(p.rootSet E)

Irreducibility over an intermediate field. Let E be a normal extension of F in which a separable polynomial p of positive degree splits, and let K be an intermediate field. Then p stays irreducible over K exactly when the automorphisms of E fixing K act transitively on the roots of p in E.

The action inside the splitting field

@[simp]

theorem Polynomial.Gal.smul_eq_apply {F : Type u} [Field F] {p : Polynomial F} (g : p.Gal) (y : p.SplittingField) : g • y = g y

The action of the polynomial Galois group on its splitting field is evaluation.

instance TauCeti.galSMulCommClass {F : Type u} [Field F] {p : Polynomial F} : SMulCommClass p.Gal F p.SplittingField

The Galois action on the splitting field commutes with the scalar action of the base field.

This is Mathlib's AlgEquiv.apply_smulCommClass' for p.SplittingField ≃ₐ[F] p.SplittingField; Polynomial.Gal p is a distinct type carrying the derived action, so the instance is transported here.

instance TauCeti.galIsGaloisGroup {F : Type u} [Field F] {p : Polynomial F} [IsGalois F p.SplittingField] : IsGaloisGroup p.Gal F p.SplittingField

Polynomial.Gal p is a Galois group for L/F, where L = p.SplittingField: it acts faithfully on L with fixed field F.

Mathlib's IsGaloisGroup.of_isGalois says this for Gal(L/F), but Polynomial.Gal p is a distinct type with its own action, so the instance is restated here; it is what makes the IsGaloisGroup form of the Galois correspondence, and the fixed-field lemmas that come with it, apply to the polynomial Galois group.

@[simp]

theorem Polynomial.Gal.coe_smul {F : Type u} [Field F] {p : Polynomial F} (g : p.Gal) (x : ↑(p.rootSet p.SplittingField)) : ↑(g • x) = g ↑x

The Galois action on the roots in the splitting field is the action by evaluation.

@[simp]

theorem TauCeti.mem_orbit_iff_minpoly_eq_splittingField {F : Type u} [Field F] {p : Polynomial F} {x y : ↑(p.rootSet p.SplittingField)} : x ∈ MulAction.orbit p.Gal y ↔ minpoly F ↑x = minpoly F ↑y

Two roots of p in the splitting field lie in the same Galois orbit exactly when their minimal polynomials over the base field agree.

This is TauCeti.mem_orbit_iff_minpoly_eq for the intrinsic action; see the note above for why that instance is not the one the general statement carries.

theorem TauCeti.orbit_eq_preimage_rootSet_minpoly_splittingField {F : Type u} [Field F] {p : Polynomial F} (x : ↑(p.rootSet p.SplittingField)) : MulAction.orbit p.Gal x = Subtype.val ⁻¹' (minpoly F ↑x).rootSet p.SplittingField

The orbit of a root of p in the splitting field consists of the roots of its minimal polynomial.

This is TauCeti.orbit_eq_preimage_rootSet_minpoly for the intrinsic action.

@[simp]

theorem TauCeti.image_val_orbit_eq_rootSet_minpoly_splittingField {F : Type u} [Field F] {p : Polynomial F} (x : ↑(p.rootSet p.SplittingField)) : Subtype.val '' MulAction.orbit p.Gal x = (minpoly F ↑x).rootSet p.SplittingField

Read inside the splitting field, the orbit of a root of p is exactly the root set of its minimal polynomial.

This is TauCeti.image_val_orbit_eq_rootSet_minpoly for the intrinsic action.

theorem TauCeti.natCard_orbit_eq_natDegree_minpoly_splittingField {F : Type u} [Field F] {p : Polynomial F} (x : ↑(p.rootSet p.SplittingField)) (hsep : (minpoly F ↑x).Separable) : Nat.card ↑(MulAction.orbit p.Gal x) = (minpoly F ↑x).natDegree

When the minimal polynomial of a root is separable, its orbit in the splitting field has as many elements as the degree of that minimal polynomial.

This is TauCeti.natCard_orbit_eq_natDegree_minpoly for the intrinsic action.

theorem Polynomial.Gal.galActionAux_isPretransitive_of_dvd_pow {F : Type u} [Field F] {p q : Polynomial F} (hq : Irreducible q) {n : ℕ} (hpq : p ∣ q ^ n) : MulAction.IsPretransitive p.Gal ↑(p.rootSet p.SplittingField)

The root action of a divisor of a power of an irreducible polynomial is transitive. If p ∣ q ^ n with q irreducible, every root of p in its splitting field is a root of q, so all of them have the same minimal polynomial and lie in one Galois orbit.

Without separability, transitivity therefore does not force irreducibility: (X ^ 2 - 2) ^ 2 is the witness over ℚ (TauCeti.isPretransitive_gal_X_sq_sub_two_sq).

theorem Polynomial.Gal.galActionAux_isPretransitive {F : Type u} [Field F] {p : Polynomial F} (hp : Irreducible p) : MulAction.IsPretransitive p.Gal ↑(p.rootSet p.SplittingField)

The root action of an irreducible polynomial is transitive.

This is Polynomial.Gal.galAction_isPretransitive for the intrinsic action on the roots in the splitting field; see the note above for why that instance is not the one Mathlib's statement carries.

Orbits and monic irreducible factors

theorem TauCeti.exists_mem_rootSet_minpoly_eq {F : Type u} [Field F] {p : Polynomial F} (E : Type v) [CommRing E] [IsDomain E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) p).Splits] (hp : p ≠ 0) (q : p.Factors) : ∃ (x : ↑(p.rootSet E)), minpoly F ↑x = ↑q

Every monic irreducible factor of a nonzero p is the minimal polynomial of a root of p in a splitting extension.

noncomputable def TauCeti.orbitQuotientEquivFactors {F : Type u} [Field F] (p : Polynomial F) (E : Type v) [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) p).Splits] (hp : p ≠ 0) : MulAction.orbitRel.Quotient p.Gal ↑(p.rootSet E) ≃ p.Factors

The Galois orbits on the roots of a nonzero p in a splitting extension are in bijection with its monic irreducible factors; the orbit of a root goes to its minimal polynomial.

Equations

• TauCeti.orbitQuotientEquivFactors p E hp = Equiv.ofBijective (Quotient.lift (fun (x : ↑(p.rootSet E)) => ⟨minpoly F ↑x, ⋯⟩) ⋯) ⋯

@[simp]

theorem TauCeti.orbitQuotientEquivFactors_apply_mk {F : Type u} [Field F] {p : Polynomial F} (E : Type v) [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) p).Splits] (hp : p ≠ 0) (x : ↑(p.rootSet E)) : ↑((orbitQuotientEquivFactors p E hp) ⟦x⟧) = minpoly F ↑x

The orbit-factor equivalence sends the orbit represented by x to minpoly F x.

@[simp]

theorem TauCeti.orbitQuotientEquivFactors_symm_apply_eq_mk_iff {F : Type u} [Field F] {p : Polynomial F} (E : Type v) [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) p).Splits] (hp : p ≠ 0) (q : p.Factors) (x : ↑(p.rootSet E)) : (orbitQuotientEquivFactors p E hp).symm q = ⟦x⟧ ↔ ↑q = minpoly F ↑x

A factor corresponds to the orbit represented by x exactly when its underlying polynomial is the minimal polynomial of x.

theorem TauCeti.natCard_orbit_eq_natDegree_factor {F : Type u} [Field F] {p : Polynomial F} (E : Type v) [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) p).Splits] (hp : p ≠ 0) (ω : MulAction.orbitRel.Quotient p.Gal ↑(p.rootSet E)) (hsep : (↑((orbitQuotientEquivFactors p E hp) ω)).Separable) : Nat.card ↑ω.orbit = (↑((orbitQuotientEquivFactors p E hp) ω)).natDegree

Along TauCeti.orbitQuotientEquivFactors, the degree of a separable monic irreducible factor is the number of roots in the matching Galois orbit.

theorem TauCeti.natCard_orbitQuotient {F : Type u} [Field F] (p : Polynomial F) (E : Type v) [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) p).Splits] (hp : p ≠ 0) : Nat.card (MulAction.orbitRel.Quotient p.Gal ↑(p.rootSet E)) = Nat.card p.Factors

For nonzero p, the number of Galois orbits on its roots is the number of its monic irreducible factors.