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

Here, we need that Nat.card α has at least 4 elements, so that either t has at least 3 elements, or tᶜ has at least 2. The condition is necessary, because the result is wrong when α = {1, 2, 3} and either t = {1, 2} or t = {1}.

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)

Note : The proof of this statement is close to that of Equiv.Perm.isCoatom_stabilizer_of_ncard_lt_ncard_compl, and while it would not be absolutely impossible to abstract both proofs, the result would be slightly awkward because the details of the results involved in the proof differ in annoying details. And it would be used only twice.

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.