# Documentation

## HNN Extensions of Groups #

This file defines 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. This construction is named after Graham Higman, Bernhard Neumann and Hanna Neumann.

## Main definitions #

• HNNExtension G A B φ : The HNN Extension of a group G, where A and B are subgroups and φ is an isomorphism between A and B.
• HNNExtension.of : The canonical embedding of G into HNNExtension G A B φ.
• HNNExtension.t : The stable letter of the HNN extension.
• HNNExtension.lift : Define a function HNNExtension G A B φ →* H, by defining it on G and t
• HNNExtension.of_injective : The canonical embedding G →* HNNExtension G A B φ is injective.
• HNNExtension.ReducedWord.toList_eq_nil_of_mem_of_range : Britton's Lemma. If an element of G is represented by a reduced word, then this reduced word does not contain t.
def HNNExtension.con (G : Type u_1) [] (A : ) (B : ) (φ : A ≃* B) :

The relation we quotient the coproduct by to form an HNNExtension.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def HNNExtension (G : Type u_1) [] (A : ) (B : ) (φ : A ≃* B) :
Type u_1

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.

Equations
Instances For
instance instGroupHNNExtension {G : Type u_1} [] {A : } {B : } {φ : A ≃* B} :
Group (HNNExtension G A B φ)
Equations
• instGroupHNNExtension = id inferInstance
def HNNExtension.of {G : Type u_1} [] {A : } {B : } {φ : A ≃* B} :
G →* HNNExtension G A B φ

The canonical embedding G →* HNNExtension G A B φ

Equations
Instances For
def HNNExtension.t {G : Type u_1} [] {A : } {B : } {φ : A ≃* B} :
HNNExtension G A B φ

The stable letter of the HNNExtension

Equations
• HNNExtension.t = ((HNNExtension.con G A B φ).mk'.comp Monoid.Coprod.inr) (Multiplicative.ofAdd 1)
Instances For
theorem HNNExtension.t_mul_of {G : Type u_1} [] {A : } {B : } {φ : A ≃* B} (a : A) :
HNNExtension.t * HNNExtension.of a = HNNExtension.of (φ a) * HNNExtension.t
theorem HNNExtension.of_mul_t {G : Type u_1} [] {A : } {B : } {φ : A ≃* B} (b : B) :
HNNExtension.of b * HNNExtension.t = HNNExtension.t * HNNExtension.of (φ.symm b)
theorem HNNExtension.equiv_eq_conj {G : Type u_1} [] {A : } {B : } {φ : A ≃* B} (a : A) :
HNNExtension.of (φ a) = HNNExtension.t * HNNExtension.of a * HNNExtension.t⁻¹
theorem HNNExtension.equiv_symm_eq_conj {G : Type u_1} [] {A : } {B : } {φ : A ≃* B} (b : B) :
HNNExtension.of (φ.symm b) = HNNExtension.t⁻¹ * HNNExtension.of b * HNNExtension.t
theorem HNNExtension.inv_t_mul_of {G : Type u_1} [] {A : } {B : } {φ : A ≃* B} (b : B) :
HNNExtension.t⁻¹ * HNNExtension.of b = HNNExtension.of (φ.symm b) * HNNExtension.t⁻¹
theorem HNNExtension.of_mul_inv_t {G : Type u_1} [] {A : } {B : } {φ : A ≃* B} (a : A) :
HNNExtension.of a * HNNExtension.t⁻¹ = HNNExtension.t⁻¹ * HNNExtension.of (φ a)
def HNNExtension.lift {G : Type u_1} [] {A : } {B : } {φ : A ≃* B} {H : Type u_2} [] (f : G →* H) (x : H) (hx : ∀ (a : A), x * f a = f (φ a) * x) :
HNNExtension G A B φ →* H

Define a function HNNExtension G A B φ →* H, by defining it on G and t

Equations
Instances For
@[simp]
theorem HNNExtension.lift_t {G : Type u_1} [] {A : } {B : } {φ : A ≃* B} {H : Type u_2} [] (f : G →* H) (x : H) (hx : ∀ (a : A), x * f a = f (φ a) * x) :
(HNNExtension.lift f x hx) HNNExtension.t = x
@[simp]
theorem HNNExtension.lift_of {G : Type u_1} [] {A : } {B : } {φ : A ≃* B} {H : Type u_2} [] (f : G →* H) (x : H) (hx : ∀ (a : A), x * f a = f (φ a) * x) (g : G) :
(HNNExtension.lift f x hx) (HNNExtension.of g) = f g
theorem HNNExtension.hom_ext_iff {G : Type u_1} [] {A : } {B : } {φ : A ≃* B} {M : Type u_3} [] {f : HNNExtension G A B φ →* M} {g : HNNExtension G A B φ →* M} :
f = g f.comp HNNExtension.of = g.comp HNNExtension.of f HNNExtension.t = g HNNExtension.t
theorem HNNExtension.hom_ext {G : Type u_1} [] {A : } {B : } {φ : A ≃* B} {M : Type u_3} [] {f : HNNExtension G A B φ →* M} {g : HNNExtension G A B φ →* M} (hg : f.comp HNNExtension.of = g.comp HNNExtension.of) (ht : f HNNExtension.t = g HNNExtension.t) :
f = g
theorem HNNExtension.induction_on {G : Type u_1} [] {A : } {B : } {φ : A ≃* B} {motive : HNNExtension G A B φProp} (x : HNNExtension G A B φ) (of : ∀ (g : G), motive (HNNExtension.of g)) (t : motive HNNExtension.t) (mul : ∀ (x y : HNNExtension G A B φ), motive xmotive ymotive (x * y)) (inv : ∀ (x : HNNExtension G A B φ), motive xmotive x⁻¹) :
motive x
def HNNExtension.toSubgroup {G : Type u_1} [] (A : ) (B : ) (u : ) :

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 φ when u = 1 and φ⁻¹ when u = -1. toSubgroup u is the subgroup such that for any a ∈ toSubgroup u, t ^ (u : ℤ) * a = toSubgroupEquiv a * t ^ (u : ℤ).

Equations
• = if u = 1 then A else B
Instances For
@[simp]
theorem HNNExtension.toSubgroup_one {G : Type u_1} [] (A : ) (B : ) :
= A
@[simp]
theorem HNNExtension.toSubgroup_neg_one {G : Type u_1} [] (A : ) (B : ) :
def HNNExtension.toSubgroupEquiv {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) (u : ) :

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 ismorphism from toSubgroup A B u to toSubgroup A B (-u). It is defined to be φ when u = 1 and φ⁻¹ when u = -1.

Equations
• = if hu : u = 1 then φ else .mpr φ.symm
Instances For
@[simp]
theorem HNNExtension.toSubgroupEquiv_one {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) :
@[simp]
theorem HNNExtension.toSubgroupEquiv_neg_one {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) :
= φ.symm
@[simp]
theorem HNNExtension.toSubgroupEquiv_neg_apply {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) (u : ) (a : ) :
( ( a)) = a
structure HNNExtension.NormalWord.TransversalPair (G : Type u_1) [] (A : ) (B : ) :
Type u_1

To put word in the HNN Extension into a normal form, we must choose an element of each right coset of both A and B, such that the chosen element of the subgroup itself is 1.

• set : Set G

The transversal of each subgroup

• compl : ∀ (u : ), Subgroup.IsComplement (↑) (self.set u)

We have exactly one element of each coset of the subgroup

Instances For
theorem HNNExtension.NormalWord.TransversalPair.compl {G : Type u_1} [] {A : } {B : } (self : ) (u : ) :
Subgroup.IsComplement (↑) (self.set u)

We have exactly one element of each coset of the subgroup

instance HNNExtension.NormalWord.TransversalPair.nonempty (G : Type u_1) [] (A : ) (B : ) :
Equations
• =
structure HNNExtension.NormalWord.ReducedWord (G : Type u_1) [] (A : ) (B : ) :
Type u_1

A reduced word is a head, which is an element of G, followed by the product list of pairs. There should also be no sequences of the form t^u * g * t^-u, where g is in toSubgroup A B u This is a less strict condition than required for NormalWord.

Every ReducedWord is the product of an element of the group and a word made up of letters each of which is in the transversal. head is that element of the base group.

• toList : List ( × G)

The list of pairs (ℤˣ × G), where each pair (u, g) represents the element t^u * g of HNNExtension G A B φ

• chain : List.Chain' (fun (a b : × G) => a.2 a.1 = b.1) self.toList

There are no sequences of the form t^u * g * t^-u where g ∈ toSubgroup A B u

Instances For
theorem HNNExtension.NormalWord.ReducedWord.chain {G : Type u_1} [] {A : } {B : } (self : ) :
List.Chain' (fun (a b : × G) => a.2 a.1 = b.1) self.toList

There are no sequences of the form t^u * g * t^-u where g ∈ toSubgroup A B u

@[simp]
theorem HNNExtension.NormalWord.ReducedWord.empty_head (G : Type u_1) [] (A : ) (B : ) :
@[simp]
theorem HNNExtension.NormalWord.ReducedWord.empty_toList (G : Type u_1) [] (A : ) (B : ) :
.toList = []
def HNNExtension.NormalWord.ReducedWord.empty (G : Type u_1) [] (A : ) (B : ) :

The empty reduced word.

Equations
• = { head := 1, toList := [], chain := }
Instances For
def HNNExtension.NormalWord.ReducedWord.prod {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) :
HNNExtension G A B φ

The product of a ReducedWord as an element of the HNNExtension

Equations
• = HNNExtension.of w.head * (List.map (fun (x : × G) => HNNExtension.t ^ x.1 * HNNExtension.of x.2) w.toList).prod
Instances For
structure HNNExtension.NormalWord {G : Type u_1} [] {A : } {B : } (d : ) extends :
Type u_1

Given a TransversalPair, we can make a normal form for words in the HNNExtension G A B φ. The normal form is a head, which is an element of G, followed by the product list of pairs, t ^ u * g, where u is 1 or -1 and g is the chosen element of its right coset of toSubgroup A B u. There should also be no sequences of the form t^u * g * t^-u where g ∈ toSubgroup A B u

• toList : List ( × G)
• chain : List.Chain' (fun (a b : × G) => a.2 a.1 = b.1) self.toList
• mem_set : ∀ (u : ) (g : G), (u, g) self.toListg d.set u

Every element g : G in the list is the chosen element of its coset

Instances For
theorem HNNExtension.NormalWord.mem_set {G : Type u_1} [] {A : } {B : } {d : } (self : ) (u : ) (g : G) :
(u, g) self.toListg d.set u

Every element g : G in the list is the chosen element of its coset

theorem HNNExtension.NormalWord.ext_iff {G : Type u_1} [] {A : } {B : } {d : } {w : } {w' : } :
theorem HNNExtension.NormalWord.ext {G : Type u_1} [] {A : } {B : } {d : } {w : } {w' : } (h1 : w.head = w'.head) (h2 : w.toList = w'.toList) :
w = w'
@[simp]
theorem HNNExtension.NormalWord.empty_toList {G : Type u_1} [] {A : } {B : } {d : } :
HNNExtension.NormalWord.empty.toList = []
@[simp]
theorem HNNExtension.NormalWord.empty_head {G : Type u_1} [] {A : } {B : } {d : } :
def HNNExtension.NormalWord.empty {G : Type u_1} [] {A : } {B : } {d : } :

The empty word

Equations
• HNNExtension.NormalWord.empty = { head := 1, toList := [], chain := , mem_set := }
Instances For
@[simp]
theorem HNNExtension.NormalWord.ofGroup_toList {G : Type u_1} [] {A : } {B : } {d : } (g : G) :
.toList = []
@[simp]
theorem HNNExtension.NormalWord.ofGroup_head {G : Type u_1} [] {A : } {B : } {d : } (g : G) :
def HNNExtension.NormalWord.ofGroup {G : Type u_1} [] {A : } {B : } {d : } (g : G) :

The NormalWord representing an element g of the group G, which is just the element g itself.

Equations
• = { head := g, toList := [], chain := , mem_set := }
Instances For
instance HNNExtension.NormalWord.instInhabited {G : Type u_1} [] {A : } {B : } {d : } :
Equations
• HNNExtension.NormalWord.instInhabited = { default := HNNExtension.NormalWord.empty }
instance HNNExtension.NormalWord.instMulAction {G : Type u_1} [] {A : } {B : } {d : } :
Equations
• HNNExtension.NormalWord.instMulAction =
theorem HNNExtension.NormalWord.group_smul_def {G : Type u_1} [] {A : } {B : } {d : } (g : G) (w : ) :
g w = { head := g * w.head, toList := w.toList, chain := , mem_set := }
@[simp]
theorem HNNExtension.NormalWord.group_smul_head {G : Type u_1} [] {A : } {B : } {d : } (g : G) (w : ) :
@[simp]
theorem HNNExtension.NormalWord.group_smul_toList {G : Type u_1} [] {A : } {B : } {d : } (g : G) (w : ) :
(g w).toList = w.toList
instance HNNExtension.NormalWord.instFaithfulSMul {G : Type u_1} [] {A : } {B : } {d : } :
Equations
• =
@[simp]
theorem HNNExtension.NormalWord.cons_toList {G : Type u_1} [] {A : } {B : } {d : } (g : G) (u : ) (w : ) (h1 : w.head d.set u) (h2 : u'Option.map Prod.fst w.toList.head?, w.head u = u') :
(HNNExtension.NormalWord.cons g u w h1 h2).toList = (u, w.head) :: w.toList
@[simp]
theorem HNNExtension.NormalWord.cons_head {G : Type u_1} [] {A : } {B : } {d : } (g : G) (u : ) (w : ) (h1 : w.head d.set u) (h2 : u'Option.map Prod.fst w.toList.head?, w.head u = u') :
(HNNExtension.NormalWord.cons g u w h1 h2).head = g
def HNNExtension.NormalWord.cons {G : Type u_1} [] {A : } {B : } {d : } (g : G) (u : ) (w : ) (h1 : w.head d.set u) (h2 : u'Option.map Prod.fst w.toList.head?, w.head u = u') :

A constructor to append an element g of G and u : ℤˣ to a word w with sufficient hypotheses that no normalization or cancellation need take place for the result to be in normal form

Equations
Instances For
def HNNExtension.NormalWord.consRecOn {G : Type u_1} [] {A : } {B : } {d : } {motive : } (w : ) (ofGroup : (g : G) → motive ) (cons : (g : G) → (u : ) → (w : ) → (h1 : w.head d.set u) → (h2 : u'Option.map Prod.fst w.toList.head?, w.head u = u') → motive wmotive (HNNExtension.NormalWord.cons g u w h1 h2)) :
motive w

A recursor to induct on a NormalWord, by proving the propert is preserved under cons

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem HNNExtension.NormalWord.consRecOn_ofGroup {G : Type u_1} [] {A : } {B : } {d : } {motive : } (g : G) (ofGroup : (g : G) → motive ) (cons : (g : G) → (u : ) → (w : ) → (h1 : w.head d.set u) → (h2 : u'Option.map Prod.fst w.toList.head?, w.head u = u') → motive wmotive (HNNExtension.NormalWord.cons g u w h1 h2)) :
= ofGroup g
@[simp]
theorem HNNExtension.NormalWord.consRecOn_cons {G : Type u_1} [] {A : } {B : } {d : } {motive : } (g : G) (u : ) (w : ) (h1 : w.head d.set u) (h2 : u'Option.map Prod.fst w.toList.head?, w.head u = u') (ofGroup : (g : G) → motive ) (cons : (g : G) → (u : ) → (w : ) → (h1 : w.head d.set u) → (h2 : u'Option.map Prod.fst w.toList.head?, w.head u = u') → motive wmotive (HNNExtension.NormalWord.cons g u w h1 h2)) :
HNNExtension.NormalWord.consRecOn (HNNExtension.NormalWord.cons g u w h1 h2) ofGroup cons = cons g u w h1 h2 (HNNExtension.NormalWord.consRecOn w ofGroup cons)
@[simp]
theorem HNNExtension.NormalWord.smul_cons {G : Type u_1} [] {A : } {B : } {d : } (g₁ : G) (g₂ : G) (u : ) (w : ) (h1 : w.head d.set u) (h2 : u'Option.map Prod.fst w.toList.head?, w.head u = u') :
g₁ HNNExtension.NormalWord.cons g₂ u w h1 h2 = HNNExtension.NormalWord.cons (g₁ * g₂) u w h1 h2
@[simp]
theorem HNNExtension.NormalWord.smul_ofGroup {G : Type u_1} [] {A : } {B : } {d : } (g₁ : G) (g₂ : G) :
noncomputable def HNNExtension.NormalWord.unitsSMulGroup {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) (d : ) (u : ) (g : G) :
(HNNExtension.toSubgroup A B (-u)) × (d.set u)

The action of t^u on ofGroup g. The normal form will be a * t^u * g' where a ∈ toSubgroup A B (-u)

Equations
• = let g' := .equiv g; ( g'.1, g'.2)
Instances For
theorem HNNExtension.NormalWord.unitsSMulGroup_snd {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) (d : ) (u : ) (g : G) :
.2 = (.equiv g).2
def HNNExtension.NormalWord.Cancels {G : Type u_1} [] {A : } {B : } {d : } (u : ) (w : ) :

Cancels u w is a predicate expressing whether t^u cancels with some occurence of t^-u when when we multiply t^u by w.

Equations
Instances For
def HNNExtension.NormalWord.unitsSMulWithCancel {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } (u : ) (w : ) :

Multiplying t^u by w in the special case where cancellation happens

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def HNNExtension.NormalWord.unitsSMul {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } (u : ) (w : ) :

Multiplying t^u by a NormalWord, w and putting the result in normal form.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem HNNExtension.NormalWord.not_cancels_of_cons_hyp {G : Type u_1} [] {A : } {B : } {d : } (u : ) (w : ) (h2 : u'Option.map Prod.fst w.toList.head?, w.head u = u') :

A condition for not cancelling whose hypothese are the same as those of the cons function.

theorem HNNExtension.NormalWord.unitsSMul_cancels_iff {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } (u : ) (w : ) :
theorem HNNExtension.NormalWord.unitsSMul_neg {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } (u : ) (w : ) :
@[simp]
theorem HNNExtension.NormalWord.unitsSMulEquiv_apply {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } (w : ) :
@[simp]
theorem HNNExtension.NormalWord.unitsSMulEquiv_symm_apply {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } (w : ) :
w =
noncomputable def HNNExtension.NormalWord.unitsSMulEquiv {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } :

the equivalence given by multiplication on the left by t

Equations
• = { toFun := , invFun := , left_inv := , right_inv := }
Instances For
theorem HNNExtension.NormalWord.unitsSMul_one_group_smul {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } (g : A) (w : ) :
HNNExtension.NormalWord.unitsSMul φ 1 (g w) = (φ g)
noncomputable instance HNNExtension.NormalWord.instMulAction_1 {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem HNNExtension.NormalWord.prod_group_smul {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } (g : G) (w : ) :
HNNExtension.NormalWord.ReducedWord.prod φ (g w).toReducedWord = HNNExtension.of g * HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord
theorem HNNExtension.NormalWord.of_smul_eq_smul {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } (g : G) (w : ) :
HNNExtension.of g w = g w
theorem HNNExtension.NormalWord.t_smul_eq_unitsSMul {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } (w : ) :
HNNExtension.t w =
theorem HNNExtension.NormalWord.t_pow_smul_eq_unitsSMul {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } (u : ) (w : ) :
HNNExtension.t ^ u w =
@[simp]
theorem HNNExtension.NormalWord.prod_cons {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } (g : G) (u : ) (w : ) (h1 : w.head d.set u) (h2 : u'Option.map Prod.fst w.toList.head?, w.head u = u') :
HNNExtension.NormalWord.ReducedWord.prod φ (HNNExtension.NormalWord.cons g u w h1 h2).toReducedWord = HNNExtension.of g * (HNNExtension.t ^ u * HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord)
theorem HNNExtension.NormalWord.prod_unitsSMul {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } (u : ) (w : ) :
HNNExtension.NormalWord.ReducedWord.prod φ .toReducedWord = HNNExtension.t ^ u * HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord
@[simp]
theorem HNNExtension.NormalWord.prod_empty {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } :
HNNExtension.NormalWord.ReducedWord.prod φ HNNExtension.NormalWord.empty.toReducedWord = 1
@[simp]
theorem HNNExtension.NormalWord.prod_smul {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } (g : HNNExtension G A B φ) (w : ) :
@[simp]
theorem HNNExtension.NormalWord.prod_smul_empty {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {d : } (w : ) :
HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord HNNExtension.NormalWord.empty = w
noncomputable def HNNExtension.NormalWord.equiv {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) (d : ) :
HNNExtension G A B φ

The equivalence between elements of the HNN extension and words in normal form.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem HNNExtension.NormalWord.prod_injective {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) (d : ) :
instance HNNExtension.NormalWord.instFaithfulSMul_1 {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) (d : ) :
Equations
• =
theorem HNNExtension.of_injective {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) :
Function.Injective HNNExtension.of
theorem HNNExtension.ReducedWord.exists_normalWord_prod_eq {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) (d : ) (w : ) :
∃ (w' : ), HNNExtension.NormalWord.ReducedWord.prod φ w'.toReducedWord = List.map Prod.fst w'.toList = List.map Prod.fst w.toList uOption.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head
theorem HNNExtension.ReducedWord.map_fst_eq_and_of_prod_eq {G : Type u_1} [] {A : } {B : } (φ : A ≃* B) {w₁ : } {w₂ : } (hprod : ) :
Two reduced words representing the same element of the HNNExtension G A B φ have the same length corresponding list, with the same pattern of occurences of t^1 and t^(-1), and also the head is in the same left coset of toSubgroup A B (-u), where u : ℤˣ is the exponent of the first occurence of t in the word.
Britton's Lemma. Any reduced word whose product is an element of G, has no occurences of t.