English
Given a map f: α → M into a monoid M that respects the relations rels via h, there exists a unique monoid homomorphism from the presented monoid to M extending f.
Русский
Для отображения f: α → M в моноид M, удовлетворяющего отношениям rels через h, существует единственный однородный моноид-гомоморфизм из представленного моноида в M, распроcтраняющий f.
LaTeX
$$$\exists!\; \phi: \operatorname{PresentedMonoid rels} \to^* M \;\text{such that}\; \phi\circ \operatorname{PresentedMonoid.of rels} = f$$$
Lean4
/-- The extension of a map `f : α → M` that satisfies the given relations to a monoid homomorphism
from `PresentedMonoid rels → M`. -/
@[to_additive /-- The extension of a map `f : α → M` that satisfies the given relations to an
additive-monoid homomorphism from `PresentedAddMonoid rels → M` -/
]
def lift : PresentedMonoid rels →* M :=
Con.lift _ (FreeMonoid.lift f) (Con.conGen_le h)
