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 #

Main results #

Tags #

alternating group permutation

TODO #

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

Equations
Instances For
    theorem alternatingGroup_eq_sign_ker {α : Type u_1} [Fintype α] [DecidableEq α] :
    alternatingGroup α = Equiv.Perm.sign.ker
    @[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 : gl, g.IsSwap) :
    l.prod alternatingGroup α Even l.length
    theorem Equiv.Perm.IsThreeCycle.mem_alternatingGroup {α : Type u_1} [Fintype α] [DecidableEq α] {f : Equiv.Perm α} (h : f.IsThreeCycle) :
    theorem alternatingGroup.normal {α : Type u_1} [Fintype α] [DecidableEq α] :
    (alternatingGroup α).Normal
    theorem alternatingGroup.isConj_of {α : Type u_1} [Fintype α] [DecidableEq α] {σ τ : (alternatingGroup α)} (hc : IsConj σ τ) (hσ : (↑σ).support.card + 2 Fintype.card α) :
    IsConj σ τ
    theorem alternatingGroup.isThreeCycle_isConj {α : Type u_1} [Fintype α] [DecidableEq α] (h5 : 5 Fintype.card α) {σ τ : (alternatingGroup α)} (hσ : (↑σ).IsThreeCycle) (hτ : (↑τ).IsThreeCycle) :
    IsConj σ τ
    theorem Equiv.Perm.IsThreeCycle.alternating_normalClosure {α : Type u_1} [Fintype α] [DecidableEq α] (h5 : 5 Fintype.card α) {f : Equiv.Perm α} (hf : f.IsThreeCycle) :

    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 g.cycleType) :
    (g * g).IsThreeCycle

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

    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 alternatingGroup (Fin 5)) (h1 : g 1) (h2 : ng.cycleType, n = 2) :

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