Polynomials with full symmetric Galois group

Polynomial.HasFullSymmetricGaloisGroup f requires separability and surjectivity of the Galois action on the roots in the splitting field. Separability ensures that this is the symmetric group on f.natDegree points, rather than on a smaller set of distinct roots. The predicate is also available as f.HasFullSymmetricGaloisGroup by dot notation.

The property can be checked in any field where f splits, or by checking that the Galois group has order f.natDegree!. A numbering of the roots gives an explicit group isomorphism with the permutations of Fin f.natDegree. These interfaces connect reduction criteria for Galois groups with realizations of symmetric groups over the rational numbers.

theorem Polynomial.instFactSplitsSplittingFieldMapAlgebraMap_tauCeti {F : Type u_1} [Field F] (f : Polynomial F) : Fact (map (algebraMap F f.SplittingField) f).Splits

def Polynomial.HasFullSymmetricGaloisGroup {F : Type u_1} [Field F] (f : Polynomial F) : Prop

A polynomial has full symmetric Galois group if it is separable and every permutation of its roots in the splitting field is induced by a Galois automorphism.

Equations

• f.HasFullSymmetricGaloisGroup = (f.Separable ∧ Function.Surjective ⇑(Polynomial.Gal.galActionHom f f.SplittingField))

theorem Polynomial.HasFullSymmetricGaloisGroup.mk {F : Type u_1} [Field F] {f : Polynomial F} (hsep : f.Separable) (hsurj : Function.Surjective ⇑(Gal.galActionHom f f.SplittingField)) : f.HasFullSymmetricGaloisGroup

Separability and surjectivity of the action on splitting-field roots give full symmetric Galois group.

theorem Polynomial.HasFullSymmetricGaloisGroup.separable {F : Type u_1} [Field F] {f : Polynomial F} (hf : f.HasFullSymmetricGaloisGroup) : f.Separable

A polynomial with full symmetric Galois group is separable.

theorem Polynomial.HasFullSymmetricGaloisGroup.surjective_galActionHom {F : Type u_1} [Field F] {f : Polynomial F} (hf : f.HasFullSymmetricGaloisGroup) : Function.Surjective ⇑(Gal.galActionHom f f.SplittingField)

Every permutation of the splitting-field roots of a polynomial with full symmetric Galois group is induced by a Galois automorphism.

theorem Polynomial.hasFullSymmetricGaloisGroup_iff_natCard_gal_eq_factorial_natDegree {F : Type u_1} [Field F] {f : Polynomial F} (hsep : f.Separable) : f.HasFullSymmetricGaloisGroup ↔ Nat.card f.Gal = f.natDegree.factorial

Among separable polynomials, full symmetric Galois group is equivalent to the Galois group having order equal to the factorial of the degree.

theorem Polynomial.hasFullSymmetricGaloisGroup_iff_separable_and_surjective_galActionHom {F : Type u_1} [Field F] {f : Polynomial F} (E : Type u_2) [Field E] [Algebra F E] [hsplit : Fact (map (algebraMap F E) f).Splits] : f.HasFullSymmetricGaloisGroup ↔ f.Separable ∧ Function.Surjective ⇑(Gal.galActionHom f E)

Full symmetric Galois group can be checked on the roots in any splitting extension.

theorem Polynomial.HasFullSymmetricGaloisGroup.nonempty_mulEquiv {F : Type u_1} [Field F] {f : Polynomial F} (hf : f.HasFullSymmetricGaloisGroup) : Nonempty (f.Gal ≃* Equiv.Perm (Fin f.natDegree))

A polynomial with full symmetric Galois group realizes the symmetric group on as many points as its degree. No numbering of its roots is fixed globally.

theorem Polynomial.not_hasFullSymmetricGaloisGroup_pow_of_not_isUnit {F : Type u_1} [Field F] {f : Polynomial F} (hf : ¬IsUnit f) (n : ℕ) (hn : 2 ≤ n) : ¬(f ^ n).HasFullSymmetricGaloisGroup

A power of a nonunit polynomial with exponent at least two cannot have full symmetric Galois group.

@[simp]

theorem Polynomial.not_hasFullSymmetricGaloisGroup_X_pow {F : Type u_1} [Field F] (n : ℕ) (hn : 2 ≤ n) : ¬(X ^ n).HasFullSymmetricGaloisGroup

Repeated roots rule out full symmetric Galois group, even when the action on the distinct roots is surjective: in particular X ^ n is excluded for 2 ≤ n.