# Documentation

Mathlib.GroupTheory.SpecificGroups.Alternating

# 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) [] [] :

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

Instances For
instance fta (α : Type u_1) [] [] :
Fintype { x // }
theorem alternatingGroup_eq_sign_ker {α : Type u_1} [] [] :
= MonoidHom.ker Equiv.Perm.sign
@[simp]
theorem Equiv.Perm.mem_alternatingGroup {α : Type u_1} [] [] {f : } :
Equiv.Perm.sign f = 1
theorem Equiv.Perm.prod_list_swap_mem_alternatingGroup_iff_even_length {α : Type u_1} [] [] {l : List ()} (hl : ∀ (g : ), g l) :
Even ()
theorem Equiv.Perm.IsThreeCycle.mem_alternatingGroup {α : Type u_1} [] [] {f : } (h : ) :
theorem two_mul_card_alternatingGroup {α : Type u_1} [] [] [] :
2 * Fintype.card { x // } =
instance alternatingGroup.normal {α : Type u_1} [] [] :
theorem alternatingGroup.isConj_of {α : Type u_1} [] [] {σ : { x // }} {τ : { x // }} (hc : IsConj σ τ) (hσ : ) :
IsConj σ τ
theorem alternatingGroup.isThreeCycle_isConj {α : Type u_1} [] [] (h5 : ) {σ : { x // }} {τ : { x // }} (hσ : ) (hτ : ) :
IsConj σ τ
theorem Equiv.Perm.IsThreeCycle.alternating_normalClosure {α : Type u_1} [] [] (h5 : ) {f : } (hf : ) :
Subgroup.normalClosure {{ val := f, property := (_ : ) }} =

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.

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} [] [] (h3 : ) :
Nontrivial { x // }

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.

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 ) (h1 : g 1) (h2 : ∀ (n : ), n = 2) :
IsConj ( * ) 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$.

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$.