The Klein Four subgroup of an alternating group on 4 letters

Let α be a finite type such that Nat.card α = 4.

• alternatingGroup.kleinFour : the subgroup of alternatingGroup α generated by permutations of cycle type (2, 2).

Main results

• alternatingGroup.kleinFour_isKleinFour: alternatingGroup.kleinFour α satisfies IsKleinFour. (When 4 < Nat.card α, it is equal to ⊤, when Nat.card α < 4, it is trivial.)

• alternatingGroup.two_sylow_eq_kleinFour_of_card_eq_four: All 2-sylow subgroups of alternatingGroup α are equal to kleinFour α.

• alternatingGroup.characteristic_kleinFour: the subgroup alternatingGroup.kleinFour α is characteristic.

• alternatingGroup.kleinFour_eq_commutator: the subgroup alternatingGroup.kleinFour α is the commutator subgroup of alternatingGroup α. (When 4 < Nat.card α, the commutator subgroup of alternatingGroup α is equal to ⊤; when Nat.card α < 3, it is trivial.)

Remark on implementation

We start from alternatingGroup.kleinFour α as given by its definition. We first prove that it is equal to any 2-sylow subgroup: the elements of such a sylow subgroup S have order a power of 2, and this implies that their cycle type is () or (2,2). Since there are exactly 4 elements of that cycle type, we conclude that alternatingGroup.kleinFour α = S. Since all 2-sylow subgroups are conjugate, we conclude that there is only one 2-sylow subgroup and that it is normal, and then characteristic.

TODO :

Prove alternatingGroup.kleinFour α = commutator (alternatingGroup α) without any assumption on Nat.card α.

def alternatingGroup.kleinFour (α : Type u_1) [DecidableEq α] [Fintype α] : Subgroup ↥(alternatingGroup α)

The subgroup of alternatingGroup α generated by permutations of cycle type (2, 2).

When Nat.card α = 4, it will effectively be of Klein Four type.

Equations

• alternatingGroup.kleinFour α = Subgroup.closure {g : ↥(alternatingGroup α) | (↑g).cycleType = {2, 2}}

theorem alternatingGroup.mem_kleinFour_of_order_two_pow {α : Type u_1} [DecidableEq α] [Fintype α] (hα4 : Nat.card α = 4) {g : Equiv.Perm α} (hg0 : g ∈ alternatingGroup α) {n : ℕ} (hg : orderOf g ∣ 2 ^ n) : g.cycleType = ∅ ∨ g.cycleType = {2, 2}

theorem alternatingGroup.card_of_card_eq_four {α : Type u_1} [DecidableEq α] [Fintype α] (hα4 : Nat.card α = 4) : Nat.card ↥(alternatingGroup α) = 12

theorem alternatingGroup.card_two_sylow_of_card_eq_four {α : Type u_1} [DecidableEq α] [Fintype α] (hα4 : Nat.card α = 4) (S : Sylow 2 ↥(alternatingGroup α)) : Nat.card ↥↑S = 4

theorem alternatingGroup.coe_two_sylow_of_card_eq_four {α : Type u_1} [DecidableEq α] [Fintype α] (hα4 : Nat.card α = 4) (S : Sylow 2 ↥(alternatingGroup α)) : ↑S = {1} ∪ {g : ↥(alternatingGroup α) | (↑g).cycleType = {2, 2}}

theorem alternatingGroup.two_sylow_eq_kleinFour_of_card_eq_four {α : Type u_1} [DecidableEq α] [Fintype α] (hα4 : Nat.card α = 4) (S : Sylow 2 ↥(alternatingGroup α)) : ↑S = kleinFour α

theorem alternatingGroup.subsingleton_two_sylow {α : Type u_1} [DecidableEq α] [Fintype α] (hα4 : Nat.card α = 4) : Subsingleton (Sylow 2 ↥(alternatingGroup α))

theorem alternatingGroup.characteristic_kleinFour {α : Type u_1} [DecidableEq α] [Fintype α] (hα4 : Nat.card α = 4) : (kleinFour α).Characteristic

theorem alternatingGroup.normal_kleinFour {α : Type u_1} [DecidableEq α] [Fintype α] (hα4 : Nat.card α = 4) : (kleinFour α).Normal

theorem alternatingGroup.kleinFour_card_of_card_eq_four {α : Type u_1} [DecidableEq α] [Fintype α] (hα4 : Nat.card α = 4) : Nat.card ↥(kleinFour α) = 4

theorem alternatingGroup.coe_kleinFour_of_card_eq_four {α : Type u_1} [DecidableEq α] [Fintype α] (hα4 : Nat.card α = 4) : ↑(kleinFour α) = {1} ∪ {g : ↥(alternatingGroup α) | (↑g).cycleType = {2, 2}}

theorem alternatingGroup.exponent_kleinFour_of_card_eq_four {α : Type u_1} [DecidableEq α] [Fintype α] (hα4 : Nat.card α = 4) : Monoid.exponent ↥(kleinFour α) = 2

theorem alternatingGroup.kleinFour_isKleinFour {α : Type u_1} [DecidableEq α] [Fintype α] (hα4 : Nat.card α = 4) : IsKleinFour ↥(kleinFour α)

theorem alternatingGroup.kleinFour_eq_commutator {α : Type u_1} [DecidableEq α] [Fintype α] (hα4 : Nat.card α = 4) : kleinFour α = commutator ↥(alternatingGroup α)