English
The relation con identifies images of A and B under the isomorphism φ inside the coproduct G ∗ Multiplicative ℤ, generating the HNN extension by quotienting by this relation.
Русский
Отношение con определяет тождество образов A и B под φ внутри копродукта G ∗ ℤ, образуя HNN-расширение как фактор по этому отношению.
LaTeX
$$$ con(G,A,B,φ) := conGen\\big(\\dots\\big)$$$
Lean4
/-- The relation we quotient the coproduct by to form an `HNNExtension`. -/
def con (G : Type*) [Group G] (A B : Subgroup G) (φ : A ≃* B) : Con (G ∗ Multiplicative ℤ) :=
conGen (fun x y => ∃ (a : A), x = inr (ofAdd 1) * inl (a : G) ∧ y = inl (φ a : G) * inr (ofAdd 1))
