The Galois group of a quintic

An irreducible separable quintic over a field carries exactly one of the five transitive-group labels 5T1, …, 5T5. For a monic such quintic, two data constrain the label. Away from characteristic 2 the discriminant reads its parity: it is a square exactly for the even labels 5T1, 5T2 and 5T4. Dummit's F₂₀ resolvent sextic gives an unconditional implication from solvability to having a root in the base field; when its specialization is separable, the converse holds as well, so a root is then equivalent to one of the labels 5T1, 5T2 and 5T3.

For monic quintics, the two data together separate 5T3, 5T4 and 5T5 from each other and from the rest, and this file proves those three identifications, together with a fourth branch concluding 5T1 or 5T2:

discriminant	resolvent sextic	label
not a square	no root in the base field	5T5
a square	no root in the base field	5T4
not a square	a root in the base field	5T3
a square	a root in the base field	5T1 or 5T2

The fourth row concludes only that the label is 5T1 or 5T2. An independent criterion identifies 5T1 when the root field has a nonidentity automorphism.

The first two rows need no hypothesis on the resolvent sextic, because they use only the unconditional direction of the resolvent criterion, that a solvable Galois group produces a root. The last two rows read a root of the sextic as a containment, which is sound only when the specialized sextic is separable; separability of f does not imply it, since specialization can make the values of two distinct orbit elements collide.

The two characterizations behind the table, TauCeti.HasGaloisLabel.isSquare_discr_iff_five and TauCeti.HasGaloisLabel.exists_isRoot_specialize_quinticF20Spec_iff, are equivalences when the specialized resolvent is separable, so under that additional hypothesis they also supply the converse of each row.

Main results

• TauCeti.existsUnique_hasGaloisLabel_five: an irreducible separable quintic carries exactly one label, and TauCeti.hasGaloisLabel_five_iff_natCard_gal_eq: the order of its Galois group recognizes that label.
• TauCeti.hasGaloisLabel_five_four_of_surjective_galActionHom: a quintic whose Galois group acts on its roots by every permutation has the label 5T5.
• TauCeti.HasGaloisLabel.isSolvable_iff_five: the Galois group of a quintic is solvable exactly for the labels 5T1, 5T2 and 5T3.
• TauCeti.HasGaloisLabel.isSquare_discr_iff_five: the discriminant reads the parity of the label, and TauCeti.HasGaloisLabel.exists_isRoot_specialize_quinticF20Spec_iff: a root of the separable resolvent sextic reads solvability of the label.
• TauCeti.hasGaloisLabel_five_four_of_not_isSquare_discr_of_forall_not_isRoot, TauCeti.hasGaloisLabel_five_three_of_isSquare_discr_of_forall_not_isRoot, TauCeti.hasGaloisLabel_five_two_of_not_isSquare_discr_of_isRoot, TauCeti.hasGaloisLabel_five_zero_or_one_of_isSquare_discr_of_isRoot: the four rows of the table above.
• TauCeti.hasGaloisLabel_five_zero_of_exists_rootField_aut_ne_one: a nonidentity automorphism of a quintic root field identifies the label as 5T1.

References

• D. S. Dummit, Solving solvable quintics, Mathematics of Computation 57 (1991), §2.
• H. Cohen, A Course in Computational Algebraic Number Theory, §6.3.

theorem TauCeti.HasGaloisLabel.eq_of_five {F : Type u} [Field F] {f : Polynomial F} {j k : TransitiveGroupIndex 5} (hj : HasGaloisLabel f j) (hk : HasGaloisLabel f k) : j = k

A polynomial carries at most one label in degree five.

theorem TauCeti.existsUnique_hasGaloisLabel_five {F : Type u} [Field F] {f : Polynomial F} (hsep : f.Separable) (hirr : Irreducible f) (hdeg : f.natDegree = 5) : ∃! j : TransitiveGroupIndex 5, HasGaloisLabel f j

An irreducible separable quintic carries exactly one label, one of 5T1, …, 5T5.

theorem TauCeti.hasGaloisLabel_five_iff_natCard_gal_eq {F : Type u} [Field F] {f : Polynomial F} (hsep : f.Separable) (hirr : Irreducible f) (hdeg : f.natDegree = 5) (j : TransitiveGroupIndex 5) : HasGaloisLabel f j ↔ Nat.card f.Gal = Nat.card ↥(referenceSubgroup 5 j)

The order of the Galois group recognizes the label of a quintic. An irreducible separable quintic has the label 5Tj exactly when its Galois group has the order of the reference subgroup of 5Tj; the orders 5, 10, 20, 60, 120 of the five labels are pairwise distinct.

theorem TauCeti.hasGaloisLabel_five_four_of_surjective_galActionHom {F : Type u} [Field F] {f : Polynomial F} (hsep : f.Separable) (hirr : Irreducible f) (hdeg : f.natDegree = 5) {E : Type u_1} [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) f).Splits] (hsurj : Function.Surjective ⇑(Polynomial.Gal.galActionHom f E)) : HasGaloisLabel f ⟨4, hasGaloisLabel_five_four_of_surjective_galActionHom._proof_1⟩

The full symmetric label from a surjective Galois action. An irreducible separable quintic whose Galois group acts on its roots in some splitting extension by every permutation has the label 5T5.

theorem TauCeti.HasGaloisLabel.isSolvable_iff_five {F : Type u} [Field F] {f : Polynomial F} {j : TransitiveGroupIndex 5} (h : HasGaloisLabel f j) : Group.IsSolvable f.Gal ↔ ↑j < 3

Solvability and the quintic labels. The Galois group of a quintic with a label is solvable exactly for the labels 5T1, 5T2 and 5T3, the cyclic, dihedral and Frobenius groups. This is a statement about the group, not about solvableByRad.

theorem TauCeti.HasGaloisLabel.isSquare_discr_iff_five {F : Type u} [Field F] {f : Polynomial F} {j : TransitiveGroupIndex 5} (h : HasGaloisLabel f j) (hf : f.Monic) (hchar : ringChar F ≠ 2) : IsSquare f.discr ↔ ↑j = 0 ∨ ↑j = 1 ∨ ↑j = 3

The discriminant reads the parity of a quintic label. Away from characteristic 2, the discriminant of a monic quintic with a label is a square exactly for the even labels 5T1, 5T2 and 5T4.

theorem TauCeti.HasGaloisLabel.exists_isRoot_specialize_quinticF20Spec_of_lt_three {F : Type u} [Field F] {f : Polynomial F} {j : TransitiveGroupIndex 5} (h : HasGaloisLabel f j) (hf : f.Monic) (hj : ↑j < 3) : ∃ (a : F), (quinticF20Spec.specialize F f).IsRoot a

A solvable label gives the resolvent sextic a root. A monic quintic whose label is 5T1, 5T2 or 5T3 has a root of its F₂₀ resolvent in the base field. Nothing is assumed about the resolvent; the converse needs its separability, and is TauCeti.HasGaloisLabel.exists_isRoot_specialize_quinticF20Spec_iff.

theorem TauCeti.HasGaloisLabel.exists_isRoot_specialize_quinticF20Spec_iff {F : Type u} [Field F] {f : Polynomial F} {j : TransitiveGroupIndex 5} (h : HasGaloisLabel f j) (hf : f.Monic) (hres : (quinticF20Spec.specialize F f).Separable) : (∃ (a : F), (quinticF20Spec.specialize F f).IsRoot a) ↔ ↑j < 3

A root of the separable resolvent sextic reads solvability of the label. For a monic quintic with a label and a separable specialized F₂₀ resolvent, that resolvent has a root in the base field exactly for the labels 5T1, 5T2 and 5T3.

theorem TauCeti.hasGaloisLabel_five_four_of_not_isSquare_discr_of_forall_not_isRoot {F : Type u} [Field F] {f : Polynomial F} (hf : f.Monic) (hchar : ringChar F ≠ 2) (hirr : Irreducible f) (hdeg : f.natDegree = 5) (hdisc : ¬IsSquare f.discr) (hroot : ∀ (a : F), ¬(quinticF20Spec.specialize F f).IsRoot a) : HasGaloisLabel f ⟨4, hasGaloisLabel_five_four_of_surjective_galActionHom._proof_1⟩

The first row of the quintic table: 5T5. Away from characteristic 2, an irreducible monic quintic whose discriminant is not a square and whose F₂₀ resolvent has no root in the base field has the full symmetric group on its five roots.

theorem TauCeti.hasGaloisLabel_five_three_of_isSquare_discr_of_forall_not_isRoot {F : Type u} [Field F] {f : Polynomial F} (hf : f.Monic) (hchar : ringChar F ≠ 2) (hsep : f.Separable) (hirr : Irreducible f) (hdeg : f.natDegree = 5) (hdisc : IsSquare f.discr) (hroot : ∀ (a : F), ¬(quinticF20Spec.specialize F f).IsRoot a) : HasGaloisLabel f ⟨3, hasGaloisLabel_five_three_of_isSquare_discr_of_forall_not_isRoot._proof_1⟩

The second row of the quintic table: 5T4. Away from characteristic 2, an irreducible separable monic quintic whose discriminant is a square and whose F₂₀ resolvent has no root in the base field has the alternating group on its five roots.

theorem TauCeti.hasGaloisLabel_five_two_of_not_isSquare_discr_of_isRoot {F : Type u} [Field F] {f : Polynomial F} (hf : f.Monic) (hchar : ringChar F ≠ 2) (hirr : Irreducible f) (hdeg : f.natDegree = 5) (hdisc : ¬IsSquare f.discr) (hres : (quinticF20Spec.specialize F f).Separable) {a : F} (ha : (quinticF20Spec.specialize F f).IsRoot a) : HasGaloisLabel f ⟨2, hasGaloisLabel_five_two_of_not_isSquare_discr_of_isRoot._proof_1⟩

The third row of the quintic table: 5T3. Away from characteristic 2, an irreducible monic quintic whose discriminant is not a square and whose separable F₂₀ resolvent has a root in the base field has the Frobenius group of order twenty on its five roots.

theorem TauCeti.hasGaloisLabel_five_zero_or_one_of_isSquare_discr_of_isRoot {F : Type u} [Field F] {f : Polynomial F} (hf : f.Monic) (hchar : ringChar F ≠ 2) (hsep : f.Separable) (hirr : Irreducible f) (hdeg : f.natDegree = 5) (hdisc : IsSquare f.discr) (hres : (quinticF20Spec.specialize F f).Separable) {a : F} (ha : (quinticF20Spec.specialize F f).IsRoot a) : HasGaloisLabel f ⟨0, hasGaloisLabel_five_zero_or_one_of_isSquare_discr_of_isRoot._proof_1⟩ ∨ HasGaloisLabel f ⟨1, hasGaloisLabel_five_zero_or_one_of_isSquare_discr_of_isRoot._proof_2⟩

The fourth row of the quintic table: 5T1 or 5T2. Away from characteristic 2, an irreducible separable monic quintic whose discriminant is a square and whose separable F₂₀ resolvent has a root in the base field has either the cyclic group or the dihedral group of order ten on its five roots.

theorem TauCeti.hasGaloisLabel_five_iff_natCard_gal {F : Type u} [Field F] {f : Polynomial F} {j : TransitiveGroupIndex 5} (hsep : f.Separable) (hirr : Irreducible f) (hdeg : f.natDegree = 5) : HasGaloisLabel f j ↔ Nat.card f.Gal = Nat.card ↥(referenceSubgroup 5 j)

For an irreducible separable quintic, its label is determined by the order of its Galois group.

theorem TauCeti.hasGaloisLabel_five_zero_of_exists_rootField_aut_ne_one {F : Type u_1} [Field F] {q : Polynomial F} (hdeg : q.natDegree = 5) (E : Type u_2) [Field E] [Algebra F E] (x : E) (hminpoly : minpoly F x = q) (hgen : F⟮x⟯ = ⊤) (hAut : ∃ (σ : Gal(E/F)), σ ≠ 1) : HasGaloisLabel q ⟨0, hasGaloisLabel_five_zero_or_one_of_isSquare_discr_of_isRoot._proof_1⟩

A quintic whose root field has a nonidentity automorphism over the base field has label 5T1. The field E is generated by x, whose minimal polynomial is q.