English
Uniqueness of morphisms from an HNN extension: if f,g : HNN(G,A,B,φ) →* M satisfy f ∘ of = g ∘ of and f(t) = g(t), then f = g. Thus a homomorphism is determined by its values on the base copy and on the stable letter t.
Русский
Уникальность гомоморфизмов из HNN-расширения: пусть f, g : HNN(G,A,B,φ) →* M удовлетворяют f ∘ of = g ∘ of и f(t) = g(t); тогда f = g. Таким образом, гомоморфизм определяется его значениями на базовой копии и на стабильной букве t.
LaTeX
$$$f,g: \\text{HNN}(G,A,B,\\varphi) \\to_* M$. If $f \\circ \\mathrm{of} = g \\circ \\mathrm{of}$ and $f(t) = g(t)$, then $f = g$.$$
Lean4
@[ext high]
theorem hom_ext {f g : HNNExtension G A B φ →* M} (hg : f.comp of = g.comp of) (ht : f t = g t) : f = g :=
(MonoidHom.cancel_right Con.mk'_surjective).mp <| Coprod.hom_ext hg (MonoidHom.ext_mint ht)
