Long cycles and transitivity

A permutation group containing a cycle on all points is transitive, and a transitive permutation group containing a cycle on all but one point is doubly transitive. In the second case, the missing point is the unique fixed point of the cycle. Its stabilizer contains the cycle and is therefore transitive on the complement; the usual point-stabilizer criterion then gives double transitivity of the original action.

Main results

• TauCeti.isPretransitive_of_isCycle_mem_of_support_eq_univ: a permutation group containing a cycle with full support is transitive.
• TauCeti.card_support_add_one_eq_card_iff_existsUnique_fixedPoint: a permutation moves all but one point exactly when it has a unique fixed point.
• TauCeti.is_two_pretransitive_of_isCycle_mem_of_existsUnique_fixedPoint: a transitive permutation group containing a cycle with a unique fixed point is doubly transitive.
• TauCeti.isPreprimitive_of_isCycle_mem_of_existsUnique_fixedPoint: such a group is primitive.
• TauCeti.is_two_pretransitive_of_isCycle_mem_of_card_support_add_one_eq_card: a transitive finite permutation group that contains a cycle moving all but one point is doubly transitive.
• TauCeti.isPreprimitive_of_isCycle_mem_of_card_support_add_one_eq_card: such a group is primitive.

These results are part of the generic recognition package in Layer 1 of TauCetiRoadmap/PolynomialGaloisGroups/README.md, which supports both the degree-at-most-five classification and Layer 9. The long-cycle criterion is used specifically in Layer 9's three-prime construction of polynomials with full symmetric Galois group.

References

• J. D. Dixon and B. Mortimer, Permutation Groups, §2.1.
• H. Wielandt, Finite Permutation Groups, Chapter II.

The point-stabilizer step is adapted from Mathlib/GroupTheory/GroupAction/Jordan.lean, by Antoine Chambert-Loir; the cycle-transitivity argument generalizes that file's Equiv.Perm.isPretransitive_of_isCycle_mem from finite support to a unique fixed point.

theorem TauCeti.is_two_pretransitive_of_isCycle_mem_of_existsUnique_fixedPoint {α : Type u_1} (G : Subgroup (Equiv.Perm α)) [MulAction.IsPretransitive (↥G) α] {σ : Equiv.Perm α} (hσ : σ.IsCycle) (hσG : σ ∈ G) (hfix : ∃! x : α, σ x = x) : MulAction.IsMultiplyPretransitive (↥G) α 2

A transitive permutation group containing a cycle with a unique fixed point is doubly transitive.

theorem TauCeti.isPreprimitive_of_isCycle_mem_of_existsUnique_fixedPoint {α : Type u_1} (G : Subgroup (Equiv.Perm α)) [MulAction.IsPretransitive (↥G) α] {σ : Equiv.Perm α} (hσ : σ.IsCycle) (hσG : σ ∈ G) (hfix : ∃! x : α, σ x = x) : MulAction.IsPreprimitive (↥G) α

A transitive permutation group containing a cycle with a unique fixed point is primitive.

theorem TauCeti.isPretransitive_of_isCycle_mem_of_support_eq_univ {α : Type u_1} [Fintype α] [DecidableEq α] {G : Subgroup (Equiv.Perm α)} {g : Equiv.Perm α} (hgc : g.IsCycle) (hg : g ∈ G) (hsupp : g.support = Finset.univ) : MulAction.IsPretransitive (↥G) α

A permutation subgroup containing a cycle with full support acts transitively.

theorem TauCeti.is_two_pretransitive_of_isCycle_mem_of_card_support_add_one_eq_card {α : Type u_1} [Fintype α] [DecidableEq α] (G : Subgroup (Equiv.Perm α)) [MulAction.IsPretransitive (↥G) α] {σ : Equiv.Perm α} (hσ : σ.IsCycle) (hσG : σ ∈ G) (hcard : σ.support.card + 1 = Fintype.card α) : MulAction.IsMultiplyPretransitive (↥G) α 2

A transitive subgroup of a finite symmetric group that contains a cycle moving all but one point is doubly transitive.

theorem TauCeti.isPreprimitive_of_isCycle_mem_of_card_support_add_one_eq_card {α : Type u_1} [Fintype α] [DecidableEq α] (G : Subgroup (Equiv.Perm α)) [MulAction.IsPretransitive (↥G) α] {σ : Equiv.Perm α} (hσ : σ.IsCycle) (hσG : σ ∈ G) (hcard : σ.support.card + 1 = Fintype.card α) : MulAction.IsPreprimitive (↥G) α

A transitive subgroup of a finite symmetric group that contains a cycle moving all but one point is primitive.