English
Let G and H be groups, with subgroups A ≤ G and B ≤ G and φ: A ≃* B. If f: G →* H is a group homomorphism and x ∈ H satisfies x f(a) = f(φ(a)) x for all a ∈ A, then the canonical lift from G to the HNN extension satisfies lift f x hx (of g) = f(g) for every g ∈ G. Intuitively, the lift agrees with f on the base copy of G inside the HNN extension.
Русский
Пусть G и H — группы, A ≤ G и B ≤ G — подгруппы, а φ: A ≃* B. Пусть f: G →* H — гомоморфизм, и x ∈ H удовлетворяет x f(a) = f(φ(a)) x для всех a ∈ A. Тогда отображение подъёма lift f x hx, применяемое к образу g через естественное вложение G в HNN-расширение, равно f(g) для каждого g ∈ G. Интуитивно, подъём совпадает с f на базовом копии G внутри HNN-расширения.
LaTeX
$$$\\forall g \\in G: \\mathrm{lift}\\;f\\;x\\;hx\\;(\\mathrm{of}\\;g) = f(g), \\quad \\text{where } hx \\; \\text{means } x f(a) = f(\\varphi(a)) x \\text{ for all } a \\in A.$$$
Lean4
@[simp]
theorem lift_of (f : G →* H) (x : H) (hx : ∀ a : A, x * f ↑a = f (φ a : G) * x) (g : G) : lift f x hx (of g) = f g := by
delta HNNExtension; simp [lift, of]
