English
For subgroups H1,H2 of G and a homomorphism f, the image of the commutator equals the commutator of the images: map f [H1,H2] = [map f H1, map f H2].
Русский
Пусть f — гомоморфизм; образ коммутатора равен коммутатору образов: map f [H1,H2] = [map f H1, map f H2].
LaTeX
$$$$ \\mathrm{map}_f([H_1, H_2]) = [\\mathrm{map}_f(H_1), \\mathrm{map}_f(H_2)]. $$$$
Lean4
theorem map_commutator (f : G →* G') : map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆ :=
by
simp_rw [le_antisymm_iff, map_le_iff_le_comap, commutator_le, mem_comap, map_commutatorElement]
constructor
· intro p hp q hq
exact commutator_mem_commutator (mem_map_of_mem _ hp) (mem_map_of_mem _ hq)
· rintro _ ⟨p, hp, rfl⟩ _ ⟨q, hq, rfl⟩
rw [← map_commutatorElement]
exact mem_map_of_mem _ (commutator_mem_commutator hp hq)
