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 #

alternating_group α is the alternating group on α, defined as a subgroup (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 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 alternating_group α is simple if and only if fintype.card α ≠ 4.

source

@[protected, instance]

def alternating_group.fintype (α : Type u_1) [fintype α] [decidable_eq α] :

fintype ↥(alternating_group α)

source

def alternating_group (α : Type u_1) [fintype α] [decidable_eq α] :

subgroup (equiv.perm α)

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

Equations

alternating_group α = equiv.perm.sign.ker

Instances for alternating_group

alternating_group.normal

Instances for ↥alternating_group

source

@[protected, instance]

def alternating_group.unique (α : Type u_1) [fintype α] [decidable_eq α] [subsingleton α] :

unique ↥(alternating_group α)

Equations

alternating_group.unique α = {to_inhabited := {default := 1}, uniq := _}

source

theorem alternating_group_eq_sign_ker {α : Type u_1} [fintype α] [decidable_eq α] :

alternating_group α = equiv.perm.sign.ker

source

@[simp]

theorem equiv.perm.mem_alternating_group {α : Type u_1} [fintype α] [decidable_eq α] {f : equiv.perm α} :

f ∈ alternating_group α ↔ ⇑equiv.perm.sign f = 1

source

theorem equiv.perm.prod_list_swap_mem_alternating_group_iff_even_length {α : Type u_1} [fintype α] [decidable_eq α] {l : list (equiv.perm α)} (hl : ∀ (g : equiv.perm α), g ∈ l → g.is_swap) :

l.prod ∈ alternating_group α ↔ even l.length

source

theorem equiv.perm.is_three_cycle.mem_alternating_group {α : Type u_1} [fintype α] [decidable_eq α] {f : equiv.perm α} (h : f.is_three_cycle) :

f ∈ alternating_group α

source

theorem equiv.perm.fin_rotate_bit1_mem_alternating_group {n : ℕ} :

fin_rotate (bit1 n) ∈ alternating_group (fin (bit1 n))

source

theorem two_mul_card_alternating_group {α : Type u_1} [fintype α] [decidable_eq α] [nontrivial α] :

2 * fintype.card ↥(alternating_group α) = fintype.card (equiv.perm α)

source

@[protected, instance]

def alternating_group.normal {α : Type u_1} [fintype α] [decidable_eq α] :

(alternating_group α).normal

source

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 σ τ

source

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 σ τ

source

@[simp]

theorem equiv.perm.closure_three_cycles_eq_alternating {α : Type u_1} [fintype α] [decidable_eq α] :

subgroup.closure {σ : equiv.perm α | σ.is_three_cycle} = alternating_group α

source

theorem equiv.perm.is_three_cycle.alternating_normal_closure {α : Type u_1} [fintype α] [decidable_eq α] (h5 : 5 ≤ fintype.card α) {f : equiv.perm α} (hf : f.is_three_cycle) :

subgroup.normal_closure {⟨f, _⟩} = ⊤

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.

source

theorem equiv.perm.is_three_cycle_sq_of_three_mem_cycle_type_five {g : equiv.perm (fin 5)} (h : 3 ∈ g.cycle_type) :

(g * g).is_three_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$.

source

theorem alternating_group.nontrivial_of_three_le_card {α : Type u_1} [fintype α] [decidable_eq α] (h3 : 3 ≤ fintype.card α) :

nontrivial ↥(alternating_group α)

source

@[protected, instance]

def alternating_group.nontrivial {n : ℕ} :

nontrivial ↥(alternating_group (fin (n + 3)))

source

theorem alternating_group.normal_closure_fin_rotate_five :

subgroup.normal_closure {⟨fin_rotate 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.

source

theorem alternating_group.normal_closure_swap_mul_swap_five :

subgroup.normal_closure {⟨equiv.swap 0 4 * equiv.swap 1 3, _⟩} = ⊤

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.

source

theorem alternating_group.is_conj_swap_mul_swap_of_cycle_type_two {g : equiv.perm (fin 5)} (ha : g ∈ alternating_group (fin 5)) (h1 : g ≠ 1) (h2 : ∀ (n : ℕ), n ∈ g.cycle_type → n = 2) :

is_conj (equiv.swap 0 4 * equiv.swap 1 3) 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$.

source

@[protected, instance]

def alternating_group.is_simple_group_five :

is_simple_group ↥(alternating_group (fin 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$.