The Galois group of a quartic

An irreducible separable quartic has transitive Galois image in Equiv.Perm (Fin 4), so it carries exactly one of the five labels 4T1, …, 4T5, the cyclic, Klein four, dihedral, alternating and symmetric groups. Away from characteristic 2 two tests read that label off the coefficients of f.

• The discriminant. The Galois image consists of even permutations exactly when f.discr is a square, which happens for 4T2 and 4T4 only.
• The resolvent cubic, the specialization at f of the D₄-specification TauCeti.quarticD4Spec of the invariant x₀x₂ + x₁x₃. Its roots in the base field detect confinement of the Galois image to a conjugate of the dihedral group of 4T3, which happens for 4T1, 4T2 and 4T3 only. No separation hypothesis is needed: a quartic and its resolvent cubic have the same discriminant, so the resolvent of a separable quartic is separable.

Together the two tests decide between 4T5, 4T4 and 4T2 and isolate the pair {4T1, 4T3}, which they do not separate: the cyclic and the dihedral group both have odd parity and both lie in a dihedral group of order eight. Separating them takes a further datum, namely whether f stays irreducible over the discriminant field TauCeti.discrField, the extension generated by a square root of the discriminant. The automorphisms fixing that field act on the roots through the even part of the Galois image, which is transitive for every quartic label except the cyclic one: the even part of 4T1 has order two, while that of 4T3 contains the Klein four-group. So f becomes reducible over the discriminant field exactly for 4T1, and this alone recognizes that label.

The resolvent cubic is monic of degree three (TauCeti.natDegree_quarticD4Spec_specialize), so Mathlib's Polynomial.irreducible_iff_roots_eq_zero_of_degree_le_three identifies having no root in the base field with irreducibility there. The first two rows below use that classical irreducible-resolvent formulation directly.

Main results

• TauCeti.existsUnique_hasGaloisLabel_four: an irreducible separable quartic carries exactly one label.
• TauCeti.HasGaloisLabel.isSquare_discr_iff_four and TauCeti.HasGaloisLabel.exists_isRoot_specialize_quarticD4Spec_iff: the discriminant test and the resolvent test, as conditions on the label.
• TauCeti.hasGaloisLabel_four_four_iff, TauCeti.hasGaloisLabel_four_three_iff, TauCeti.hasGaloisLabel_four_one_iff, TauCeti.hasGaloisLabel_four_zero_or_two_iff: the quartic decision table, one theorem for each of its four rows.
• TauCeti.hasGaloisLabel_four_one_iff_splits_resolvent: the row for 4T2 with the resolvent cubic asked to split completely, and TauCeti.hasGaloisLabel_four_zero_or_two_iff_existsUnique_isRoot_resolvent: the row for {4T1, 4T3} with the resolvent cubic asked to have exactly one root. Both drop the discriminant condition, which the resolvent condition already implies.
• TauCeti.HasGaloisLabel.irreducible_map_discrField_iff_ne_zero: a quartic with a label stays irreducible over its discriminant field exactly when the label is not 4T1.
• TauCeti.hasGaloisLabel_four_zero_iff, TauCeti.hasGaloisLabel_four_two_iff: the split of the last row, 4T1 for an irreducible quartic that becomes reducible over the discriminant field, and 4T3 for one in the last row that stays irreducible there.
• TauCeti.HasGaloisLabel.isAtom_adjoin_simple_iff_three_le: the field generated by a root has a proper intermediate field exactly for the labels 4T1, 4T2 and 4T3.

References

• K. Conrad, Galois groups of cubics and quartics (not in characteristic 2), §3.
• H. Cohen, A Course in Computational Algebraic Number Theory, §6.3.

theorem TauCeti.HasGaloisLabel.eq_of_four {F : Type u_1} [Field F] {f : Polynomial F} {j k : TransitiveGroupIndex 4} (hj : HasGaloisLabel f j) (hk : HasGaloisLabel f k) : j = k

A polynomial carries at most one label in degree four.

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

An irreducible separable quartic carries exactly one label, one of 4T1, …, 4T5.

theorem TauCeti.HasGaloisLabel.isAtom_adjoin_simple_iff_three_le {F : Type u_1} [Field F] {f : Polynomial F} {j : TransitiveGroupIndex 4} (h : HasGaloisLabel f j) (x : ↑(f.rootSet f.SplittingField)) : IsAtom F⟮↑x⟯ ↔ 3 ≤ ↑j

The field generated by a root of a quartic has a proper intermediate field exactly for the labels 4T1, 4T2 and 4T3. For a quartic f with a label and a root x in its splitting field, the simple extension F(x) is an atom among the intermediate fields of the splitting field, that is, F(x)/F has no intermediate field other than its two ends, exactly when the label is 4T4 or 4T5.

theorem TauCeti.HasGaloisLabel.exists_isRoot_specialize_quarticD4Spec_iff {F : Type u_1} [Field F] {f : Polynomial F} {j : TransitiveGroupIndex 4} (h : HasGaloisLabel f j) (hf : f.Monic) : (∃ (a : F), (quarticD4Spec.specialize F f).IsRoot a) ↔ ↑j ≤ 2

The resolvent cubic reads three of the five quartic labels. The resolvent cubic of a monic quartic with a label has a root in the base field exactly when that label is 4T1, 4T2 or 4T3, the labels whose reference subgroup lies in a conjugate of the dihedral group of 4T3.

The resolvent cubic of a separable quartic is separable, by TauCeti.separable_quarticD4Spec_specialize_iff, so no separation hypothesis appears.

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

The discriminant reads the parity of a quartic label. Away from characteristic 2, the discriminant of a monic quartic with a label is a square exactly when that label is 4T2 or 4T4.

theorem TauCeti.hasGaloisLabel_four_four_iff {F : Type u_1} [Field F] {f : Polynomial F} (hchar : ringChar F ≠ 2) (hf : f.Monic) : HasGaloisLabel f ⟨4, hasGaloisLabel_four_four_iff._proof_1⟩ ↔ Irreducible f ∧ f.natDegree = 4 ∧ ¬IsSquare f.discr ∧ Irreducible (quarticD4Spec.specialize F f)

A quartic with non-square discriminant and irreducible resolvent cubic has label 4T5. Away from characteristic 2, a monic polynomial has label 4T5, that is Galois group the full symmetric group on its four roots, exactly when it is an irreducible quartic whose discriminant is not a square and whose resolvent cubic is irreducible over the base field.

theorem TauCeti.hasGaloisLabel_four_three_iff {F : Type u_1} [Field F] {f : Polynomial F} (hchar : ringChar F ≠ 2) (hf : f.Monic) : HasGaloisLabel f ⟨3, hasGaloisLabel_four_three_iff._proof_1⟩ ↔ Irreducible f ∧ f.natDegree = 4 ∧ IsSquare f.discr ∧ Irreducible (quarticD4Spec.specialize F f)

A quartic with square discriminant and irreducible resolvent cubic has label 4T4. Away from characteristic 2, a monic polynomial has label 4T4, that is Galois group the alternating group on its four roots, exactly when it is an irreducible quartic whose discriminant is a square and whose resolvent cubic is irreducible over the base field.

theorem TauCeti.hasGaloisLabel_four_one_iff {F : Type u_1} [Field F] {f : Polynomial F} (hchar : ringChar F ≠ 2) (hf : f.Monic) : HasGaloisLabel f ⟨1, hasGaloisLabel_four_one_iff._proof_1⟩ ↔ Irreducible f ∧ f.natDegree = 4 ∧ IsSquare f.discr ∧ ∃ (a : F), (quarticD4Spec.specialize F f).IsRoot a

A quartic with square discriminant whose resolvent cubic has a root has label 4T2. Away from characteristic 2, a monic polynomial has label 4T2, that is Galois group the Klein four-group acting regularly on its four roots, exactly when it is an irreducible quartic whose discriminant is a square and whose resolvent cubic has a root in the base field.

theorem TauCeti.hasGaloisLabel_four_zero_or_two_iff {F : Type u_1} [Field F] {f : Polynomial F} (hchar : ringChar F ≠ 2) (hf : f.Monic) : HasGaloisLabel f ⟨0, hasGaloisLabel_four_zero_or_two_iff._proof_1⟩ ∨ HasGaloisLabel f ⟨2, hasGaloisLabel_four_zero_or_two_iff._proof_2⟩ ↔ Irreducible f ∧ f.natDegree = 4 ∧ ¬IsSquare f.discr ∧ ∃ (a : F), (quarticD4Spec.specialize F f).IsRoot a

A quartic with non-square discriminant whose resolvent cubic has a root has label 4T1 or 4T3. Away from characteristic 2, a monic polynomial has label 4T1 or 4T3, that is Galois group cyclic of order four or dihedral of order eight, exactly when it is an irreducible quartic whose discriminant is not a square and whose resolvent cubic has a root in the base field.

The discriminant and the resolvent cubic do not separate the two labels: both reference subgroups contain odd permutations and both lie in a dihedral group of order eight, so the two tests take the same values on them.

theorem TauCeti.hasGaloisLabel_four_one_iff_splits_resolvent {F : Type u_1} [Field F] {f : Polynomial F} (hchar : ringChar F ≠ 2) (hf : f.Monic) : HasGaloisLabel f ⟨1, hasGaloisLabel_four_one_iff._proof_1⟩ ↔ Irreducible f ∧ f.natDegree = 4 ∧ (quarticD4Spec.specialize F f).Splits

The split-resolvent row for 4T2. Away from characteristic 2, a monic polynomial has label 4T2 exactly when it is an irreducible quartic whose resolvent cubic splits completely over the base field. The square-discriminant condition follows from splitting.

theorem TauCeti.hasGaloisLabel_four_zero_or_two_iff_existsUnique_isRoot_resolvent {F : Type u_1} [Field F] {f : Polynomial F} (hchar : ringChar F ≠ 2) (hf : f.Monic) : HasGaloisLabel f ⟨0, hasGaloisLabel_four_zero_or_two_iff._proof_1⟩ ∨ HasGaloisLabel f ⟨2, hasGaloisLabel_four_zero_or_two_iff._proof_2⟩ ↔ Irreducible f ∧ f.natDegree = 4 ∧ ∃! a : F, (quarticD4Spec.specialize F f).IsRoot a

The unique-root row for 4T1 or 4T3. Away from characteristic 2, a monic polynomial has label 4T1 or 4T3 exactly when it is an irreducible quartic whose resolvent cubic has exactly one root in the base field. The non-square-discriminant condition follows from the uniqueness of the root.

Separating 4T1 from 4T3 over the discriminant field

theorem TauCeti.HasGaloisLabel.irreducible_map_discrField_iff_ne_zero {F : Type u_1} [Field F] {f : Polynomial F} {j : TransitiveGroupIndex 4} {E : Type u_2} [Field E] [Algebra F E] (h : HasGaloisLabel f j) (hf : f.Monic) (hchar : ringChar F ≠ 2) {δ : E} (hδ : δ ^ 2 = (algebraMap F E) f.discr) : Irreducible (Polynomial.map (algebraMap F ↥(discrField f E)) f) ↔ j ≠ ⟨0, hasGaloisLabel_four_zero_or_two_iff._proof_1⟩

The discriminant field detects the cyclic quartic label. Away from characteristic 2, a monic quartic with a label stays irreducible over its discriminant field exactly when that label is not 4T1. The discriminant field may be taken in any extension E containing a square root δ of the discriminant.

theorem TauCeti.hasGaloisLabel_four_zero_iff {F : Type u_1} [Field F] {f : Polynomial F} (hchar : ringChar F ≠ 2) (hf : f.Monic) {E : Type u_2} [Field E] [Algebra F E] {δ : E} (hδ : δ ^ 2 = (algebraMap F E) f.discr) : HasGaloisLabel f ⟨0, hasGaloisLabel_four_zero_or_two_iff._proof_1⟩ ↔ Irreducible f ∧ f.natDegree = 4 ∧ ¬Irreducible (Polynomial.map (algebraMap F ↥(discrField f E)) f)

An irreducible quartic that factors over its discriminant field has label 4T1. Away from characteristic 2, a monic polynomial has label 4T1, that is cyclic Galois group of order four, exactly when it is an irreducible quartic that becomes reducible over its discriminant field. The discriminant field may be taken in any extension E containing a square root δ of the discriminant.

The conditions of the last row of the decision table, a non-square discriminant and a root of the resolvent cubic, follow from reducibility over the discriminant field and need not be stated.

theorem TauCeti.hasGaloisLabel_four_two_iff {F : Type u_1} [Field F] {f : Polynomial F} (hchar : ringChar F ≠ 2) (hf : f.Monic) {E : Type u_2} [Field E] [Algebra F E] {δ : E} (hδ : δ ^ 2 = (algebraMap F E) f.discr) : HasGaloisLabel f ⟨2, hasGaloisLabel_four_zero_or_two_iff._proof_2⟩ ↔ Irreducible f ∧ f.natDegree = 4 ∧ ¬IsSquare f.discr ∧ (∃ (a : F), (quarticD4Spec.specialize F f).IsRoot a) ∧ Irreducible (Polynomial.map (algebraMap F ↥(discrField f E)) f)

A quartic in the last row that stays irreducible over its discriminant field has label 4T3. Away from characteristic 2, a monic polynomial has label 4T3, that is dihedral Galois group of order eight, exactly when it is an irreducible quartic whose discriminant is not a square, whose resolvent cubic has a root in the base field, and which stays irreducible over its discriminant field. The discriminant field may be taken in any extension E containing a square root δ of the discriminant.

Together with TauCeti.hasGaloisLabel_four_zero_iff this splits the row TauCeti.hasGaloisLabel_four_zero_or_two_iff of the decision table.