English
A MonoidHom f induces a well-defined map on conjugacy classes sending the class of a to the class of f(a). If a ~ a', then f(a) ~ f(a').
Русский
Любой гомоморфизм f индуцирует отображение на классах сопряжённости: [a] ↦ [f(a)]. Если a ~ a', то f(a) ~ f(a').
LaTeX
$$$\text{map}(f)(\mathrm{ConjClasses.mk}(a)) = \mathrm{ConjClasses.mk}(f(a))$ and if $a_1 \sim a_2$ then $f(a_1) \sim f(a_2)$.$$
Lean4
/-- A `MonoidHom` maps conjugacy classes of one group to conjugacy classes of another. -/
def map (f : α →* β) : ConjClasses α → ConjClasses β :=
Quotient.lift (ConjClasses.mk ∘ f) fun _ _ ab => mk_eq_mk_iff_isConj.2 (f.map_isConj ab)
