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) (φ : { x : G // x A } ≃* { x : G // x 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.
def HNNExtension (G : Type u_1) [Group G] (A : Subgroup G) (B : Subgroup G) (φ : { x : G // x A } ≃* { x : G // x 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} {φ : { x : G // x A } ≃* { x : G // x 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} {φ : { x : G // x A } ≃* { x : G // x B }} :
G →* HNNExtension G A B φ

The canonical embedding G →* HNNExtension G A B φ

Equations
def HNNExtension.t {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : { x : G // x A } ≃* { x : G // x 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)
theorem HNNExtension.t_mul_of {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : { x : G // x A } ≃* { x : G // x B }} (a : { x : G // x 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} {φ : { x : G // x A } ≃* { x : G // x B }} (b : { x : G // x 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} {φ : { x : G // x A } ≃* { x : G // x B }} (a : { x : G // x 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} {φ : { x : G // x A } ≃* { x : G // x B }} (b : { x : G // x 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} {φ : { x : G // x A } ≃* { x : G // x B }} (b : { x : G // x 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} {φ : { x : G // x A } ≃* { x : G // x B }} (a : { x : G // x 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} {φ : { x : G // x A } ≃* { x : G // x B }} {H : Type u_2} [Group H] (f : G →* H) (x : H) (hx : ∀ (a : { x : G // x 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
@[simp]
theorem HNNExtension.lift_t {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : { x : G // x A } ≃* { x : G // x B }} {H : Type u_2} [Group H] (f : G →* H) (x : H) (hx : ∀ (a : { x : G // x 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} {φ : { x : G // x A } ≃* { x : G // x B }} {H : Type u_2} [Group H] (f : G →* H) (x : H) (hx : ∀ (a : { x : G // x 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} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : { x : G // x A } ≃* { x : G // x B }} {M : Type u_3} [Monoid M] {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} [Group G] {A : Subgroup G} {B : Subgroup G} {φ : { x : G // x A } ≃* { x : G // x 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} {φ : { x : G // x A } ≃* { x : G // x 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
@[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} (φ : { x : G // x A } ≃* { x : G // x B }) (u : ˣ) :
{ x : G // x HNNExtension.toSubgroup A B u } ≃* { x : G // x HNNExtension.toSubgroup 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
@[simp]
theorem HNNExtension.toSubgroupEquiv_one {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x B }) :
@[simp]
theorem HNNExtension.toSubgroupEquiv_neg_one {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x B }) :
@[simp]
theorem HNNExtension.toSubgroupEquiv_neg_apply {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x B }) (u : ˣ) (a : { x : G // x 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

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
def HNNExtension.NormalWord.ReducedWord.prod {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x B }) :

The product of a ReducedWord as an element of the HNNExtension

Equations

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_iff {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} :
w = w' w.head = w'.head w.toList = w'.toList
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'
@[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 empty word

Equations
  • HNNExtension.NormalWord.empty = { head := 1, toList := [], chain := , mem_set := }

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

Equations
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
@[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.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
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.
@[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} (φ : { x : G // x A } ≃* { x : G // x B }) (d : HNNExtension.NormalWord.TransversalPair G A B) (u : ˣ) (g : G) :
{ x : G // x 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
theorem HNNExtension.NormalWord.unitsSMulGroup_snd {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x 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

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.
noncomputable def HNNExtension.NormalWord.unitsSMul {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x 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.
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.

noncomputable def HNNExtension.NormalWord.unitsSMulEquiv {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x B }) {d : HNNExtension.NormalWord.TransversalPair G A B} :

the equivalence given by multiplication on the left by t

Equations
theorem HNNExtension.NormalWord.unitsSMul_one_group_smul {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x B }) {d : HNNExtension.NormalWord.TransversalPair G A B} (g : { x : G // x A }) (w : HNNExtension.NormalWord d) :
noncomputable instance HNNExtension.NormalWord.instMulAction_1 {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x 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} (φ : { x : G // x A } ≃* { x : G // x 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} (φ : { x : G // x A } ≃* { x : G // x B }) {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G) (w : HNNExtension.NormalWord d) :
HNNExtension.of g w = g w
theorem HNNExtension.NormalWord.t_smul_eq_unitsSMul {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x B }) {d : HNNExtension.NormalWord.TransversalPair G A B} (w : HNNExtension.NormalWord d) :
HNNExtension.t w = HNNExtension.NormalWord.unitsSMul φ 1 w
theorem HNNExtension.NormalWord.t_pow_smul_eq_unitsSMul {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x B }) {d : HNNExtension.NormalWord.TransversalPair G A B} (u : ˣ) (w : HNNExtension.NormalWord d) :
HNNExtension.t ^ u w = HNNExtension.NormalWord.unitsSMul φ u w
@[simp]
theorem HNNExtension.NormalWord.prod_cons {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x 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)
theorem HNNExtension.NormalWord.prod_unitsSMul {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x B }) {d : HNNExtension.NormalWord.TransversalPair G A B} (u : ˣ) (w : HNNExtension.NormalWord d) :
@[simp]
theorem HNNExtension.NormalWord.prod_empty {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x 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} (φ : { x : G // x A } ≃* { x : G // x 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} (φ : { x : G // x A } ≃* { x : G // x 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} (φ : { x : G // x A } ≃* { x : G // x 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.
theorem HNNExtension.NormalWord.prod_injective {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x B }) (d : HNNExtension.NormalWord.TransversalPair G A B) :
instance HNNExtension.NormalWord.instFaithfulSMul_1 {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x B }) (d : HNNExtension.NormalWord.TransversalPair G A B) :
Equations
  • =
theorem HNNExtension.of_injective {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x B }) :
Function.Injective HNNExtension.of
theorem HNNExtension.ReducedWord.exists_normalWord_prod_eq {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (φ : { x : G // x A } ≃* { x : G // x 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} (φ : { x : G // x A } ≃* { x : G // x 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} (φ : { x : G // x A } ≃* { x : G // x 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.