English
There is a natural rack homomorphism from any rack R to the conjugation quandle of the group of automorphisms of R, sending x to the corresponding inner action ad_x.
Русский
Существует естественное отображение-раку из индекса (rack) R в сопряжённый куандл группы аутоморфизмов R, отправляющее x в соответствующее внутреннее действие ad_x.
LaTeX
$$$\text{toConj}: R \to\mathrm{Conj}(R\simeq R)\quad \text{is a rack homomorphism with } (toConj)(x) = \mathrm{act}'_x.$$$
Lean4
/-- This is the natural rack homomorphism to the conjugation quandle of the group `R ≃ R`
that acts on the rack. -/
def toConj (R : Type*) [Rack R] : R →◃ Quandle.Conj (R ≃ R)
where
toFun := act'
map_act' := by
intro x y
exact ad_conj x y
