English
Let G be a group with A, B subgroups and φ: A ≃* B. The natural embedding of G into the HNN extension HNN(G, A, B, φ) is injective.
Русский
Пусть G — группа, A и B — подгруппы, φ: A ≃* B. естественное вложение G в расширение HNN(G, A, B, φ) инъективно.
LaTeX
$$$\\ker(\\iota) = \\{e_G\\}$, where $\\iota: G \\to \\mathrm{HNN}(G, A, B, φ)$ is the natural embedding.$$
Lean4
theorem of_injective : Function.Injective (of : G → HNNExtension G A B φ) :=
by
rcases TransversalPair.nonempty G A B with ⟨d⟩
refine Function.Injective.of_comp (f := ((· • ·) : HNNExtension G A B φ → NormalWord d → NormalWord d)) ?_
intro _ _ h
exact eq_of_smul_eq_smul (fun w : NormalWord d => by simp_all [funext_iff, of_smul_eq_smul])
