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 An, 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) :
    instance alternatingGroup.normal {α : Type u_1} [Fintype α] [DecidableEq α] :
    (alternatingGroup α).Normal
    Equations
    • =
    theorem alternatingGroup.isConj_of {α : Type u_1} [Fintype α] [DecidableEq α] {σ : { x : Equiv.Perm α // x alternatingGroup α }} {τ : { x : Equiv.Perm α // x alternatingGroup α }} (hc : IsConj σ τ) (hσ : (↑σ).support.card + 2 Fintype.card α) :
    IsConj σ τ
    theorem alternatingGroup.isThreeCycle_isConj {α : Type u_1} [Fintype α] [DecidableEq α] (h5 : 5 Fintype.card α) {σ : { x : Equiv.Perm α // x alternatingGroup α }} {τ : { x : Equiv.Perm α // x 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 A5 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 A5 is simple. Shows that the square of any element of A5 with a 3-cycle in its cycle decomposition is a 3-cycle, so the normal closure of the original element must be A5.

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

    The normal closure of (04)(13) within A5 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 A5 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 A5 is A5.

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

    Equations