English
There is a canonical homomorphism mk rels from the free group on α to the presented group, sending a generator to its equivalence class in the quotient.
Русский
Существует каноническое гомоморфизм mk rels от свободной группы на α к представленной группе, отправляющий генератор в его класс в фактор-группе.
LaTeX
$$$\mathrm{mk}_{\mathrm{rels}} : \mathrm{FreeGroup}(\alpha) \to \mathrm{PresentedGroup}(\mathrm{rels})$ является природным гомоморфизмом, который на образе генератора x даёт его класс в факторе.$$
Lean4
/-- The canonical map from the free group on `α` to a presented group with generators `x : α`,
where `x` is mapped to its equivalence class under the given set of relations `rels` -/
def mk (rels : Set (FreeGroup α)) : FreeGroup α →* PresentedGroup rels :=
⟨⟨QuotientGroup.mk, rfl⟩, fun _ _ => rfl⟩
