English
The normal closure of the permutation (0 4)(1 3) inside A5 is the whole group.
Русский
Нормальное замыкание перестановки (0 4)(1 3) внутри A5 равно всей группе.
LaTeX
$$$$\\operatorname{normalClosure}\\{(0\\;4)(1\\;3)\\} = \\operatorname{top}.$$$$
Lean4
/-- The normal closure of $(04)(13)$ within $A_5$ is the whole group. This will be
used to show that the normal closure of any permutation of cycle type $(2,2)$ is the whole group.
-/
theorem normalClosure_swap_mul_swap_five :
normalClosure ({⟨swap 0 4 * swap 1 3, mem_alternatingGroup.2 (by decide)⟩} : Set (alternatingGroup (Fin 5))) = ⊤ :=
by
let g1 := (⟨swap 0 2 * swap 0 1, mem_alternatingGroup.2 (by decide)⟩ : alternatingGroup (Fin 5))
let g2 := (⟨swap 0 4 * swap 1 3, mem_alternatingGroup.2 (by decide)⟩ : alternatingGroup (Fin 5))
have h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, finRotate_bit1_mem_alternatingGroup (n := 2)⟩ :=
by
rw [Subtype.ext_iff]
simp only [Subgroup.coe_mul, Subgroup.coe_inv]
decide
rw [eq_top_iff, ← normalClosure_finRotate_five]
refine normalClosure_le_normal ?_
rw [Set.singleton_subset_iff, SetLike.mem_coe, ← h5]
have h : g2 ∈ normalClosure { g2 } := SetLike.mem_coe.1 (subset_normalClosure (Set.mem_singleton _))
exact mul_mem (Subgroup.normalClosure_normal.conj_mem _ h g1) (inv_mem h)
