English
There is a natural isomorphism between the subgroups in the two endpoints of the HNN extension, given by φ when u = 1 and φ^{-1} when u = -1.
Русский
Существует естественное изоморство между подгруппами на двух концах HNN-расширения, задаваемое φ при u = 1 и φ^{-1} при u = -1.
LaTeX
$$$toSubgroupEquiv(u): toSubgroup A B u \\cong toSubgroup A B (-u),\\quad toSubgroupEquiv(1) = φ,\\quad toSubgroupEquiv(-1) = φ^{-1}$$$
Lean4
/-- To avoid duplicating code, we define `toSubgroup A B u` and `toSubgroupEquiv u`
where `u : ℤˣ` is `1` or `-1`. `toSubgroup A B u` is `A` when `u = 1` and `B` when `u = -1`,
and `toSubgroupEquiv` is the group isomorphism from `toSubgroup A B u` to `toSubgroup A B (-u)`.
It is defined to be `φ` when `u = 1` and `φ⁻¹` when `u = -1`. -/
def toSubgroupEquiv (u : ℤˣ) : toSubgroup A B u ≃* toSubgroup A B (-u) :=
if hu : u = 1 then hu ▸ φ else by convert φ.symm <;> cases Int.units_eq_one_or u <;> simp_all
