mathlib3 documentation

group_theory.specific_groups.alternating

Alternating Groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

@[protected, instance]
def alternating_group (α : Type u_1) [fintype α] [decidable_eq α] :

The alternating group on a finite type, realized as a subgroup of equiv.perm. For $A_n$, use alternating_group (fin n).

Equations
Instances for alternating_group
Instances for alternating_group
@[protected, instance]
Equations
@[protected, instance]
theorem alternating_group.is_conj_of {α : Type u_1} [fintype α] [decidable_eq α] {σ τ : (alternating_group α)} (hc : is_conj σ τ) (hσ : σ.support.card + 2 fintype.card α) :
is_conj σ τ
theorem alternating_group.is_three_cycle_is_conj {α : Type u_1} [fintype α] [decidable_eq α] (h5 : 5 fintype.card α) {σ τ : (alternating_group α)} (hσ : σ.is_three_cycle) (hτ : τ.is_three_cycle) :
is_conj σ τ

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

@[protected, instance]

The normal closure of the 5-cycle fin_rotate 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.

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

@[protected, instance]

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