Theorems of Jordan

A proof of theorems of Jordan regarding primitive permutation groups.

This mostly follows the book Wielandt, Finite permutation groups.

• MulAction.IsPreprimitive.is_two_pretransitive and MulAction.IsPreprimitive.is_two_preprimitive are technical lemmas that prove 2-pretransitivity / 2-preprimitivity for some group primitive actions given the transitivity / primitivity of ofFixingSubgroup G s (Wielandt, 13.1)

• MulAction.IsPreprimitive.isMultiplyPreprimitive: A multiple preprimitivity criterion of Jordan (1871) for a preprimitive action: the hypothesis is the preprimitivity of the SubMulAction of fixingSubgroup s on ofFixingSubgroup G s (Wielandt, 13.2)

• Equiv.Perm.eq_top_of_isPreprimitive_of_isSwap_mem : a primitive subgroup of a permutation group that contains a swap is equal to the full permutation group (Wielandt, 13.3)

• Equiv.Perm.alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem : a primitive subgroup of a permutation group that contains a 3-cycle contains the alternating group (Wielandt, 13.3)

TODO

• Prove Equiv.Perm.alternatingGroup_le_of_isPreprimitive_of_isCycle_mem: a primitive subgroup of a permutation group that contains a cycle of prime order contains the alternating group (Wielandt, 13.9).

• Prove the stronger versions of the technical lemmas of Jordan (Wielandt, 13.1').

theorem normalClosure_of_stabilizer_eq_top {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (hsn' : 2 < ENat.card α) (hG' : MulAction.IsMultiplyPretransitive G α 2) {a : α} : Subgroup.normalClosure ↑(MulAction.stabilizer G a) = ⊤

In a 2-transitive action, the normal closure of stabilizers is the full group.

theorem MulAction.IsPreprimitive.is_two_motive_of_is_motive {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (hG : IsPreprimitive G α) {s : Set α} {n : ℕ} (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α) : (IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧ (IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)

Simultaneously prove MulAction.IsPreprimitive.is_two_pretransitive and MulAction.IsPreprimitive.is_two_preprimitive.

theorem MulAction.IsPreprimitive.is_two_pretransitive {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (hG : IsPreprimitive G α) {s : Set α} {n : ℕ} (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α) (hs_trans : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)) : IsMultiplyPretransitive G α 2

A criterion due to Jordan for being 2-pretransitive (Wielandt, 13.1)

theorem MulAction.IsPreprimitive.is_two_preprimitive {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (hG : IsPreprimitive G α) {s : Set α} {n : ℕ} (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α) (hs_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)) : IsMultiplyPreprimitive G α 2

A criterion due to Jordan for being 2-preprimitive (Wielandt, 13.1)

theorem MulAction.IsPreprimitive.isMultiplyPreprimitive {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (hG : IsPreprimitive G α) {s : Set α} {n : ℕ} (hsn : s.ncard = n + 1) (hsn' : n + 2 < Nat.card α) (hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)) : IsMultiplyPreprimitive G α (n + 2)

Jordan's multiple primitivity criterion (Wielandt, 13.3)

theorem Equiv.Perm.subgroup_eq_top_of_nontrivial {α : Type u_1} {G : Subgroup (Perm α)} [Finite α] (hα : Nat.card α ≤ 2) (hG : Nontrivial ↥G) : G = ⊤

theorem Equiv.Perm.isMultiplyPretransitive_of_nontrivial {α : Type u_1} {K : Type u_2} [Group K] [MulAction K α] (hα : Nat.card α = 2) (hK : MulAction.fixedPoints K α ≠ _root_.Set.univ) (n : ℕ) : MulAction.IsMultiplyPretransitive K α n

theorem Equiv.Perm.isPretransitive_of_isCycle_mem {α : Type u_1} {G : Subgroup (Perm α)} [Fintype α] [DecidableEq α] {g : Perm α} (hgc : g.IsCycle) (hg : g ∈ G) : MulAction.IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(SubMulAction.ofFixingSubgroup (↥G) (↑g.support)ᶜ)

theorem Equiv.Perm.eq_top_of_isPreprimitive_of_isSwap_mem {α : Type u_1} {G : Subgroup (Perm α)} [Fintype α] [DecidableEq α] (hG : MulAction.IsPreprimitive (↥G) α) (g : Perm α) (h2g : g.IsSwap) (hg : g ∈ G) : G = ⊤

A primitive subgroup of Equiv.Perm α that contains a swap is the full permutation group (Jordan).

theorem Equiv.Perm.alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem {α : Type u_1} {G : Subgroup (Perm α)} [Fintype α] [DecidableEq α] (hG : MulAction.IsPreprimitive (↥G) α) {g : Perm α} (h3g : g.IsThreeCycle) (hg : g ∈ G) : alternatingGroup α ≤ G

A primitive subgroup of Equiv.Perm α that contains a 3-cycle contains the alternating group (Jordan).