Maximal subgroups of the symmetric groups

• Equiv.Perm.isCoatom_stabilizer: if neither s : Set α nor its complementary subset is empty, and the cardinality of s is not half of that of α, then MulAction.stabilizer (Equiv.Perm α) s is a maximal subgroup of the symmetric group Equiv.Perm α.

  This is the intransitive case of the O'Nan-Scott classification.

TODO

• Application to primitivity of the action of Equiv.Perm α on finite combinations of α.

• Formalize the other cases of the classification. The next one should be the imprimitive case.

Reference

The argument is taken from [M. Liebeck, C. Praeger, J. Saxl, A classification of the maximal subgroups of the finite alternating and symmetric groups, 1987][LiebeckPraegerSaxl-1987].

theorem MulAction.isPreprimitive_stabilizer_of_surjective {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] (s : Set α) (hs : Function.Surjective toPerm) : IsPreprimitive ↥(stabilizer M s) ↑s

In the permutation group, the stabilizer of any set acts primitively on that set.

theorem MulAction.isPreprimitive_stabilizer_subgroup {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s : Set α} [IsPreprimitive ↥(stabilizer M s) ↑s] {G : Subgroup M} (hG : stabilizer M s ≤ G) : IsPreprimitive ↥(stabilizer (↥G) s) ↑s

A (mostly trivial) primitivity criterion for stabilizers.

theorem MulAction.IsPretransitive.of_partition {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s : Set α} (hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), g • a = b) (hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ (g : M), g • a = b) (hM : stabilizer M s ≠ ⊤) : IsPretransitive M α

theorem Equiv.Perm.ofSubtype_mem_stabilizer {α : Type u_2} {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (g : Perm ↑s) : ofSubtype g ∈ MulAction.stabilizer (Perm α) s

theorem Equiv.Perm.swap_mem_stabilizer {α : Type u_2} [DecidableEq α] {a b : α} {s : Set α} (ha : a ∈ s) (hb : b ∈ s) : swap a b ∈ MulAction.stabilizer (Perm α) s

theorem Equiv.Perm.exists_mem_stabilizer_smul_eq {α : Type u_2} {s : Set α} (a : α) : a ∈ s → ∀ b ∈ s, ∃ g ∈ MulAction.stabilizer (Perm α) s, g • a = b

theorem Equiv.Perm.stabilizer.surjective_toPerm {α : Type u_2} (s : Set α) : Function.Surjective MulAction.toPerm

instance Equiv.Perm.stabilizer_isPreprimitive {α : Type u_2} (s : Set α) : MulAction.IsPreprimitive ↥(MulAction.stabilizer (Perm α) s) ↑s

In the permutation group, the stabilizer of a set acts primitively on that set.

theorem Equiv.Perm.stabilizer_ne_top_of_nonempty_of_nonempty_compl {α : Type u_2} {s : Set α} (hs : s.Nonempty) (hsc : sᶜ.Nonempty) : MulAction.stabilizer (Perm α) s ≠ ⊤

theorem Equiv.Perm.has_swap_mem_of_lt_stabilizer {α : Type u_2} [DecidableEq α] (s : Set α) (G : Subgroup (Perm α)) (hG : MulAction.stabilizer (Perm α) s < G) : ∃ (g : Perm α), g.IsSwap ∧ g ∈ G

theorem Subgroup.isPretransitive_of_stabilizer_lt {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s : Set α} {G : Subgroup M} (hG : MulAction.stabilizer M s < G) (moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ MulAction.stabilizer M s, g • a = b) : MulAction.IsPretransitive (↥G) α

theorem MulAction.IsBlock.subsingleton_of_ssubset_of_stabilizer_le {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s B : Set α} (hB_ss_sc : B ⊂ s) (hB : IsBlock M B) (hG : Function.Surjective toPerm) : B.Subsingleton

theorem MulAction.IsBlock.subsingleton_of_ssubset_of_stabilizer_Perm_le {α : Type u_2} {s B : Set α} {G : Subgroup (Equiv.Perm α)} (hB : IsBlock (↥G) B) (hB_ss_sc : B ⊂ s) (hG : stabilizer (Equiv.Perm α) s ≤ G) : B.Subsingleton

theorem MulAction.IsBlock.subsingleton_of_stabilizer_lt_of_subset {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s B : Set α} {G : Subgroup M} [IsPreprimitive ↥(stabilizer (↥G) s) ↑s] (hB : IsBlock (↥G) B) (hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton) (hG : stabilizer M s < G) (hBs : B ⊆ s) : B.Subsingleton

theorem MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s : Set α} [Finite α] [IsMultiplyPretransitive M α (s.ncard + 1)] {G : Subgroup M} (hG : stabilizer M s ≤ G) {B : Set α} (hBs : ¬B ⊆ s) (hBsc : ¬B ⊆ sᶜ) (hB : IsBlock (↥G) B) : sᶜ ⊆ B

theorem Equiv.Perm.isCoatom_stabilizer_of_ncard_lt_ncard_compl {α : Type u_2} [Finite α] {s : Set α} (h0 : s.Nonempty) (hα : s.ncard < sᶜ.ncard) : IsCoatom (MulAction.stabilizer (Perm α) s)

theorem Equiv.Perm.isCoatom_stabilizer {α : Type u_2} [Finite α] {s : Set α} (hs_nonempty : s.Nonempty) (hsc_nonempty : sᶜ.Nonempty) (hα : Nat.card α ≠ 2 * s.ncard) : IsCoatom (MulAction.stabilizer (Perm α) s)

MulAction.stabilizer (Perm α) s is a maximal subgroup of Perm α, provided s and sᶜ are nonempty, and Nat.card α ≠ 2 * Nat.card s.

This is the intransitive case of the O'Nan–Scott classification.