English
Given f: R → Conj G, the corresponding map from EnvelGroup(R) to G satisfies the universal property: the composed map with toEnvelGroup recovers f.
Русский
Пусть f: R → Conj G. Тогда соответствующий гомоморфизм EnvelGroup(R) →* G удовлетворяет универсальному свойству: композиция с toEnvelGroup восстанавливает f.
LaTeX
$$$\big(\mathrm{Quandle.Conj.map} (\mathrm{toEnvelGroup.map}\ f)\big) \circ (\mathrm{toEnvelGroup}\ R) = f.$$$
Lean4
/-- The homomorphism `toEnvelGroup.map f` is the unique map that fits into the commutative
triangle in `toEnvelGroup.univ`.
-/
theorem univ_uniq (R : Type*) [Rack R] (G : Type*) [Group G] (f : R →◃ Quandle.Conj G) (g : EnvelGroup R →* G)
(h : f = (Quandle.Conj.map g).comp (toEnvelGroup R)) : g = toEnvelGroup.map f :=
h.symm ▸ (toEnvelGroup.map.apply_symm_apply g).symm
