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.

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

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.moves_in {α : Type u_2} (G : Subgroup (Perm α)) (t : Set α) (hGt : MulAction.stabilizer (Perm α) t ≤ G) (a : α) : a ∈ t → ∀ b ∈ t, ∃ (g : ↥G), g • a = b

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 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 Subgroup.isPretransitive_of_stabilizer_lt {α : Type u_2} {s : Set α} {G : Subgroup (Equiv.Perm α)} (hG : MulAction.stabilizer (Equiv.Perm α) s < G) : MulAction.IsPretransitive (↥G) α

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

theorem IsBlock.subsingleton_of_stabilizer_lt_of_subset {α : Type u_2} {s B : Set α} {G : Subgroup (Equiv.Perm α)} (hB_not_le_sc : ∀ (B : Set α), MulAction.IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton) (hG : MulAction.stabilizer (Equiv.Perm α) s < G) (hBs : B ⊆ s) (hB : MulAction.IsBlock (↥G) B) : B.Subsingleton

theorem IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl {α : Type u_2} [Finite α] {s B : Set α} {G : Subgroup (Equiv.Perm α)} (hG : MulAction.stabilizer (Equiv.Perm α) s ≤ G) (hBs : ¬B ⊆ s) (hBsc : ¬B ⊆ sᶜ) (hB : MulAction.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.