English
The Klein four subgroup equals the commutator subgroup of the alternating group.
Русский
Подгруппа Klein Four равна коммутаторной подгруппе чередующей группы.
LaTeX
$$$\mathrm{kleinFour}(\alpha) = \mathrm{commutator}(\mathrm{alternatingGroup}(\alpha))$$$
Lean4
theorem kleinFour_eq_commutator (hα4 : Nat.card α = 4) : kleinFour α = commutator (alternatingGroup α) :=
by
have _ : (kleinFour α).Normal := normal_kleinFour hα4
have : Nat.card (alternatingGroup α ⧸ kleinFour α) = 3 :=
by
rw [← Nat.mul_left_inj (a := Nat.card (kleinFour α))]
· rw [← Subgroup.card_eq_card_quotient_mul_card_subgroup]
rw [card_of_card_eq_four hα4, kleinFour_card_of_card_eq_four hα4]
rw [kleinFour_card_of_card_eq_four hα4]; simp
have comm_le : commutator (alternatingGroup α) ≤ kleinFour α :=
by
rw [← Subgroup.Normal.quotient_commutative_iff_commutator_le]
exact (isCyclic_of_prime_card this).commutative
have comm_ne_bot : commutator (alternatingGroup α) ≠ ⊥ :=
by
rw [ne_eq, commutator_eq_bot_iff_center_eq_top, center_eq_bot (le_of_eq hα4.symm)]
apply @bot_ne_top _ _ _ ?_
rw [Subgroup.nontrivial_iff, ← Finite.one_lt_card_iff_nontrivial, card_of_card_eq_four hα4]
simp
obtain ⟨k, hk, hk'⟩ := Or.resolve_left (Subgroup.bot_or_exists_ne_one _) comm_ne_bot
suffices hk22 : (k : Equiv.Perm α).cycleType = { 2, 2 }
by
refine le_antisymm ?_ comm_le
intro g hg
rw [← SetLike.mem_coe, coe_kleinFour_of_card_eq_four hα4, Set.mem_union, Set.mem_singleton_iff,
Set.mem_setOf_eq] at hg
rcases hg with ⟨rfl⟩ | hg
· exact Subgroup.one_mem _
· rw [← hg, ← Equiv.Perm.isConj_iff_cycleType_eq, isConj_iff] at hk22
obtain ⟨c, hc⟩ := hk22
rw [← MulAut.conjNormal_apply, Subtype.coe_inj] at hc
simp only [commutator, ← hc]
let fc : MulAut (alternatingGroup α) := MulAut.conjNormal c
suffices (⊤ : Subgroup (alternatingGroup α)) = Subgroup.map fc.toMonoidHom (⊤ : Subgroup (alternatingGroup α))
by
rw [this, ← Subgroup.map_commutator]
refine Subgroup.mem_map_of_mem _ hk
apply symm
rw [← MonoidHom.range_eq_map]
rw [MonoidHom.range_eq_top]
exact MulEquiv.surjective _
have hk2 := comm_le hk
rw [← SetLike.mem_coe, coe_kleinFour_of_card_eq_four hα4, Set.mem_union, Set.mem_singleton_iff,
Set.mem_setOf_eq] at hk2
exact hk2.resolve_left hk'
