English
Given a rack R and a group G with a shelf homomorphism f, mapAux defines the canonical map from the enveloping structure on R to G by recursion on the PreEnvelGroup constructors.
Русский
Дано раку R и группе G с отображением- shelf-гомоморфизмом f, mapAux задаёт каноническое отображение от обобщающей (enveloping) структуры R в G по рекурсии по конструктору PreEnvelGroup.
LaTeX
$$$\text{mapAux}_f("unit") = 1,\quad \text{mapAux}_f("incl\,x") = f(x),\quad \text{mapAux}_f(a\,\cdot\, b) = \text{mapAux}_f(a)\cdot\text{mapAux}_f(b),\quad \text{mapAux}_f(a^{-1}) = (\text{mapAux}_f(a))^{-1}.$$$
Lean4
/-- The preliminary definition of the induced map from the enveloping group.
See `toEnvelGroup.map`.
-/
def mapAux {R : Type*} [Rack R] {G : Type*} [Group G] (f : R →◃ Quandle.Conj G) : PreEnvelGroup R → G
| .unit => 1
| .incl x => f x
| .mul a b => toEnvelGroup.mapAux f a * toEnvelGroup.mapAux f b
| .inv a => (toEnvelGroup.mapAux f a)⁻¹
