commutator_alternatingGroup_eq_top

English

If the set of three-cycles generates the alternating group on α, then the commutator subgroup equals the whole alternating group (for |α| ≥ 5).

Русский

Если трициклические перестановки порождают чередующуюся группу на α, то коммутатор равен всей чередующей группе (при |α| ≥ 5).

LaTeX

$$$\text{If } |\alpha| \ge 5:\; [\operatorname{Alt}(\alpha), \operatorname{Alt}(\alpha)] = \operatorname{Alt}(\alpha)$$$

Lean4

/-- If `n ≥ 5`, then the alternating group on `n` letters is perfect -/
theorem commutator_alternatingGroup_eq_top (h5 : 5 ≤ Fintype.card α) : commutator (alternatingGroup α) = ⊤ :=
  by
  suffices closure {b : alternatingGroup α | (b : Perm α).IsThreeCycle} = ⊤
    by
    rw [eq_top_iff, ← this, Subgroup.closure_le]
    intro b hb
    exact hb.mem_commutator_alternatingGroup h5
  rw [← closure_three_cycles_eq_alternating]
  exact Subgroup.closure_closure_coe_preimage

Похожие утверждения