The alternating group is simple

Main results

• Equiv.Perm.alternatingGroup_le_of_normal: If α has at least 5 elements, then a nontrivial normal subgroup of Equiv.Perm α contains the alternating group.

• alternatingGroup.normal_subgroup_eq_bot_or_eq_top: If α has at least 5 elements, then a nontrivial normal subgroup of alternatingGroup is ⊤.

• alternatingGroup.isSimpleGroup: If α has at least 5 elements, then alternatingGroup α is a simple group.

Main definitions

The proofs of the above results follow from the Iwasawa criterion applied to the following Iwasawa structures. Their definitions are similar: the groups Equiv.Perm α and alternatingGroup α act on α hence they act on Set.powersetCard α n, for any natural number n. For n = 2, this gives an Iwaswa structure of Equiv.Perm α, for n = 3 or n = 4, this gives an Iwasawa structure of alternatingGroup α.

• Equiv.Perm.iwasawaStructure_two: the natural IwasawaStructure of Equiv.Perm α acting on Set.powersetCard α 2. Its commutative subgroups consist of the permutations with support in a given element of Set.powersetCard α 2. They are cyclic of order 2.

• alternatingGroup.iwasawaStructure_three: the natural IwasawaStructure of alternatingGroup α acting on Set.powersetCard α 3.

  Its commutative subgroups consist of the permutations with support in a given element of Set.powersetCard α 2. They are cyclic of order 3.

• alternatingGroup.iwasawaStructure_four: the natural IwasawaStructure of alternatingGroup α acting on Set.powersetCard α 4

  Its commutative subgroups consist of the permutations of cycleType (2, 2) with support in a given element of Set.powersetCard α 2. They have order 4 and exponent 2 (IsKleinFour).

TODO

This file contains two uncomfortable uses of convert:

• on line 81, to identify MulAut.conj and ConjAct.toConjAct.

• on line 148, to match the subtype coercions for Finset and Set.

def Equiv.Perm.iwasawaStructure_two {α : Type u_1} [Finite α] [DecidableEq α] [(s : Set α) → DecidablePred fun (x : α) => x ∈ s] : MulAction.IwasawaStructure (Perm α) ↑(Set.powersetCard α 2)

The Iwasawa structure of Perm α acting on Set.powersetCard α 2.

Equations

• Equiv.Perm.iwasawaStructure_two = { T := fun (s : ↑(Set.powersetCard α 2)) => Equiv.Perm.ofSubtype.range, is_comm := ⋯, is_conj := ⋯, is_generator := ⋯ }

theorem Equiv.Perm.alternatingGroup_le_of_normal {α : Type u_2} [DecidableEq α] [Fintype α] (hα : 5 ≤ Nat.card α) {N : Subgroup (Perm α)} [N.Normal] (ntN : Nontrivial ↥N) : alternatingGroup α ≤ N

If α has at least 5 elements, then any nontrivial normal subgroup of Equiv.Perm α contains alternatingGroup α.

def alternatingGroup.iwasawaStructure_three {α : Type u_1} [DecidableEq α] [Fintype α] : MulAction.IwasawaStructure ↥(alternatingGroup α) ↑(Set.powersetCard α 3)

The Iwasawa structure of alternatingGroup α acting on Set.powersetCard α 3.

Equations

• alternatingGroup.iwasawaStructure_three = { T := fun (s : ↑(Set.powersetCard α 3)) => (alternatingGroup.ofSubtype ↑s).range, is_comm := ⋯, is_conj := ⋯, is_generator := ⋯ }

theorem alternatingGroup.normal_subgroup_eq_bot_or_eq_top_of_card_ne_six {α : Type u_1} [DecidableEq α] [Fintype α] (hα : 5 ≤ Nat.card α) (hα' : Nat.card α ≠ 6) {N : Subgroup ↥(alternatingGroup α)} [N.Normal] : N = ⊥ ∨ N = ⊤

If α has at least 5 elements, but not 6, then the only nontrivial normal subgroup of alternatingGroup α is ⊤.

theorem alternatingGroup.mem_map_kleinFour_ofSubtype {α : Type u_1} [DecidableEq α] [Fintype α] {s : Finset α} (hs : s.card = 4) (k : ↥(alternatingGroup α)) : k ∈ Subgroup.map (ofSubtype s) (kleinFour ↥s) ↔ (↑k).support ⊆ s ∧ (↑k = 1 ∨ (↑k).cycleType = {2, 2})

theorem alternatingGroup.map_kleinFour_conj {α : Type u_1} [DecidableEq α] [Fintype α] (s : Finset α) (hs : s.card = 4) (g : ↥(alternatingGroup α)) : Subgroup.map (ofSubtype (g • s)) (kleinFour ↥(g • s)) = MulAut.conj g • Subgroup.map (ofSubtype s) (kleinFour ↥s)

def alternatingGroup.iwasawaStructure_four {α : Type u_1} [DecidableEq α] [Fintype α] (h5 : 5 ≤ Nat.card α) : MulAction.IwasawaStructure ↥(alternatingGroup α) ↑(Set.powersetCard α 4)

The Iwasawa structure of alternatingGroup α acting on Set.powersetCard α 4, provided α has at least 5 elements.

Equations

• One or more equations did not get rendered due to their size.

theorem alternatingGroup.normal_subgroup_eq_bot_or_eq_top_of_card_ne_eight {α : Type u_1} [DecidableEq α] [Fintype α] (hα : 5 ≤ Nat.card α) (hα' : Nat.card α ≠ 8) {N : Subgroup ↥(alternatingGroup α)} [N.Normal] : N = ⊥ ∨ N = ⊤

If α has at least 5 elements, but not 8, then the only nontrivial normal subgroup of alternatingGroup α is ⊤.

theorem alternatingGroup.normal_subgroup_eq_bot_or_eq_top {α : Type u_1} [DecidableEq α] [Fintype α] (hα : 5 ≤ Nat.card α) {N : Subgroup ↥(alternatingGroup α)} [N.Normal] : N = ⊥ ∨ N = ⊤

theorem alternatingGroup.isSimpleGroup {α : Type u_1} [DecidableEq α] [Fintype α] (hα : 5 ≤ Nat.card α) : IsSimpleGroup ↥(alternatingGroup α)

When α has at least 5 elements, then alternatingGroup α is a simple group.