Degree of the root permutation representation

This file records the degree bookkeeping for the faithful permutation representation of the Galois group of a polynomial. A separable polynomial has natDegree distinct roots in its splitting field, so its intrinsic root set admits a numbering by Fin p.natDegree. No numbering is chosen globally: the result is stated as a Nonempty equivalence, leaving later comparisons with reference permutation groups to carry their chosen numbering explicitly.

The Galois action itself is faithful over every splitting extension. Consequently its image has the same cardinality as the polynomial Galois group, and the Galois-group order divides the factorial of the polynomial degree. For the same reason the Galois group of a polynomial of degree at most four embeds in a symmetric group on at most four points, and is therefore solvable.

Main results

• TauCeti.nonempty_rootSet_splittingField_equiv_fin: a separable polynomial's roots in its splitting field can be numbered by Fin p.natDegree.
• TauCeti.natCard_galActionHom_range: the faithful Galois image has the order of the polynomial Galois group.
• TauCeti.natCard_gal_dvd_factorial_card_rootSet: the Galois-group order divides the factorial of the number of distinct roots.
• TauCeti.natCard_gal_dvd_factorial_natDegree: the order of a polynomial's Galois group divides the factorial of its degree.
• TauCeti.isSolvable_gal_of_natDegree_le_four: a polynomial of degree at most four has a solvable Galois group.

The proofs reuse Mathlib's Polynomial.card_rootSet_eq_natDegree, Polynomial.Gal.galActionHom_injective, MonoidHom.ofInjective, and Lagrange's theorem. This is the degree bookkeeping used by the orbit-to-factor dictionary and by low-degree label predicates.

Numbering the roots

theorem TauCeti.nonempty_rootSet_splittingField_equiv_fin {F : Type u} [Field F] (p : Polynomial F) (hsep : p.Separable) : Nonempty (↑(p.rootSet p.SplittingField) ≃ Fin p.natDegree)

A separable polynomial's roots in its splitting field admit a numbering by Fin p.natDegree.

Only existence is recorded: later statements choose a numbering locally, so the intrinsic root set is not equipped with a global order.

The faithful image

theorem TauCeti.natCard_galActionHom_range {F : Type u} [Field F] (p : Polynomial F) (E : Type v) [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) p).Splits] : Nat.card ↥(Polynomial.Gal.galActionHom p E).range = Nat.card p.Gal

The image of the Galois action on the roots in any splitting extension has the same order as the polynomial Galois group.

theorem TauCeti.natCard_gal_dvd_factorial_card_rootSet {F : Type u} [Field F] (p : Polynomial F) : Nat.card p.Gal ∣ (Fintype.card ↑(p.rootSet p.SplittingField)).factorial

The order of the Galois group of a polynomial divides the factorial of the number of its distinct roots in the splitting field, through the faithful root action.

theorem TauCeti.natCard_gal_dvd_factorial_natDegree {F : Type u} [Field F] (p : Polynomial F) : Nat.card p.Gal ∣ p.natDegree.factorial

The order of the Galois group of a polynomial divides the factorial of its degree, through its faithful action on the distinct roots.

Solvability in degree at most four

theorem TauCeti.isSolvable_gal_of_natDegree_le_four {F : Type u} [Field F] {p : Polynomial F} (hp : p.natDegree ≤ 4) : Group.IsSolvable p.Gal

A polynomial of degree at most four has a solvable Galois group. The Galois group acts faithfully on the at most four roots in the splitting field, and the symmetric group on at most four points is solvable. Neither separability nor irreducibility is needed. This is a statement about the group, not about solvableByRad.