The Galois group of a cubic

An irreducible separable cubic has transitive Galois image in Equiv.Perm (Fin 3), and the only transitive subgroups of the symmetric group on three points are the alternating group A₃, the reference subgroup of the label 3T1, and the whole group S₃, that of 3T2. So such a cubic carries exactly one label, and which one is decided by parity: away from characteristic 2 the Galois image lies in the alternating group exactly when the discriminant is a square. The discriminant therefore determines the Galois group of an irreducible separable cubic on its own: the label is 3T1 when f.discr is a square and 3T2 when it is not.

The two classical examples over ℚ are computed in full. The cubic X³ - 3X - 1 has discriminant 81 = 9², so its Galois group is cyclic of order three; the cubic X³ - 2 has discriminant -108, which is not a square in ℚ since it is negative, so its Galois group is S₃, of order six. Irreducibility over ℚ is checked by the integral root theorem and a reduction modulo a small prime.

Main results

• TauCeti.existsUnique_hasGaloisLabel_three: an irreducible separable cubic carries exactly one label.
• TauCeti.hasGaloisLabel_three_zero_iff, TauCeti.hasGaloisLabel_three_one_iff: the discriminant decides the label of a cubic, 3T1 for a square discriminant and 3T2 otherwise.
• TauCeti.hasGaloisLabel_X_pow_three_sub_three_mul_X_sub_one: X³ - 3X - 1 over ℚ has label 3T1, and TauCeti.natCard_gal_X_pow_three_sub_three_mul_X_sub_one: its Galois group has order 3.
• TauCeti.hasGaloisLabel_X_pow_three_sub_two: X³ - 2 over ℚ has label 3T2, and TauCeti.natCard_gal_X_pow_three_sub_two: its Galois group has order 6.

References

• K. Conrad, Galois groups of cubics and quartics (not in characteristic 2), Theorem 2.3 and Examples 2.4–2.5.
• LMFDB, number fields 3.3.81.1 and 3.1.108.1.

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

A polynomial carries at most one label in degree three.

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

An irreducible separable cubic carries exactly one label, 3T1 or 3T2.

theorem TauCeti.hasGaloisLabel_three_zero_iff {F : Type u_1} [Field F] {f : Polynomial F} (hchar : ringChar F ≠ 2) : HasGaloisLabel f ⟨0, hasGaloisLabel_three_zero_iff._proof_1⟩ ↔ f.Separable ∧ Irreducible f ∧ f.natDegree = 3 ∧ IsSquare f.discr

A cubic with square discriminant has label 3T1. Away from characteristic 2, a polynomial has label 3T1, that is Galois group cyclic of order three acting on its roots, exactly when it is a separable irreducible cubic whose discriminant is a square.

theorem TauCeti.hasGaloisLabel_three_one_iff {F : Type u_1} [Field F] {f : Polynomial F} (hchar : ringChar F ≠ 2) : HasGaloisLabel f ⟨1, hasGaloisLabel_three_one_iff._proof_1⟩ ↔ Irreducible f ∧ f.natDegree = 3 ∧ ¬IsSquare f.discr

A cubic with non-square discriminant has label 3T2. Away from characteristic 2, a polynomial has label 3T2, that is Galois group the full symmetric group on its three roots, exactly when it is an irreducible cubic whose discriminant is not a square.

Two cubics over ℚ

theorem TauCeti.discr_X_pow_three_sub_three_mul_X_sub_one : (Polynomial.X ^ 3 - 3 * Polynomial.X - 1).discr = 81

The discriminant of X³ - 3X - 1 is 81.

theorem TauCeti.discr_X_pow_three_sub_two : (Polynomial.X ^ 3 - 2).discr = -108

The discriminant of X³ - 2 is -108.

theorem TauCeti.irreducible_X_pow_three_sub_three_mul_X_sub_one : Irreducible (Polynomial.X ^ 3 - 3 * Polynomial.X - 1)

X³ - 3X - 1 is irreducible over ℚ: it has no root modulo 2, so no integral root.

theorem TauCeti.irreducible_X_pow_three_sub_two : Irreducible (Polynomial.X ^ 3 - 2)

X³ - 2 is irreducible over ℚ: it has no root modulo 7, so no integral root.

theorem TauCeti.hasGaloisLabel_X_pow_three_sub_three_mul_X_sub_one : HasGaloisLabel (Polynomial.X ^ 3 - 3 * Polynomial.X - 1) ⟨0, hasGaloisLabel_three_zero_iff._proof_1⟩

X³ - 3X - 1 has label 3T1: its Galois group over ℚ is cyclic of order three.

theorem TauCeti.hasGaloisLabel_X_pow_three_sub_two : HasGaloisLabel (Polynomial.X ^ 3 - 2) ⟨1, hasGaloisLabel_three_one_iff._proof_1⟩

X³ - 2 has label 3T2: its Galois group over ℚ is the symmetric group on its three roots. The discriminant -108 is negative, hence not a square.

theorem TauCeti.natCard_gal_X_pow_three_sub_three_mul_X_sub_one : Nat.card (Polynomial.X ^ 3 - 3 * Polynomial.X - 1).Gal = 3

The Galois group of X³ - 3X - 1 over ℚ has order 3.

theorem TauCeti.natCard_gal_X_pow_three_sub_two : Nat.card (Polynomial.X ^ 3 - 2).Gal = 6

The Galois group of X³ - 2 over ℚ has order 6.