Jordan's theorem for a cycle of prime length

A primitive permutation group of degree n that contains a cycle of prime length p, with p + 3 ≤ n, contains the alternating group. This is Jordan's theorem of 1873, the analogue for cycles of arbitrary prime length of Mathlib's Equiv.Perm.subgroup_eq_top_of_isPreprimitive_of_isSwap_mem and Equiv.Perm.alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem, which need no bound on the degree. The bound p + 3 ≤ n cannot be weakened to p ≤ n or p + 1 ≤ n: the affine group AGL(1, 5) is primitive of degree 5 and contains a 5-cycle, and AGL(1, 8) is primitive of degree 8 and contains a 7-cycle. Neither contains the alternating group. These two witnesses are proved in TauCeti.GroupTheory.Perm.Jordan.Counterexamples.

Main results

• TauCeti.isMultiplyPreprimitive_of_isCycle_mem: a primitive group containing a cycle of prime length whose complement of the support has k points is (k + 1)-fold primitive.
• TauCeti.exists_eqOn_compl_support_mul_mul_inv_mem_zpowers: the Frattini step for an element preserving the support of a cycle of prime length.
• TauCeti.alternatingGroup_le_of_isPreprimitive_of_isCycle_mem: Jordan's theorem, a primitive permutation group of degree at least p + 3 containing a p-cycle for a prime p contains the alternating group.

References

• H. Wielandt, Finite Permutation Groups, Theorem 13.9, with the Sylow argument of Theorem 9.4.
• J. D. Dixon and B. Mortimer, Permutation Groups, Theorem 3.3E.
• Mathlib's Mathlib/GroupTheory/GroupAction/Jordan.lean, by Antoine Chambert-Loir, for the related transposition and 3-cycle results.

theorem TauCeti.isMultiplyPreprimitive_of_isCycle_mem {α : Type u_1} [Fintype α] [DecidableEq α] {G : Subgroup (Equiv.Perm α)} (hG : MulAction.IsPreprimitive (↥G) α) {g : Equiv.Perm α} (hgc : g.IsCycle) (hgp : Nat.Prime g.support.card) (hg : g ∈ G) : MulAction.IsMultiplyPreprimitive (↥G) α (g.supportᶜ.card + 1)

Jordan's multiple primitivity for a cycle of prime length. A primitive permutation group containing a cycle g of prime length is (k + 1)-fold primitive, where k is the number of fixed points of g.

theorem TauCeti.exists_eqOn_compl_support_mul_mul_inv_mem_zpowers {α : Type u_1} [Fintype α] [DecidableEq α] {G : Subgroup (Equiv.Perm α)} {g x : Equiv.Perm α} (hgc : g.IsCycle) (hgp : Nat.Prime g.support.card) (hg : g ∈ G) (hx : x ∈ G) (hxs : ∀ (z : α), x z ∈ g.support ↔ z ∈ g.support) : ∃ n ∈ G, (∀ z ∉ g.support, n z = x z) ∧ n * g * n⁻¹ ∈ Subgroup.zpowers g

The Frattini step: if x ∈ G preserves the support of a cycle g ∈ G of prime length, then x can be corrected by an element of G supported on the support of g so that it normalizes ⟨g⟩. The subgroup of G supported on the support of g has ⟨g⟩ as a Sylow subgroup.

theorem TauCeti.alternatingGroup_le_of_isPreprimitive_of_isCycle_mem {α : Type u_1} [Fintype α] [DecidableEq α] {G : Subgroup (Equiv.Perm α)} (hG : MulAction.IsPreprimitive (↥G) α) {p : ℕ} (hp : Nat.Prime p) (hp' : p + 3 ≤ Nat.card α) {g : Equiv.Perm α} (hgc : g.IsCycle) (hgp : g.support.card = p) (hg : g ∈ G) : alternatingGroup α ≤ G

Jordan's theorem for a cycle of prime length (Wielandt, Theorem 13.9). A primitive permutation group of degree at least p + 3 that contains a cycle of prime length p contains the alternating group.