English
If two groups G and H are isomorphic, then their abelianizations are isomorphic. The isomorphism on abelianizations is induced by the original isomorphism and acts by sending the abelianization class of g to the abelianization class of its image under the isomorphism.
Русский
Если две группы G и H изоморфны, то их абелизациям также подставляется изоморфизм. Изоморфизм на абелизациях индуцирован изоморфизмом и отправляет класс абелизации элемента g в класс абелизации образа e(g).
LaTeX
$$$ (G^{ab}) \cong (H^{ab}) $$$
Lean4
/-- Equivalent groups have equivalent abelianizations -/
def abelianizationCongr (e : G ≃* H) : Abelianization G ≃* Abelianization H
where
toFun := Abelianization.map e.toMonoidHom
invFun := Abelianization.map e.symm.toMonoidHom
left_inv := by
rintro ⟨a⟩
simp
right_inv := by
rintro ⟨a⟩
simp
map_mul' := MonoidHom.map_mul _
