Alternating Groups

The alternating group on a finite type α is the subgroup of the permutation group Perm α consisting of the even permutations.

Main definitions

• alternatingGroup α is the alternating group on α, defined as a Subgroup (Perm α).

Main results

• two_mul_card_alternatingGroup shows that the alternating group is half as large as the permutation group it is a subgroup of.

• closure_three_cycles_eq_alternating shows that the alternating group is generated by 3-cycles.

• alternatingGroup.isSimpleGroup_five shows that the alternating group on Fin 5 is simple. The proof shows that the normal closure of any non-identity element of this group contains a 3-cycle.

Tags

alternating group permutation

TODO

• Show that alternatingGroup α is simple if and only if Fintype.card α ≠ 4.

def alternatingGroup (α : Type u_1) [Fintype α] [DecidableEq α] : Subgroup (Equiv.Perm α)

The alternating group on a finite type, realized as a subgroup of Equiv.Perm. For $A_n$, use alternatingGroup (Fin n).

Equations

• alternatingGroup α = MonoidHom.ker Equiv.Perm.sign

instance fta (α : Type u_1) [Fintype α] [DecidableEq α] : Fintype ↥(alternatingGroup α)

Equations

• fta α = Subtype.fintype fun (x : Equiv.Perm α) => x ∈ alternatingGroup α

instance instUniqueSubtypePermMemSubgroupPermGroupInstMembershipInstSetLikeSubgroupAlternatingGroup (α : Type u_1) [Fintype α] [DecidableEq α] [Subsingleton α] : Unique ↥(alternatingGroup α)

Equations

• instUniqueSubtypePermMemSubgroupPermGroupInstMembershipInstSetLikeSubgroupAlternatingGroup α = { toInhabited := { default := 1 }, uniq := (_ : ∀ (x : ↥(alternatingGroup α)), x = default) }

theorem alternatingGroup_eq_sign_ker {α : Type u_1} [Fintype α] [DecidableEq α] : alternatingGroup α = MonoidHom.ker Equiv.Perm.sign

@[simp]

theorem Equiv.Perm.mem_alternatingGroup {α : Type u_1} [Fintype α] [DecidableEq α] {f : Equiv.Perm α} : f ∈ alternatingGroup α ↔ Equiv.Perm.sign f = 1

theorem Equiv.Perm.prod_list_swap_mem_alternatingGroup_iff_even_length {α : Type u_1} [Fintype α] [DecidableEq α] {l : List (Equiv.Perm α)} (hl : ∀ g ∈ l, Equiv.Perm.IsSwap g) : List.prod l ∈ alternatingGroup α ↔ Even (List.length l)

theorem Equiv.Perm.IsThreeCycle.mem_alternatingGroup {α : Type u_1} [Fintype α] [DecidableEq α] {f : Equiv.Perm α} (h : Equiv.Perm.IsThreeCycle f) : f ∈ alternatingGroup α

theorem Equiv.Perm.finRotate_bit1_mem_alternatingGroup {n : ℕ} : finRotate (bit1 n) ∈ alternatingGroup (Fin (bit1 n))

theorem two_mul_card_alternatingGroup {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] : 2 * Fintype.card ↥(alternatingGroup α) = Fintype.card (Equiv.Perm α)

instance alternatingGroup.normal {α : Type u_1} [Fintype α] [DecidableEq α] : Subgroup.Normal (alternatingGroup α)

Equations

• (_ : Subgroup.Normal (alternatingGroup α)) = (_ : Subgroup.Normal (MonoidHom.ker Equiv.Perm.sign))

theorem alternatingGroup.isConj_of {α : Type u_1} [Fintype α] [DecidableEq α] {σ : ↥(alternatingGroup α)} {τ : ↥(alternatingGroup α)} (hc : IsConj ↑σ ↑τ) (hσ : (Equiv.Perm.support ↑σ).card + 2 ≤ Fintype.card α) : IsConj σ τ

theorem alternatingGroup.isThreeCycle_isConj {α : Type u_1} [Fintype α] [DecidableEq α] (h5 : 5 ≤ Fintype.card α) {σ : ↥(alternatingGroup α)} {τ : ↥(alternatingGroup α)} (hσ : Equiv.Perm.IsThreeCycle ↑σ) (hτ : Equiv.Perm.IsThreeCycle ↑τ) : IsConj σ τ

@[simp]

theorem Equiv.Perm.closure_three_cycles_eq_alternating {α : Type u_1} [Fintype α] [DecidableEq α] : Subgroup.closure {σ : Equiv.Perm α | Equiv.Perm.IsThreeCycle σ} = alternatingGroup α

theorem Equiv.Perm.IsThreeCycle.alternating_normalClosure {α : Type u_1} [Fintype α] [DecidableEq α] (h5 : 5 ≤ Fintype.card α) {f : Equiv.Perm α} (hf : Equiv.Perm.IsThreeCycle f) : Subgroup.normalClosure {{ val := f, property := (_ : f ∈ alternatingGroup α) }} = ⊤

A key lemma to prove $A_5$ is simple. Shows that any normal subgroup of an alternating group on at least 5 elements is the entire alternating group if it contains a 3-cycle.

theorem Equiv.Perm.isThreeCycle_sq_of_three_mem_cycleType_five {g : Equiv.Perm (Fin 5)} (h : 3 ∈ Equiv.Perm.cycleType g) : Equiv.Perm.IsThreeCycle (g * g)

Part of proving $A_5$ is simple. Shows that the square of any element of $A_5$ with a 3-cycle in its cycle decomposition is a 3-cycle, so the normal closure of the original element must be $A_5$.

theorem alternatingGroup.nontrivial_of_three_le_card {α : Type u_1} [Fintype α] [DecidableEq α] (h3 : 3 ≤ Fintype.card α) : Nontrivial ↥(alternatingGroup α)

instance alternatingGroup.instNontrivialSubtypePermFinHAddNatInstHAddInstAddNatOfNatMemSubgroupPermGroupInstMembershipInstSetLikeSubgroupAlternatingGroupFintypeInstDecidableEqFin {n : ℕ} : Nontrivial ↥(alternatingGroup (Fin (n + 3)))

Equations

• (_ : Nontrivial ↥(alternatingGroup (Fin (n + 3)))) = (_ : Nontrivial ↥(alternatingGroup (Fin (n + 3))))

theorem alternatingGroup.normalClosure_finRotate_five : Subgroup.normalClosure {{ val := finRotate 5, property := (_ : finRotate (bit1 2) ∈ alternatingGroup (Fin (bit1 2))) }} = ⊤

The normal closure of the 5-cycle finRotate 5 within $A_5$ is the whole group. This will be used to show that the normal closure of any 5-cycle within $A_5$ is the whole group.

theorem alternatingGroup.normalClosure_swap_mul_swap_five : Subgroup.normalClosure {{ val := Equiv.swap 0 4 * Equiv.swap 1 3, property := (_ : Equiv.swap 0 4 * Equiv.swap 1 3 ∈ alternatingGroup (Fin 5)) }} = ⊤

The normal closure of $(04)(13)$ within $A_5$ is the whole group. This will be used to show that the normal closure of any permutation of cycle type $(2,2)$ is the whole group.

theorem alternatingGroup.isConj_swap_mul_swap_of_cycleType_two {g : Equiv.Perm (Fin 5)} (ha : g ∈ alternatingGroup (Fin 5)) (h1 : g ≠ 1) (h2 : ∀ n ∈ Equiv.Perm.cycleType g, n = 2) : IsConj (Equiv.swap 0 4 * Equiv.swap 1 3) g

Shows that any non-identity element of $A_5$ whose cycle decomposition consists only of swaps is conjugate to $(04)(13)$. This is used to show that the normal closure of such a permutation in $A_5$ is $A_5$.

instance alternatingGroup.isSimpleGroup_five : IsSimpleGroup ↥(alternatingGroup (Fin 5))

Shows that $A_5$ is simple by taking an arbitrary non-identity element and showing by casework on its cycle type that its normal closure is all of $A_5$.

Equations

• alternatingGroup.isSimpleGroup_five = (_ : IsSimpleGroup ↥(alternatingGroup (Fin 5)))