English
Let G and H be groups and f: G →* H a group homomorphism. Then there is a natural morphism from the conjugation quandle of G to the conjugation quandle of H, sending each element g ∈ G to f(g), and this construction respects the quandle operation. In other words, conjugation is functorial with respect to group homomorphisms.
Русский
Пусть G и H — группы, f: G →* H — гомоморфизм групп. Тогда существует естественное отображение между сопряжёнными куандлами G и H, отправляющее элемент g ∈ G в f(g), и это отображение сохраняет операцию куандла. То есть сопряжение задаёт функторность по гомоморфизмам групп.
LaTeX
$$$\forall g,h \in G:\ f(g \triangleleft h) = f(g) \triangleleft f(h),$ where $g \triangleleft h$ denotes the conjugation operation in the conjugation quandle of $G$.$$
Lean4
/-- `Conj` is functorial
-/
def map {G : Type*} {H : Type*} [Group G] [Group H] (f : G →* H) : Conj G →◃ Conj H
where
toFun := f
map_act' := by simp
