toGroup — Mathlib

English

Given a relation-preserving map from α to G, there is a unique homomorphism from the presented group extending it.

Русский

Существуют единственные гомоморфизмы, расширяющие отображение из генераторов, сохраняющее отношения.

LaTeX

$$If $h$ respects rels on generators, there is a unique $g: \mathrm{PresentedGroup}(\mathrm{rels}) \to G$ with $g\circ \mathrm{of} = f$.$$

Lean4

/-- The extension of a map `f : α → G` that satisfies the given relations to a group homomorphism
from `PresentedGroup rels → G`. -/
def toGroup (h : ∀ r ∈ rels, FreeGroup.lift f r = 1) : PresentedGroup rels →* G :=
  QuotientGroup.lift (Subgroup.normalClosure rels) F (to_group_eq_one_of_mem_closure h)

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