Conjugating the base group by the stable letter of an HNN extension

Let HNNExtension G A B φ be the HNN extension of G along an isomorphism φ : A ≃* B of subgroups, with stable letter t, so that t * a * t⁻¹ = φ a for a ∈ A. Britton's lemma (HNNExtension.ReducedWord.toList_eq_nil_of_mem_of_range) shows that these are the only elements of G that t conjugates back into G: t * g * t⁻¹ lies in G exactly when g ∈ A, and t⁻¹ * g * t lies in G exactly when g ∈ B. Consequently g ∈ G commutes with t exactly when g ∈ A and φ g = g; for the HNN extension along the identity of A, exactly when g ∈ A.

This controls commutation transitivity in an HNN extension along the identity of A. If c ∈ A is nontrivial then t commutes with c, so if commutation is transitive through c then every element of G commuting with c commutes with t and therefore lies in A. Extensions of centralizers ⟨G, t | [c, t] = 1, c ∈ C_G(u)⟩ therefore have to use the full centralizer C_G(u): for u ≠ 1, replacing it by a smaller subgroup A ∋ u with C_G(u) ⊄ A produces a group that is not commutative transitive, hence not CSA. In a torsion-free group this happens for A = zpowers u whenever u is a nontrivial proper power, since a root of u commutes with u without lying in zpowers u.

Main results

• HNNExtension.t_mul_of_mul_inv_t_mem_range_iff: t * g * t⁻¹ ∈ G ↔ g ∈ A.
• HNNExtension.inv_t_mul_of_mul_t_mem_range_iff: t⁻¹ * g * t ∈ G ↔ g ∈ B.
• HNNExtension.commute_of_t_iff: g commutes with t iff g ∈ A and φ g = g.
• HNNExtension.commute_of_t_iff_mem: along the identity of A, g commutes with t iff g ∈ A.
• HNNExtension.centralizer_le_of_isCommTransitive: if the HNN extension along the identity of A is commutative transitive, then A contains the centralizer in G of each of its nontrivial elements.
• HNNExtension.not_isCommTransitive_zpowers_of_isProperPower: over a torsion-free group, the HNN extension along the identity of the cyclic subgroup generated by a nontrivial proper power is not commutative transitive.

References

• R. C. Lyndon, P. E. Schupp, Combinatorial Group Theory, Springer (1977), Chapter IV, §2 (Britton's lemma).
• O. Kharlampovich, A. Myasnikov, Irreducible affine varieties over a free group. I, J. Algebra 200 (1998), §1, Definition 5 (free extensions of centralizers).

theorem HNNExtension.t_mul_of_mul_inv_t_mem_range_iff {G : Type u_1} [Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} {g : G} : t * of g * t⁻¹ ∈ of.range ↔ g ∈ A

The stable letter conjugates g into the base group exactly when g ∈ A.

theorem HNNExtension.inv_t_mul_of_mul_t_mem_range_iff {G : Type u_1} [Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} {g : G} : t⁻¹ * of g * t ∈ of.range ↔ g ∈ B

The inverse of the stable letter conjugates g into the base group exactly when g ∈ B.

theorem HNNExtension.commute_of_t_iff {G : Type u_1} [Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} {g : G} : Commute (of g) t ↔ ∃ (hg : g ∈ A), ↑(φ ⟨g, hg⟩) = g

An element of the base group commutes with the stable letter exactly when it lies in A and is fixed by φ.

@[simp]

theorem HNNExtension.commute_of_t_iff_mem {G : Type u_1} [Group G] {A : Subgroup G} {g : G} : Commute (of g) t ↔ g ∈ A

In the HNN extension along the identity of A, an element of the base group commutes with the stable letter exactly when it lies in A.

theorem HNNExtension.centralizer_le_of_isCommTransitive {G : Type u_1} [Group G] {A : Subgroup G} (h : Group.IsCommTransitive (HNNExtension G A A (MulEquiv.refl ↥A))) {c : G} (hcA : c ∈ A) (hc : c ≠ 1) : Subgroup.centralizer {c} ≤ A

If the HNN extension along the identity of A is commutative transitive, then A contains the centralizer in G of each of its nontrivial elements.

theorem HNNExtension.not_isCommTransitive_zpowers_of_isProperPower {G : Type u_1} [Group G] [IsMulTorsionFree G] {u : G} (hu : Group.IsProperPower u) (hu1 : u ≠ 1) : ¬Group.IsCommTransitive (HNNExtension G (Subgroup.zpowers u) (Subgroup.zpowers u) (MulEquiv.refl ↥(Subgroup.zpowers u)))

Over a torsion-free group, the HNN extension along the identity of zpowers u for a nontrivial proper power u is not commutative transitive: a root of u commutes with u, and u with the stable letter, but the root does not commute with the stable letter.