English
Let α be finite with at least 5 elements, and f a 3-cycle in Perm(α). Then the normal closure of {f} inside the alternating group α is the whole group.
Русский
Пусть α конечна и |α| ≥ 5, и f — трёхцикл в Perm(α). Тогда нормальное замыкание множества {f} внутри A_α равно всей группе.
LaTeX
$$$$5 \\leq |\\alpha| \\Rightarrow \\operatorname{normalClosure}\\{ f \\} = \\top.$$$$
Lean4
/-- 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. -/
theorem alternating_normalClosure (h5 : 5 ≤ Fintype.card α) {f : Perm α} (hf : IsThreeCycle f) :
normalClosure ({⟨f, hf.mem_alternatingGroup⟩} : Set (alternatingGroup α)) = ⊤ :=
eq_top_iff.2
(by
have hi : Function.Injective (alternatingGroup α).subtype := Subtype.coe_injective
refine eq_top_iff.1 (map_injective hi (le_antisymm (map_mono le_top) ?_))
rw [← MonoidHom.range_eq_map, range_subtype, normalClosure, MonoidHom.map_closure]
refine (le_of_eq closure_three_cycles_eq_alternating.symm).trans (closure_mono ?_)
intro g h
obtain ⟨c, rfl⟩ := isConj_iff.1 (isConj_iff_cycleType_eq.2 (hf.trans h.symm))
refine ⟨⟨c * f * c⁻¹, h.mem_alternatingGroup⟩, ?_, rfl⟩
rw [Group.mem_conjugatesOfSet_iff]
exact ⟨⟨f, hf.mem_alternatingGroup⟩, Set.mem_singleton _, isThreeCycle_isConj h5 hf h⟩)
