Alternating Groups #
The alternating group on a finite type α
is the subgroup of the permutation group perm α
consisting of the even permutations.
Main definitions #
alternating_group α
is the alternating group onα
, defined as asubgroup (perm α)
.
Main results #
-
two_mul_card_alternating_group
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. -
alternating_group.is_simple_group_five
shows that the alternating group onfin 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
alternating_group α
is simple if and only iffintype.card α ≠ 4
.
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
Equations
- alternating_group.unique α = {to_inhabited := {default := 1}, uniq := _}
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$.
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$.
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$.