univ — Mathlib

English

There is an equivalence between shelf homomorphisms R → Conj G and monoid homomorphisms EnvelGroup(R) →* G.

Русский

Существует эквиваленция между отображениями-куандлами R → Conj G и гомоморфизмами EnvelGroup(R) →* G.

LaTeX

$$$\mathrm{Equiv}\big(\mathrm{ShelfHom}(R,\mathrm{Conj}\,G),\mathrm{EnvelGroup}(R) \to^* G\big).$$$

Lean4

/-- Given a homomorphism from a rack to a group, it factors through the enveloping group.
-/
theorem univ (R : Type*) [Rack R] (G : Type*) [Group G] (f : R →◃ Quandle.Conj G) :
    (Quandle.Conj.map (toEnvelGroup.map f)).comp (toEnvelGroup R) = f :=
  toEnvelGroup.map.symm_apply_apply f

Похожие утверждения