Documentation

Mathlib.GroupTheory.HNNExtension

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 #

def HNNExtension.con (G : Type u_1) [Group G] (A : Subgroup G) (B : Subgroup G) (φ : 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) [Group G] (A : Subgroup G) (B : Subgroup G) (φ : 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} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : A ≃* B} :
      Group (HNNExtension G A B φ)
      Equations
      • instGroupHNNExtension = id inferInstance
      def HNNExtension.of {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : 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} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : 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} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : A ≃* B} (a : A) :
          HNNExtension.t * HNNExtension.of a = HNNExtension.of (φ a) * HNNExtension.t
          theorem HNNExtension.of_mul_t {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : A ≃* B} (b : B) :
          HNNExtension.of b * HNNExtension.t = HNNExtension.t * HNNExtension.of (φ.symm b)
          theorem HNNExtension.equiv_eq_conj {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : A ≃* B} (a : A) :
          HNNExtension.of (φ a) = HNNExtension.t * HNNExtension.of a * HNNExtension.t⁻¹
          theorem HNNExtension.equiv_symm_eq_conj {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : 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} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : 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} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : A ≃* B} (a : A) :
          HNNExtension.of a * HNNExtension.t⁻¹ = HNNExtension.t⁻¹ * HNNExtension.of (φ a)
          def HNNExtension.lift {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : A ≃* B} {H : Type u_2} [Group H] (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} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : A ≃* B} {H : Type u_2} [Group H] (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} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : A ≃* B} {H : Type u_2} [Group H] (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 {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : A ≃* B} {M : Type u_3} [Monoid M] {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} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : 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} [Group G] (A : Subgroup G) (B : Subgroup G) (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
            Instances For
              @[simp]
              theorem HNNExtension.toSubgroup_one {G : Type u_1} [Group G] (A : Subgroup G) (B : Subgroup G) :
              @[simp]
              theorem HNNExtension.toSubgroup_neg_one {G : Type u_1} [Group G] (A : Subgroup G) (B : Subgroup G) :
              def HNNExtension.toSubgroupEquiv {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : 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
              Instances For
                @[simp]
                theorem HNNExtension.toSubgroupEquiv_one {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) :
                @[simp]
                theorem HNNExtension.toSubgroupEquiv_neg_one {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) :
                @[simp]
                theorem HNNExtension.toSubgroupEquiv_neg_apply {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) (u : ˣ) (a : (HNNExtension.toSubgroup A B u)) :
                structure HNNExtension.NormalWord.TransversalPair (G : Type u_1) [Group G] (A : Subgroup G) (B : Subgroup G) :
                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.

                Instances For

                  We have exactly one element of each coset of the subgroup

                  structure HNNExtension.NormalWord.ReducedWord (G : Type u_1) [Group G] (A : Subgroup G) (B : Subgroup G) :
                  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.

                  • head : G

                    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 HNNExtension.toSubgroup A B a.1a.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} [Group G] {A : Subgroup G} {B : Subgroup G} (self : HNNExtension.NormalWord.ReducedWord G A B) :
                    List.Chain' (fun (a b : ˣ × G) => a.2 HNNExtension.toSubgroup A B a.1a.1 = b.1) self.toList

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

                    The empty reduced word.

                    Equations
                    Instances For
                      def HNNExtension.NormalWord.ReducedWord.prod {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) :

                      The product of a ReducedWord as an element of the HNNExtension

                      Equations
                      Instances For

                        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

                        Instances For
                          theorem HNNExtension.NormalWord.mem_set {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (self : HNNExtension.NormalWord d) (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 {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} {w : HNNExtension.NormalWord d} {w' : HNNExtension.NormalWord d} (h1 : w.head = w'.head) (h2 : w.toList = w'.toList) :
                          w = w'

                          The empty word

                          Equations
                          • HNNExtension.NormalWord.empty = { head := 1, toList := [], chain := , mem_set := }
                          Instances For
                            @[simp]
                            theorem HNNExtension.NormalWord.empty_toList {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} :
                            HNNExtension.NormalWord.empty.toList = []
                            @[simp]
                            theorem HNNExtension.NormalWord.empty_head {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} :
                            HNNExtension.NormalWord.empty.head = 1

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

                            Equations
                            Instances For
                              Equations
                              • HNNExtension.NormalWord.instInhabited = { default := HNNExtension.NormalWord.empty }
                              Equations
                              theorem HNNExtension.NormalWord.group_smul_def {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G) (w : HNNExtension.NormalWord d) :
                              g w = { head := g * w.head, toList := w.toList, chain := , mem_set := }
                              @[simp]
                              theorem HNNExtension.NormalWord.group_smul_head {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G) (w : HNNExtension.NormalWord d) :
                              (g w).head = g * w.head
                              @[simp]
                              theorem HNNExtension.NormalWord.group_smul_toList {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G) (w : HNNExtension.NormalWord d) :
                              (g w).toList = w.toList
                              def HNNExtension.NormalWord.cons {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G) (u : ˣ) (w : HNNExtension.NormalWord d) (h1 : w.head d.set u) (h2 : u'Option.map Prod.fst w.toList.head?, w.head HNNExtension.toSubgroup A B uu = 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
                                @[simp]
                                theorem HNNExtension.NormalWord.cons_head {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G) (u : ˣ) (w : HNNExtension.NormalWord d) (h1 : w.head d.set u) (h2 : u'Option.map Prod.fst w.toList.head?, w.head HNNExtension.toSubgroup A B uu = u') :
                                (HNNExtension.NormalWord.cons g u w h1 h2).head = g
                                @[simp]
                                theorem HNNExtension.NormalWord.cons_toList {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G) (u : ˣ) (w : HNNExtension.NormalWord d) (h1 : w.head d.set u) (h2 : u'Option.map Prod.fst w.toList.head?, w.head HNNExtension.toSubgroup A B uu = u') :
                                (HNNExtension.NormalWord.cons g u w h1 h2).toList = (u, w.head) :: w.toList
                                def HNNExtension.NormalWord.consRecOn {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} {motive : HNNExtension.NormalWord dSort u_4} (w : HNNExtension.NormalWord d) (ofGroup : (g : G) → motive (HNNExtension.NormalWord.ofGroup g)) (cons : (g : G) → (u : ˣ) → (w : HNNExtension.NormalWord d) → (h1 : w.head d.set u) → (h2 : u'Option.map Prod.fst w.toList.head?, w.head HNNExtension.toSubgroup A B uu = u') → motive wmotive (HNNExtension.NormalWord.cons g u w h1 h2)) :
                                motive w

                                A recursor to induct on a NormalWord, by proving the property 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} [Group G] {A : Subgroup G} {B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} {motive : HNNExtension.NormalWord dSort u_4} (g : G) (ofGroup : (g : G) → motive (HNNExtension.NormalWord.ofGroup g)) (cons : (g : G) → (u : ˣ) → (w : HNNExtension.NormalWord d) → (h1 : w.head d.set u) → (h2 : u'Option.map Prod.fst w.toList.head?, w.head HNNExtension.toSubgroup A B uu = u') → motive wmotive (HNNExtension.NormalWord.cons g u w h1 h2)) :
                                  @[simp]
                                  theorem HNNExtension.NormalWord.consRecOn_cons {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} {motive : HNNExtension.NormalWord dSort u_4} (g : G) (u : ˣ) (w : HNNExtension.NormalWord d) (h1 : w.head d.set u) (h2 : u'Option.map Prod.fst w.toList.head?, w.head HNNExtension.toSubgroup A B uu = u') (ofGroup : (g : G) → motive (HNNExtension.NormalWord.ofGroup g)) (cons : (g : G) → (u : ˣ) → (w : HNNExtension.NormalWord d) → (h1 : w.head d.set u) → (h2 : u'Option.map Prod.fst w.toList.head?, w.head HNNExtension.toSubgroup A B uu = 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} [Group G] {A : Subgroup G} {B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g₁ : G) (g₂ : G) (u : ˣ) (w : HNNExtension.NormalWord d) (h1 : w.head d.set u) (h2 : u'Option.map Prod.fst w.toList.head?, w.head HNNExtension.toSubgroup A B uu = u') :
                                  g₁ HNNExtension.NormalWord.cons g₂ u w h1 h2 = HNNExtension.NormalWord.cons (g₁ * g₂) u w h1 h2
                                  noncomputable def HNNExtension.NormalWord.unitsSMulGroup {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) (d : HNNExtension.NormalWord.TransversalPair G A B) (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
                                  Instances For
                                    theorem HNNExtension.NormalWord.unitsSMulGroup_snd {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) (d : HNNExtension.NormalWord.TransversalPair G A B) (u : ˣ) (g : G) :
                                    (HNNExtension.NormalWord.unitsSMulGroup φ d u g).2 = (.equiv g).2

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

                                    Equations
                                    Instances For

                                      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} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) {d : HNNExtension.NormalWord.TransversalPair G A B} (u : ˣ) (w : HNNExtension.NormalWord d) :

                                        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} [Group G] {A : Subgroup G} {B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (u : ˣ) (w : HNNExtension.NormalWord d) (h2 : u'Option.map Prod.fst w.toList.head?, w.head HNNExtension.toSubgroup A B uu = u') :

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

                                          the equivalence given by multiplication on the left by t

                                          Equations
                                          Instances For
                                            noncomputable instance HNNExtension.NormalWord.instMulAction_1 {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) {d : HNNExtension.NormalWord.TransversalPair G A B} :
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            @[simp]
                                            theorem HNNExtension.NormalWord.prod_group_smul {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G) (w : HNNExtension.NormalWord d) :
                                            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} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G) (w : HNNExtension.NormalWord d) :
                                            HNNExtension.of g w = g w
                                            @[simp]
                                            theorem HNNExtension.NormalWord.prod_cons {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G) (u : ˣ) (w : HNNExtension.NormalWord d) (h1 : w.head d.set u) (h2 : u'Option.map Prod.fst w.toList.head?, w.head HNNExtension.toSubgroup A B uu = 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)
                                            @[simp]
                                            theorem HNNExtension.NormalWord.prod_empty {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) {d : HNNExtension.NormalWord.TransversalPair G A B} :
                                            HNNExtension.NormalWord.ReducedWord.prod φ HNNExtension.NormalWord.empty.toReducedWord = 1
                                            @[simp]
                                            theorem HNNExtension.NormalWord.prod_smul {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) {d : HNNExtension.NormalWord.TransversalPair G A B} (g : HNNExtension G A B φ) (w : HNNExtension.NormalWord d) :
                                            @[simp]
                                            theorem HNNExtension.NormalWord.prod_smul_empty {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) {d : HNNExtension.NormalWord.TransversalPair G A B} (w : HNNExtension.NormalWord d) :
                                            HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord HNNExtension.NormalWord.empty = w
                                            noncomputable def HNNExtension.NormalWord.equiv {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) (d : HNNExtension.NormalWord.TransversalPair 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
                                              Equations
                                              • =
                                              theorem HNNExtension.of_injective {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) :
                                              Function.Injective HNNExtension.of
                                              theorem HNNExtension.ReducedWord.exists_normalWord_prod_eq {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) (d : HNNExtension.NormalWord.TransversalPair G A B) (w : HNNExtension.NormalWord.ReducedWord G A B) :
                                              ∃ (w' : HNNExtension.NormalWord d), HNNExtension.NormalWord.ReducedWord.prod φ w'.toReducedWord = HNNExtension.NormalWord.ReducedWord.prod φ w List.map Prod.fst w'.toList = List.map Prod.fst w.toList uOption.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head HNNExtension.toSubgroup A B (-u)
                                              theorem HNNExtension.ReducedWord.map_fst_eq_and_of_prod_eq {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) {w₁ : HNNExtension.NormalWord.ReducedWord G A B} {w₂ : HNNExtension.NormalWord.ReducedWord G A B} (hprod : HNNExtension.NormalWord.ReducedWord.prod φ w₁ = HNNExtension.NormalWord.ReducedWord.prod φ w₂) :
                                              List.map Prod.fst w₁.toList = List.map Prod.fst w₂.toList uOption.map Prod.fst w₁.toList.head?, w₁.head⁻¹ * w₂.head HNNExtension.toSubgroup A B (-u)

                                              Two reduced words representing the same element of the HNNExtension G A B φ have the same length corresponding list, with the same pattern of occurrences 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 occurrence of t in the word.

                                              theorem HNNExtension.ReducedWord.toList_eq_nil_of_mem_of_range {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : A ≃* B) (w : HNNExtension.NormalWord.ReducedWord G A B) (hw : HNNExtension.NormalWord.ReducedWord.prod φ w HNNExtension.of.range) :
                                              w.toList = []

                                              Britton's Lemma. Any reduced word whose product is an element of G, has no occurrences of t.