Non-examples: inseparable and reducible polynomials #

Three polynomials test that the permutation picture of a Galois group excludes what it should.

(X² - 2)² is not separable, so it has no transitive-group label (TauCeti.not_hasGaloisLabel_of_not_separable) and does not have full symmetric Galois group (Polynomial.not_hasFullSymmetricGaloisGroup_pow_of_not_isUnit). It is also reducible, yet its Galois group acts transitively on its two distinct roots. It is therefore the witness that separability cannot be dropped from TauCeti.isPretransitive_iff_irreducible.
(X² - 2)(X² - 3) is separable and reducible. Over ℚ its Galois group is the Klein four-group V₄. It acts on the four roots with two orbits, each of size two: the roots of X² - 2 and the roots of X² - 3. Being reducible, the polynomial carries no transitive-group label.
X⁵ + X + 1 = (X² + X + 1)(X³ - X² + 1) is a reducible quintic, so no label 5Tj is attached to it.

The Galois group of (X² - 2)(X² - 3) comes from the multiquadratic theory: TauCeti.Multiquadratic.nonempty_mulEquiv_gal_definingPolynomial identifies it with (ℤ/2)², because 2, 3 and 6 are not squares in ℚ.

Main results #

TauCeti.isPretransitive_gal_X_sq_sub_two_sq: the Galois group of the reducible polynomial (X² - 2)² acts transitively on its roots.
TauCeti.isKleinFour_gal_X_sq_sub_two_mul_X_sq_sub_three: the Galois group of (X² - 2)(X² - 3) over ℚ is a Klein four-group.
TauCeti.natCard_orbit_X_sq_sub_two_mul_X_sq_sub_three and TauCeti.natCard_orbitQuotient_X_sq_sub_two_mul_X_sq_sub_three: its root action has two orbits, each of size two.
TauCeti.not_hasGaloisLabel_X_sq_sub_two_mul_X_sq_sub_three and TauCeti.not_hasGaloisLabel_X_pow_five_add_X_add_one: neither polynomial has a label.

References #

LMFDB, Galois group labels, https://www.lmfdb.org/GaloisGroup/.

`(X² - 2)²`: transitive but reducible #

source

theorem TauCeti.not_separable_X_sq_sub_two_sq {F : Type u_1} [Field F] :

¬((Polynomial.X ^ 2 - 2) ^ 2).Separable

(X² - 2)² is not separable, over any field.

source

theorem TauCeti.not_irreducible_X_sq_sub_two_sq {F : Type u_1} [Field F] :

¬Irreducible ((Polynomial.X ^ 2 - 2) ^ 2)

(X² - 2)² is reducible, over any field.

source

theorem TauCeti.isPretransitive_gal_X_sq_sub_two_sq :

MulAction.IsPretransitive ((Polynomial.X ^ 2 - 2) ^ 2).Gal ↑(((Polynomial.X ^ 2 - 2) ^ 2).rootSet ((Polynomial.X ^ 2 - 2) ^ 2).SplittingField)

The Galois group of the reducible polynomial (X² - 2)² over ℚ acts transitively on its roots. Its two distinct roots ±√2 are the roots of the irreducible X² - 2. Together with TauCeti.not_irreducible_X_sq_sub_two_sq, this shows that separability cannot be dropped from TauCeti.isPretransitive_iff_irreducible.

`(X² - 2)(X² - 3)`: separable and reducible, with group `V₄` #

source

theorem TauCeti.separable_X_sq_sub_two_mul_X_sq_sub_three {F : Type u_1} [Field F] [CharZero F] :

((Polynomial.X ^ 2 - 2) * (Polynomial.X ^ 2 - 3)).Separable

(X² - 2)(X² - 3) is separable over every field of characteristic zero.

source

theorem TauCeti.not_irreducible_X_sq_sub_two_mul_X_sq_sub_three {F : Type u_1} [Field F] :

¬Irreducible ((Polynomial.X ^ 2 - 2) * (Polynomial.X ^ 2 - 3))

(X² - 2)(X² - 3) is reducible, over any field.

source

theorem TauCeti.isKleinFour_gal_X_sq_sub_two_mul_X_sq_sub_three :

IsKleinFour ((Polynomial.X ^ 2 - 2) * (Polynomial.X ^ 2 - 3)).Gal

The Galois group of (X² - 2)(X² - 3) over ℚ is the Klein four-group. The splitting field is ℚ(√2, √3), and the radicands 2 and 3 are square-class independent: none of 2, 3 and 6 is a square in ℚ.

source

theorem TauCeti.natCard_orbit_X_sq_sub_two_mul_X_sq_sub_three (E : Type u_2) [Field E] [Algebra ℚ E] [Fact (Polynomial.map (algebraMap ℚ E) ((Polynomial.X ^ 2 - 2) * (Polynomial.X ^ 2 - 3))).Splits] (x : ↑(((Polynomial.X ^ 2 - 2) * (Polynomial.X ^ 2 - 3)).rootSet E)) :

Nat.card ↑(MulAction.orbit ((Polynomial.X ^ 2 - 2) * (Polynomial.X ^ 2 - 3)).Gal x) = 2

Each Galois orbit on the roots of (X² - 2)(X² - 3) has two elements: the orbit of a root is the pair of roots of its irreducible factor X² - 2 or X² - 3.

source