English
Let f: α → M and h be as above. Then any monoid homomorphism g from the quotient that agrees with f on generators must be equal to the canonical lift.
Русский
Пусть f: α → M и h удовлетворяют условию. Любой моноид-гомоморфизм g из квартифицного моноида, сходящийся на образах генераторов с f, должен быть равен каноническому подъёму.
LaTeX
$$$\forall g:\operatorname{MonoidHom}((\operatorname{conGen rels}).\operatorname{Quotient} M),\; \forall hg:\forall a:\alpha, g(\operatorname{of rels} a) = f a\; \Rightarrow\; g = \operatorname{lift} f h$$$
Lean4
@[to_additive]
theorem unique (g : MonoidHom (conGen rels).Quotient M) (hg : ∀ a : α, g (of rels a) = f a) : g = lift f h :=
Con.lift_unique (Con.conGen_le h) g (FreeMonoid.hom_eq hg)
