Double transitivity of polynomial Galois groups

For an irreducible separable polynomial p and a root x, the other roots form the roots of p / (X - x) over the simple extension generated by x. The point stabilizer is the Galois group over that simple extension, so transitivity on the other roots is equivalent to irreducibility of the quotient. This identifies double transitivity of the original root action with that irreducibility criterion.

Main result

• TauCeti.is_two_pretransitive_iff_irreducible_divByMonic: the root action is doubly pretransitive exactly when the quotient by the chosen root remains irreducible over the field generated by that root.

theorem TauCeti.is_two_pretransitive_iff_irreducible_divByMonic {F : Type u} [Field F] {p : Polynomial F} (hp : Irreducible p) (hsep : p.Separable) (hdeg : 1 < p.natDegree) (x : ↑(p.rootSet p.SplittingField)) : MulAction.IsMultiplyPretransitive p.Gal (↑(p.rootSet p.SplittingField)) 2 ↔ Irreducible (Polynomial.map (algebraMap F ↥F⟮↑x⟯) p /ₘ (Polynomial.X - Polynomial.C (IntermediateField.AdjoinSimple.gen F ↑x)))

Double transitivity of a polynomial Galois group is irreducibility over a root field. For an irreducible separable polynomial of degree at least two, the Galois action on its roots is doubly pretransitive exactly when, after adjoining a chosen root x, the quotient p / (X - x) remains irreducible.

The quotient is formed after mapping p to F⟮x⟯; the removed linear factor is X - C (IntermediateField.AdjoinSimple.gen F x).