Transitivity of the even part of a quartic permutation group

Intersecting a transitive subgroup of S₄ with A₄ distinguishes the cyclic group 4T1 from the dihedral group 4T3. This is the permutation step in the test using the discriminant quadratic field: its fixing subgroup is the even part of the Galois group, and irreducibility over that field is equivalent to transitivity of that subgroup on the four roots.

The cyclic group's even part cannot be transitive: the cyclic group has order four but contains odd permutations. The even part of the dihedral group contains the Klein four-group, which acts regularly on four points.

theorem TauCeti.not_isPretransitive_referenceSubgroup_four_zero_inf_alternatingGroup : ¬MulAction.IsPretransitive (↥(referenceSubgroup 4 ⟨0, not_isPretransitive_referenceSubgroup_four_zero_inf_alternatingGroup._proof_1⟩ ⊓ alternatingGroup (Fin 4))) (Fin 4)

The even part of the cyclic quartic reference group is not transitive.

theorem TauCeti.isPretransitive_referenceSubgroup_four_two_inf_alternatingGroup : MulAction.IsPretransitive (↥(referenceSubgroup 4 ⟨2, isPretransitive_referenceSubgroup_four_two_inf_alternatingGroup._proof_1⟩ ⊓ alternatingGroup (Fin 4))) (Fin 4)

The even part of the dihedral quartic reference group is transitive.

theorem TauCeti.TransitiveGroupLabel.isPretransitive_inf_alternatingGroup_iff_ne_zero {j : TransitiveGroupIndex 4} {G : Subgroup (Equiv.Perm (Fin 4))} (h : TransitiveGroupLabel j G) : MulAction.IsPretransitive (↥(G ⊓ alternatingGroup (Fin 4))) (Fin 4) ↔ j ≠ ⟨0, not_isPretransitive_referenceSubgroup_four_zero_inf_alternatingGroup._proof_1⟩

The even part of a transitive quartic permutation group is transitive exactly when the group is not the cyclic group 4T1. In particular, this separates the cyclic and dihedral groups.