Alternating Groups

The alternating group on a finite type α is the subgroup of the permutation group Perm α consisting of the even permutations.

Main definitions

• alternatingGroup α is the alternating group on α, defined as a Subgroup (Perm α).

Main results

• alternatingGroup.index_eq_two shows that the index of the alternating group is two.

• two_mul_card_alternatingGroup 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.

• alternatingGroup.isSimpleGroup_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.

• Equiv.Perm.eq_alternatingGroup_of_index_eq_two shows that a subgroup of index 2 of Equiv.Perm α is the alternating group.

• Equiv.Perm.alternatingGroup_le_of_index_le_two shows that a subgroup of index at most 2 of Equiv.Perm α contains the alternating group.

• Equiv.Perm.alternatingGroup.center_eq_bot: when 4 ≤ Nat.card α, then center of alternatingGroup α is trivial.

Instances

• The alternating group is a characteristic subgroup of the permutation group.

Tags

alternating group permutation simple characteristic index

TODO

• Show that alternatingGroup α is simple if and only if Fintype.card α ≠ 4.

def alternatingGroup (α : Type u_1) [Fintype α] [DecidableEq α] : Subgroup (Equiv.Perm α)

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

Equations

• alternatingGroup α = Equiv.Perm.sign.ker

@[implicit_reducible]

instance alternatingGroup.instFintype (α : Type u_1) [Fintype α] [DecidableEq α] : Fintype ↥(alternatingGroup α)

Equations

• alternatingGroup.instFintype α = Subtype.fintype (Membership.mem (alternatingGroup α))

@[implicit_reducible]

instance instUniqueSubtypePermMemSubgroupAlternatingGroupOfSubsingleton (α : Type u_1) [Fintype α] [DecidableEq α] [Subsingleton α] : Unique ↥(alternatingGroup α)

Equations

• instUniqueSubtypePermMemSubgroupAlternatingGroupOfSubsingleton α = { default := 1, uniq := ⋯ }

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 : Perm α} : f ∈ alternatingGroup α ↔ sign f = 1

theorem Equiv.Perm.mul_mem_alternatingGroup_of_isSwap {α : Type u_1} [Fintype α] [DecidableEq α] {g g' : Perm α} (hg : g.IsSwap) (hg' : g'.IsSwap) : g * g' ∈ alternatingGroup α

theorem Equiv.Perm.prod_list_swap_mem_alternatingGroup_iff_even_length {α : Type u_1} [Fintype α] [DecidableEq α] {l : List (Perm α)} (hl : ∀ g ∈ l, g.IsSwap) : l.prod ∈ alternatingGroup α ↔ Even l.length

theorem Equiv.Perm.IsThreeCycle.mem_alternatingGroup {α : Type u_1} [Fintype α] [DecidableEq α] {f : Perm α} (h : f.IsThreeCycle) : f ∈ alternatingGroup α

theorem Equiv.Perm.finRotate_bit1_mem_alternatingGroup {n : ℕ} : finRotate (2 * n + 1) ∈ alternatingGroup (Fin (2 * n + 1))

@[simp]

theorem alternatingGroup.index_eq_two {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] : (alternatingGroup α).index = 2

theorem alternatingGroup.index_eq_one {α : Type u_1} [Fintype α] [DecidableEq α] [Subsingleton α] : (alternatingGroup α).index = 1

def Equiv.altCongrHom {α : Type u_1} [Fintype α] [DecidableEq α] {β : Type u_2} [Fintype β] [DecidableEq β] (e : α ≃ β) : ↥(alternatingGroup α) ≃* ↥(alternatingGroup β)

The group isomorphism between alternatingGroups induced by the given Equiv.

Equations

• e.altCongrHom = (e.permCongrHom.subgroupMap (alternatingGroup α)).trans (MulEquiv.subgroupCongr ⋯)

@[simp]

theorem Equiv.altCongrHom_apply_coe {α : Type u_1} [Fintype α] [DecidableEq α] {β : Type u_2} [Fintype β] [DecidableEq β] (e : α ≃ β) (a✝ : ↥(alternatingGroup α)) : ↑(e.altCongrHom a✝) = e.permCongr ↑a✝

theorem two_mul_nat_card_alternatingGroup {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] : 2 * Nat.card ↥(alternatingGroup α) = Nat.card (Equiv.Perm α)

theorem two_mul_card_alternatingGroup {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] : 2 * Fintype.card ↥(alternatingGroup α) = Fintype.card (Equiv.Perm α)

theorem card_alternatingGroup {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] : Fintype.card ↥(alternatingGroup α) = (Fintype.card α).factorial / 2

theorem nat_card_alternatingGroup {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] : Nat.card ↥(alternatingGroup α) = (Nat.card α).factorial / 2

theorem alternatingGroup.isCyclic_of_card_le_three {α : Type u_1} [Fintype α] [DecidableEq α] (hα : Nat.card α ≤ 3) : IsCyclic ↥(alternatingGroup α)

theorem alternatingGroup.isMulCommutative_of_card_le_three {α : Type u_1} [Fintype α] [DecidableEq α] (hα : Nat.card α ≤ 3) : IsMulCommutative ↥(alternatingGroup α)

instance 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 ≤ Nat.card α) {σ τ : ↥(alternatingGroup α)} (hσ : (↑σ).IsThreeCycle) (hτ : (↑τ).IsThreeCycle) : IsConj σ τ

@[simp]

theorem Equiv.Perm.closure_three_cycles_eq_alternating {α : Type u_1} [Fintype α] [DecidableEq α] : Subgroup.closure {σ : Perm α | σ.IsThreeCycle} = alternatingGroup α

theorem Equiv.Perm.isThreeCycle_subset_alternatingGroup {α : Type u_1} [Fintype α] [DecidableEq α] : {g : Perm α | g.IsThreeCycle} ⊆ ↑(alternatingGroup α)

theorem alternatingGroup.closure_isThreeCycles_eq_top {α : Type u_1} [Fintype α] [DecidableEq α] : Subgroup.closure {g : ↥(alternatingGroup α) | (↑g).IsThreeCycle} = ⊤

theorem Equiv.Perm.closure_cycleType_eq_two_two_eq_alternatingGroup {α : Type u_1} [Fintype α] [DecidableEq α] (h5 : 5 ≤ Nat.card α) : Subgroup.closure {g : Perm α | g.cycleType = {2, 2}} = alternatingGroup α

The alternating group is the closure of the set of permutations with cycle type (2, 2).

@[deprecated Equiv.Perm.closure_cycleType_eq_two_two_eq_alternatingGroup (since := "2026-03-10")]

theorem Equiv.Perm.closure_cycleType_eq_2_2_eq_alternatingGroup {α : Type u_1} [Fintype α] [DecidableEq α] (h5 : 5 ≤ Nat.card α) : Subgroup.closure {g : Perm α | g.cycleType = {2, 2}} = alternatingGroup α

Alias of Equiv.Perm.closure_cycleType_eq_two_two_eq_alternatingGroup.

---

The alternating group is the closure of the set of permutations with cycle type (2, 2).

theorem Equiv.Perm.cycleType_eq_two_two_subset_alternatingGroup {α : Type u_1} [Fintype α] [DecidableEq α] : {g : Perm α | g.cycleType = {2, 2}} ⊆ ↑(alternatingGroup α)

theorem alternatingGroup.closure_cycleType_eq_two_two_eq_top {α : Type u_1} [Fintype α] [DecidableEq α] (h5 : 5 ≤ Nat.card α) : Subgroup.closure {g : ↥(alternatingGroup α) | (↑g).cycleType = {2, 2}} = ⊤

theorem Equiv.Perm.isThreeCycle_sq_of_three_mem_cycleType_five {g : 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$.

theorem alternatingGroup.eq_bot_of_card_le_two {α : Type u_1} [Fintype α] [DecidableEq α] (h2 : Nat.card α ≤ 2) : alternatingGroup α = ⊥

theorem alternatingGroup.nontrivial_of_three_le_card {α : Type u_1} [Fintype α] [DecidableEq α] (h3 : 3 ≤ Nat.card α) : Nontrivial ↥(alternatingGroup α)

instance alternatingGroup.instNontrivialSubtypePermFinHAddNatOfNatMemSubgroup {n : ℕ} : Nontrivial ↥(alternatingGroup (Fin (n + 3)))

@[deprecated "This was an auxilliary lemma for the proof of simplicity of A_5 which has now been superceded by `alternatingGroup.isSimpleGroup`." (since := "2026-04-28")]

theorem alternatingGroup.isConj_swap_mul_swap_of_cycleType_two {g : Equiv.Perm (Fin 5)} (ha : g ∈ alternatingGroup (Fin 5)) (h1 : g ≠ 1) (h2 : ∀ n ∈ g.cycleType, n = 2) : IsConj (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$.

theorem alternatingGroup.center_eq_bot {α : Type u_1} [Fintype α] [DecidableEq α] (hα4 : 4 ≤ Nat.card α) : Subgroup.center ↥(alternatingGroup α) = ⊥

theorem alternatingGroup.isMulCommutative_iff_card_le_three {α : Type u_1} [Fintype α] [DecidableEq α] : IsMulCommutative ↥(alternatingGroup α) ↔ Nat.card α ≤ 3

theorem alternatingGroup.isCyclic_iff_card_le_three {α : Type u_1} [Fintype α] [DecidableEq α] : IsCyclic ↥(alternatingGroup α) ↔ Nat.card α ≤ 3

def alternatingGroup.ofSubtype {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : ↥(alternatingGroup ↥s) →* ↥(alternatingGroup α)

The element of alternatingGroup α induced by an element of alternatingGroup s, when s : Finset α.

Equations

• alternatingGroup.ofSubtype s = { toFun := fun (x : ↥(alternatingGroup ↥s)) => ⟨Equiv.Perm.ofSubtype ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

theorem alternatingGroup.ofSubtype_injective {α : Type u_1} [Fintype α] [DecidableEq α] {s : Finset α} : Function.Injective ⇑(ofSubtype s)

theorem alternatingGroup.ofSubtype_inj {α : Type u_1} [Fintype α] [DecidableEq α] {s : Finset α} {g h : ↥(alternatingGroup ↥s)} : (ofSubtype s) g = (ofSubtype s) h ↔ g = h

theorem alternatingGroup.coe_ofSubtype {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) (k : ↥(alternatingGroup ↥s)) : ↑((ofSubtype s) k) = Equiv.Perm.ofSubtype ↑k

theorem alternatingGroup.map_ofSubtype {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : Subgroup.map Equiv.Perm.ofSubtype (alternatingGroup ↥s) = Equiv.Perm.ofSubtype.range ⊓ alternatingGroup α

theorem alternatingGroup.ofSubtype_comp_subtype {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : (alternatingGroup α).subtype.comp (ofSubtype s) = Equiv.Perm.ofSubtype.comp (alternatingGroup ↥s).subtype

theorem alternatingGroup.range_ofSubtype {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : (ofSubtype s).range = Equiv.Perm.ofSubtype.range.subgroupOf (alternatingGroup α)

theorem alternatingGroup.mem_range_ofSubtype_iff {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) (k : ↥(alternatingGroup α)) : k ∈ (ofSubtype s).range ↔ (↑k).support ⊆ s

theorem alternatingGroup.conj_smul_range_ofSubtype {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) (g : ↥(alternatingGroup α)) : MulAut.conj g • (ofSubtype s).range = (ofSubtype (g • s)).range

theorem Equiv.Perm.eq_alternatingGroup_of_index_eq_two {α : Type u_1} [Fintype α] [DecidableEq α] {G : Subgroup (Perm α)} (hG : G.index = 2) : G = alternatingGroup α

The alternating group is the only subgroup of index 2 of the permutation group.

theorem Equiv.Perm.alternatingGroup_le_of_index_le_two {α : Type u_1} [Fintype α] [DecidableEq α] {G : Subgroup (Perm α)} (hG : G.index ≤ 2) : alternatingGroup α ≤ G

A subgroup of the permutation group of index ≤ 2 contains the alternating group.

instance instCharacteristicPermAlternatingGroup {α : Type u_1} [Fintype α] [DecidableEq α] : (alternatingGroup α).Characteristic

The alternating group is a characteristic subgroup of the permutation group.