English
The HNN extension HNNExtension G A B φ is the quotient of the coproduct G ∗ Multiplicative ℤ by the normal closure of the relation con; it adjoins a stable letter t with the isomorphism φ identifying A with B by conjugation by t.
Русский
HNN-расширение HNNExtension G A B φ есть фактор-по-нормальномзамечании coprod G ∗ ⟨t⟩ по отношению con; оно прибавляет устойчивую букву t так, что элементы A и φ(A) идентифицируются через сопряжение t.
LaTeX
$$$ HNNExtension\\ G\\ A\\ B\\ φ = (HNNExtension.con\\ G\\ A\\ B\\ φ).Quotient $$$
Lean4
/-- The HNN Extension of a group `G`, `HNNExtension G A B φ`. Given a group `G`, subgroups `A` and
`B` and an isomorphism `φ` of `A` and `B`, we adjoin a letter `t` to `G`, such that for
any `a ∈ A`, the conjugate of `of a` by `t` is `of (φ a)`, where `of` is the canonical
map from `G` into the `HNNExtension`. -/
def HNNExtension (G : Type*) [Group G] (A B : Subgroup G) (φ : A ≃* B) : Type _ :=
(HNNExtension.con G A B φ).Quotient
