English
The equality mapAux interacts with products in PreEnvelGroup, i.e. the map respects the product operation up to the corresponding algebraic multiplication in G.
Русский
Отображение mapAux взаимодействоет с операцией умножения в PreEnvelGroup, т.е. отображение сохраняет произведение согласно умножению в G.
LaTeX
$$$\forall a,b:\ Rack.toEnvelGroup.mapAux\ f (a \cdot b) = (Rack.toEnvelGroup.mapAux\ f\ a) \; \text{\ensuremath{\ast}}\; (Rack.toEnvelGroup.mapAux\ f\ b).$$$
Lean4
/-- Given a map from a rack to a group, lift it to being a map from the enveloping group.
More precisely, the `EnvelGroup` functor is left adjoint to `Quandle.Conj`.
-/
def map {R : Type*} [Rack R] {G : Type*} [Group G] : (R →◃ Quandle.Conj G) ≃ (EnvelGroup R →* G)
where
toFun
f :=
{ toFun := fun x => Quotient.liftOn x (toEnvelGroup.mapAux f) fun _ _ ⟨hab⟩ => toEnvelGroup.mapAux.well_def f hab
map_one' := by
change Quotient.liftOn ⟦Rack.PreEnvelGroup.unit⟧ (toEnvelGroup.mapAux f) _ = 1
simp only [Quotient.lift_mk, mapAux]
map_mul' := fun x y =>
Quotient.inductionOn₂ x y fun x y =>
by
change Quotient.liftOn ⟦mul x y⟧ (toEnvelGroup.mapAux f) _ = _
simp [toEnvelGroup.mapAux] }
invFun F := (Quandle.Conj.map F).comp (toEnvelGroup R)
right_inv
F :=
MonoidHom.ext fun x =>
Quotient.inductionOn x fun x => by
induction x with
| unit => exact F.map_one.symm
| incl => rfl
| mul x y ih_x ih_y =>
have hm : ⟦x.mul y⟧ = @Mul.mul (EnvelGroup R) _ ⟦x⟧ ⟦y⟧ := rfl
simp only [MonoidHom.coe_mk, OneHom.coe_mk, Quotient.lift_mk]
suffices ∀ x y, F (Mul.mul x y) = F (x) * F (y)
by
simp_all only [MonoidHom.coe_mk, OneHom.coe_mk, Quotient.lift_mk]
rw [← ih_x, ← ih_y, mapAux]
exact F.map_mul
| inv x ih_x =>
have hm : ⟦x.inv⟧ = @Inv.inv (EnvelGroup R) _ ⟦x⟧ := rfl
rw [hm, F.map_inv, MonoidHom.map_inv, ih_x]
