English
There is a universal homomorphism from HNNExtension G A B φ to any H given a hom f: G → H and an element x ∈ H satisfying hx = xφ(a) for all a ∈ A; this homomorphism extends f and sends t to x, uniquely.
Русский
Существует универсальное гомоморфное отображение из HNNExtension G A B φ в любое H при данного гомоморфизма f: G → H и элемента x ∈ H, удовлетворяющего требованию hx = f(φ(a))x; такое отображение распространяется на f и отправляет t в x, единственно.
LaTeX
$$$ \\exists! \\ell: HNNExtension G A B φ \\to^* H \\; (\\ell\\circ of = f) \\land (\\ell(t) = x)$ при условии $ hx = f(φ(a))x \\ (a ∈ A) $$$
Lean4
/-- Define a function `HNNExtension G A B φ →* H`, by defining it on `G` and `t` -/
def lift (f : G →* H) (x : H) (hx : ∀ a : A, x * f ↑a = f (φ a : G) * x) : HNNExtension G A B φ →* H :=
Con.lift _ (Coprod.lift f (zpowersHom H x))
(Con.conGen_le <| by
rintro _ _ ⟨a, rfl, rfl⟩
simp [hx])
