Jordan's theorem for a prime cycle: the bound is sharp

Jordan's theorem TauCeti.alternatingGroup_le_of_isPreprimitive_of_isCycle_mem says that a primitive permutation group of degree n containing a cycle of prime length p, with p + 3 ≤ n, contains the alternating group. This file shows that the bound cannot be weakened to p ≤ n or to p + 1 ≤ n. The witnesses are affine groups AGL(1, q) acting on q points: they are primitive, too small to contain the alternating group once q ≥ 5, and yet contain long cycles.

• AGL(1, 5) is primitive of degree 5 and contains a 5-cycle.
• AGL(1, 8) is primitive of degree 8 and contains a 7-cycle.

Main results

• TauCeti.not_forall_alternatingGroup_le_of_isPreprimitive_of_isCycle_mem_of_card_support_eq: Jordan's theorem fails for a cycle of prime length p in degree p.
• Jordan's theorem fails for a cycle of prime length p in degree p + 1: TauCeti.not_forall_alternatingGroup_le_of_isPreprimitive_of_isCycle_mem_of_card_support_add_one_eq

References

• H. Wielandt, Finite Permutation Groups, §13.
• J. D. Dixon and B. Mortimer, Permutation Groups, §3.3 and §7.7.

theorem TauCeti.not_forall_alternatingGroup_le_of_isPreprimitive_of_isCycle_mem_of_card_support_eq : ¬∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] (G : Subgroup (Equiv.Perm α)), MulAction.IsPreprimitive (↥G) α → ∀ g ∈ G, g.IsCycle → Nat.Prime g.support.card → g.support.card = Nat.card α → alternatingGroup α ≤ G

Jordan's theorem fails in degree p. A primitive permutation group of degree n containing a cycle of prime length p need not contain the alternating group when p = n: the affine group AGL(1, 5) is primitive on five points and contains a 5-cycle. This shows that the bound p + 3 ≤ n of TauCeti.alternatingGroup_le_of_isPreprimitive_of_isCycle_mem cannot be weakened to p ≤ n.

theorem TauCeti.not_forall_alternatingGroup_le_of_isPreprimitive_of_isCycle_mem_of_card_support_add_one_eq : ¬∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] (G : Subgroup (Equiv.Perm α)), MulAction.IsPreprimitive (↥G) α → ∀ g ∈ G, g.IsCycle → Nat.Prime g.support.card → g.support.card + 1 = Nat.card α → alternatingGroup α ≤ G

Jordan's theorem fails in degree p + 1. A primitive permutation group of degree n containing a cycle of prime length p need not contain the alternating group when p + 1 = n: the affine group AGL(1, 8) of the field with eight elements is primitive on eight points and contains a 7-cycle. This shows that the bound p + 3 ≤ n of TauCeti.alternatingGroup_le_of_isPreprimitive_of_isCycle_mem cannot be weakened to p + 1 ≤ n.