Maximal subgroups of the alternating group

• alternatingGroup.isCoatom_stabilizer: if neither s : Set α nor its complement is empty, and if, moreover, Nat.card α ≠ 2 * s.ncard, then stabilizer (alternatingGroup α) s is a maximal subgroup of alternatingGroup α.

This is the “intransitive case” of the O'Nan-Scott classification of maximal subgroups of the alternating groups.

Compare with Equiv.Perm.isCoatom_stabilizer for the case of the permutation group.

TODO

• Application to primitivity of the action of alternatingGroup α 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.exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard {α : Type u_1} [Fintype α] [DecidableEq α] {s : Set α} (hs : 2 < s.ncard) : ∃ g ∈ MulAction.stabilizer (Perm α) s, g.IsThreeCycle

theorem Equiv.Perm.exists_mem_stabilizer_isThreeCycle {α : Type u_1} [Fintype α] [DecidableEq α] (s : Set α) (hα : 4 < Nat.card α) : ∃ g ∈ MulAction.stabilizer (Perm α) s, g.IsThreeCycle

theorem Equiv.Perm.alternatingGroup_le_of_isPreprimitive {α : Type u_1} [Fintype α] [DecidableEq α] (h4 : 4 < Nat.card α) (G : Subgroup (Perm α)) [hG' : MulAction.IsPreprimitive (↥G) α] {s : Set α} (hG : MulAction.stabilizer (Perm α) s ⊓ alternatingGroup α ≤ G) : alternatingGroup α ≤ G

theorem alternatingGroup.stabilizer.surjective_toPerm {α : Type u_1} [Fintype α] [DecidableEq α] {s : Set α} (hs : sᶜ.Nontrivial) : Function.Surjective MulAction.toPerm

theorem alternatingGroup.stabilizer_isPreprimitive {α : Type u_1} [Fintype α] [DecidableEq α] {s : Set α} (hs : sᶜ.Nontrivial) : MulAction.IsPreprimitive ↥(MulAction.stabilizer (↥(alternatingGroup α)) s) ↑s

In the alternating group, the stabilizer of a set acts primitively on that set if the complement is nontrivial.

theorem alternatingGroup.stabilizer_subgroup_isPreprimitive {α : Type u_1} [Fintype α] [DecidableEq α] {s : Set α} (hsc : sᶜ.Nontrivial) {G : Subgroup ↥(alternatingGroup α)} (hG : MulAction.stabilizer (↥(alternatingGroup α)) s ≤ G) : MulAction.IsPreprimitive ↥(MulAction.stabilizer (↥G) s) ↑s

A subgroup of the alternating group that contains the stabilizer of a set acts primitively on that set if the complement is nontrivial.

theorem alternatingGroup.stabilizer_ne_top {α : Type u_1} [Fintype α] [DecidableEq α] {s : Set α} (hs : s.Nonempty) (hsc : sᶜ.Nontrivial) : MulAction.stabilizer (↥(alternatingGroup α)) s ≠ ⊤

If s : Set α is nonempty and its complement has at least two elements, then stabilizer (alternatingGroup α) s ≠ ⊤.

theorem alternatingGroup.exists_mem_stabilizer_smul_eq {α : Type u_1} [Fintype α] [DecidableEq α] (hα : 4 ≤ Nat.card α) {t : Set α} (a : α) : a ∈ t → ∀ b ∈ t, ∃ g ∈ MulAction.stabilizer (↥(alternatingGroup α)) t, g • a = b

theorem alternatingGroup.subgroup_eq_top_of_isPreprimitive {α : Type u_1} [Fintype α] [DecidableEq α] (h4 : 4 < Nat.card α) (G : Subgroup ↥(alternatingGroup α)) [hG' : MulAction.IsPreprimitive (↥G) α] {s : Set α} (hG : MulAction.stabilizer (↥(alternatingGroup α)) s ≤ G) : G = ⊤

theorem MulAction.IsBlock.subsingleton_of_ssubset_compl_of_stabilizer_alternatingGroup_le {α : Type u_1} [Fintype α] [DecidableEq α] {s B : Set α} {G : Subgroup ↥(alternatingGroup α)} (hs : s.Nontrivial) (hB_ss_sc : B ⊂ sᶜ) (hG : stabilizer (↥(alternatingGroup α)) s ≤ G) (hB : IsBlock (↥G) B) : B.Subsingleton

theorem alternatingGroup.isCoatom_stabilizer_of_ncard_lt_ncard_compl {α : Type u_1} [Fintype α] [DecidableEq α] {s : Set α} (h0 : s.Nontrivial) (hs : s.ncard < sᶜ.ncard) : IsCoatom (MulAction.stabilizer (↥(alternatingGroup α)) s)

theorem alternatingGroup.isCoatom_stabilizer_singleton {α : Type u_1} [Fintype α] [DecidableEq α] (h3 : 3 ≤ Nat.card α) {s : Set α} (h : s.Nonempty) (h1 : s.Subsingleton) : IsCoatom (MulAction.stabilizer (↥(alternatingGroup α)) s)

theorem alternatingGroup.isCoatom_stabilizer {α : Type u_1} [Fintype α] [DecidableEq α] {s : Set α} (h0 : s.Nonempty) (h1 : sᶜ.Nonempty) (hs : Nat.card α ≠ 2 * s.ncard) : IsCoatom (MulAction.stabilizer (↥(alternatingGroup α)) s)

MulAction.stabilizer (alternatingGroup α) s is a maximal subgroup of alternatingGroup α, provided s ≠ ∅, sᶜ ≠ ∅ and Nat.card α ≠ 2 * s.ncard.

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