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) [Group G] (A B : Subgroup G) (φ : ↥A ≃* ↥B) : Con (Monoid.Coprod G (Multiplicative ℤ))

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 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

• HNNExtension G A B φ = (HNNExtension.con G A B φ).Quotient

instance instGroupHNNExtension {G : Type u_1} [Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} : Group (HNNExtension G A B φ)

Equations

• instGroupHNNExtension = id inferInstance

def HNNExtension.of {G : Type u_1} [Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} : G →* HNNExtension G A B φ

The canonical embedding G →* HNNExtension G A B φ

Equations

• HNNExtension.of = (HNNExtension.con G A B φ).mk'.comp Monoid.Coprod.inl

def HNNExtension.t {G : Type u_1} [Group G] {A 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)

theorem HNNExtension.t_mul_of {G : Type u_1} [Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} (a : ↥A) : t * of ↑a = of ↑(φ a) * t

theorem HNNExtension.of_mul_t {G : Type u_1} [Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} (b : ↥B) : of ↑b * t = t * of ↑(φ.symm b)

theorem HNNExtension.equiv_eq_conj {G : Type u_1} [Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} (a : ↥A) : of ↑(φ a) = t * of ↑a * t⁻¹

theorem HNNExtension.equiv_symm_eq_conj {G : Type u_1} [Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} (b : ↥B) : of ↑(φ.symm b) = t⁻¹ * of ↑b * t

theorem HNNExtension.inv_t_mul_of {G : Type u_1} [Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} (b : ↥B) : t⁻¹ * of ↑b = of ↑(φ.symm b) * t⁻¹

theorem HNNExtension.of_mul_inv_t {G : Type u_1} [Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} (a : ↥A) : of ↑a * t⁻¹ = t⁻¹ * of ↑(φ a)

def HNNExtension.lift {G : Type u_1} [Group G] {A 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

• HNNExtension.lift f x hx = (HNNExtension.con G A B φ).lift (Monoid.Coprod.lift f ((zpowersHom H) x)) ⋯

@[simp]

theorem HNNExtension.lift_t {G : Type u_1} [Group G] {A 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) : (lift f x hx) t = x

@[simp]

theorem HNNExtension.lift_of {G : Type u_1} [Group G] {A 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) : (lift f x hx) (of g) = f g

theorem HNNExtension.hom_ext {G : Type u_1} [Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} {M : Type u_3} [Monoid M] {f g : HNNExtension G A B φ →* M} (hg : f.comp of = g.comp of) (ht : f t = g t) : f = g

theorem HNNExtension.induction_on {G : Type u_1} [Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} {motive : HNNExtension G A B φ → Prop} (x : HNNExtension G A B φ) (of : ∀ (g : G), motive (of g)) (t : motive t) (mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)) (inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹) : motive x

def HNNExtension.toSubgroup {G : Type u_1} [Group G] (A B : Subgroup G) (u : ℤˣ) : Subgroup G

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

• HNNExtension.toSubgroup A B u = if u = 1 then A else B

@[simp]

theorem HNNExtension.toSubgroup_one {G : Type u_1} [Group G] (A B : Subgroup G) : toSubgroup A B 1 = A

@[simp]

theorem HNNExtension.toSubgroup_neg_one {G : Type u_1} [Group G] (A B : Subgroup G) : toSubgroup A B (-1) = B

def HNNExtension.toSubgroupEquiv {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) (u : ℤˣ) : ↥(toSubgroup A B u) ≃* ↥(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

• HNNExtension.toSubgroupEquiv φ u = if hu : u = 1 then ⋯ ▸ φ else ⋯.mpr φ.symm

@[simp]

theorem HNNExtension.toSubgroupEquiv_one {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) : toSubgroupEquiv φ 1 = φ

@[simp]

theorem HNNExtension.toSubgroupEquiv_neg_one {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) : toSubgroupEquiv φ (-1) = φ.symm

@[simp]

theorem HNNExtension.toSubgroupEquiv_neg_apply {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) (u : ℤˣ) (a : ↥(toSubgroup A B u)) : ↑((toSubgroupEquiv φ (-u)) ((toSubgroupEquiv φ u) a)) = ↑a

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

• set : ℤˣ → Set G

  The transversal of each subgroup

• compl (u : ℤˣ) : Subgroup.IsComplement (↑(toSubgroup A B u)) (self.set u)

  We have exactly one element of each coset of the subgroup

instance HNNExtension.NormalWord.TransversalPair.nonempty (G : Type u_1) [Group G] (A B : Subgroup G) : Nonempty (TransversalPair G A B)

structure HNNExtension.NormalWord.ReducedWord (G : Type u_1) [Group G] (A 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 ∈ toSubgroup A B a.1 → a.1 = b.1) self.toList

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

def HNNExtension.NormalWord.ReducedWord.empty (G : Type u_1) [Group G] (A B : Subgroup G) : ReducedWord G A B

The empty reduced word.

Equations

• HNNExtension.NormalWord.ReducedWord.empty G A B = { head := 1, toList := [], chain := ⋯ }

@[simp]

theorem HNNExtension.NormalWord.ReducedWord.empty_toList (G : Type u_1) [Group G] (A B : Subgroup G) : (empty G A B).toList = []

@[simp]

theorem HNNExtension.NormalWord.ReducedWord.empty_head (G : Type u_1) [Group G] (A B : Subgroup G) : (empty G A B).head = 1

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

The product of a ReducedWord as an element of the HNNExtension

Equations

• HNNExtension.NormalWord.ReducedWord.prod φ w = HNNExtension.of w.head * (List.map (fun (x : ℤˣ × G) => HNNExtension.t ^ ↑x.1 * HNNExtension.of x.2) w.toList).prod

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

• head : G
• toList : List (ℤˣ × G)
• chain : List.Chain' (fun (a b : ℤˣ × G) => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) self.toList
• mem_set (u : ℤˣ) (g : G) : (u, g) ∈ self.toList → g ∈ 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 B : Subgroup G} {d : TransversalPair G A B} {w w' : NormalWord d} (h1 : w.head = w'.head) (h2 : w.toList = w'.toList) : w = w'

def HNNExtension.NormalWord.empty {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} : NormalWord d

The empty word

Equations

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

@[simp]

theorem HNNExtension.NormalWord.empty_toList {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} : empty.toList = []

@[simp]

theorem HNNExtension.NormalWord.empty_head {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} : empty.head = 1

def HNNExtension.NormalWord.ofGroup {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} (g : G) : NormalWord d

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

Equations

• HNNExtension.NormalWord.ofGroup g = { head := g, toList := [], chain := ⋯, mem_set := ⋯ }

@[simp]

theorem HNNExtension.NormalWord.ofGroup_head {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} (g : G) : (ofGroup g).head = g

@[simp]

theorem HNNExtension.NormalWord.ofGroup_toList {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} (g : G) : (ofGroup g).toList = []

instance HNNExtension.NormalWord.instInhabited {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} : Inhabited (NormalWord d)

Equations

• HNNExtension.NormalWord.instInhabited = { default := HNNExtension.NormalWord.empty }

instance HNNExtension.NormalWord.instMulAction {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} : MulAction G (NormalWord d)

Equations

• HNNExtension.NormalWord.instMulAction = MulAction.mk ⋯ ⋯

theorem HNNExtension.NormalWord.group_smul_def {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} (g : G) (w : 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 B : Subgroup G} {d : TransversalPair G A B} (g : G) (w : NormalWord d) : (g • w).head = g * w.head

@[simp]

theorem HNNExtension.NormalWord.group_smul_toList {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} (g : G) (w : NormalWord d) : (g • w).toList = w.toList

instance HNNExtension.NormalWord.instFaithfulSMul {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} : FaithfulSMul G (NormalWord d)

def HNNExtension.NormalWord.cons {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} (g : G) (u : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u) (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u') : NormalWord d

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

• HNNExtension.NormalWord.cons g u w h1 h2 = { head := g, toList := (u, w.head) :: w.toList, chain := ⋯, mem_set := ⋯ }

@[simp]

theorem HNNExtension.NormalWord.cons_toList {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} (g : G) (u : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u) (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u') : (cons g u w h1 h2).toList = (u, w.head) :: w.toList

@[simp]

theorem HNNExtension.NormalWord.cons_head {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} (g : G) (u : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u) (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u') : (cons g u w h1 h2).head = g

def HNNExtension.NormalWord.consRecOn {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} {motive : NormalWord d → Sort u_4} (w : NormalWord d) (ofGroup : (g : G) → motive (ofGroup g)) (cons : (g : G) → (u : ℤˣ) → (w : NormalWord d) → (h1 : w.head ∈ d.set u) → (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u') → motive w → motive (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 B : Subgroup G} {d : TransversalPair G A B} {motive : NormalWord d → Sort u_4} (g : G) (ofGroup : (g : G) → motive (ofGroup g)) (cons : (g : G) → (u : ℤˣ) → (w : NormalWord d) → (h1 : w.head ∈ d.set u) → (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u') → motive w → motive (cons g u w h1 h2)) : consRecOn (HNNExtension.NormalWord.ofGroup g) ofGroup cons = ofGroup g

@[simp]

theorem HNNExtension.NormalWord.consRecOn_cons {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} {motive : NormalWord d → Sort u_4} (g : G) (u : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u) (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u') (ofGroup : (g : G) → motive (ofGroup g)) (cons : (g : G) → (u : ℤˣ) → (w : NormalWord d) → (h1 : w.head ∈ d.set u) → (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u') → motive w → motive (cons g u w h1 h2)) : consRecOn (HNNExtension.NormalWord.cons g u w h1 h2) ofGroup cons = cons g u w h1 h2 (consRecOn w ofGroup cons)

@[simp]

theorem HNNExtension.NormalWord.smul_cons {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} (g₁ g₂ : G) (u : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u) (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u') : g₁ • cons g₂ u w h1 h2 = cons (g₁ * g₂) u w h1 h2

@[simp]

theorem HNNExtension.NormalWord.smul_ofGroup {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} (g₁ g₂ : G) : g₁ • ofGroup g₂ = ofGroup (g₁ * g₂)

noncomputable def HNNExtension.NormalWord.unitsSMulGroup {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) (d : TransversalPair G A B) (u : ℤˣ) (g : G) : ↥(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

• HNNExtension.NormalWord.unitsSMulGroup φ d u g = ((HNNExtension.toSubgroupEquiv φ u) (⋯.equiv g).1, (⋯.equiv g).2)

theorem HNNExtension.NormalWord.unitsSMulGroup_snd {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) (d : TransversalPair G A B) (u : ℤˣ) (g : G) : (unitsSMulGroup φ d u g).2 = (⋯.equiv g).2

def HNNExtension.NormalWord.Cancels {G : Type u_1} [Group G] {A B : Subgroup G} {d : TransversalPair G A B} (u : ℤˣ) (w : NormalWord d) : Prop

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

• HNNExtension.NormalWord.Cancels u w = (w.head ∈ HNNExtension.toSubgroup A B u ∧ Option.map Prod.fst w.toList.head? = some (-u))

def HNNExtension.NormalWord.unitsSMulWithCancel {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : TransversalPair G A B} (u : ℤˣ) (w : NormalWord d) : Cancels u w → NormalWord d

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 B : Subgroup G} (φ : ↥A ≃* ↥B) {d : TransversalPair G A B} (u : ℤˣ) (w : NormalWord d) : 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 B : Subgroup G} {d : TransversalPair G A B} (u : ℤˣ) (w : NormalWord d) (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u') : ¬Cancels u w

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} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : TransversalPair G A B} (u : ℤˣ) (w : NormalWord d) : Cancels (-u) (unitsSMul φ u w) ↔ ¬Cancels u w

theorem HNNExtension.NormalWord.unitsSMul_neg {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : TransversalPair G A B} (u : ℤˣ) (w : NormalWord d) : unitsSMul φ (-u) (unitsSMul φ u w) = w

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

the equivalence given by multiplication on the left by t

Equations

• HNNExtension.NormalWord.unitsSMulEquiv φ = { toFun := HNNExtension.NormalWord.unitsSMul φ 1, invFun := HNNExtension.NormalWord.unitsSMul φ (-1), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem HNNExtension.NormalWord.unitsSMulEquiv_symm_apply {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : TransversalPair G A B} (w : NormalWord d) : (unitsSMulEquiv φ).symm w = unitsSMul φ (-1) w

@[simp]

theorem HNNExtension.NormalWord.unitsSMulEquiv_apply {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : TransversalPair G A B} (w : NormalWord d) : (unitsSMulEquiv φ) w = unitsSMul φ 1 w

theorem HNNExtension.NormalWord.unitsSMul_one_group_smul {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : TransversalPair G A B} (g : ↥A) (w : NormalWord d) : unitsSMul φ 1 (↑g • w) = ↑(φ g) • unitsSMul φ 1 w

noncomputable instance HNNExtension.NormalWord.instMulAction_1 {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : TransversalPair G A B} : MulAction (HNNExtension G A B φ) (NormalWord 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} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : TransversalPair G A B} (g : G) (w : NormalWord d) : ReducedWord.prod φ (g • w).toReducedWord = of g * ReducedWord.prod φ w.toReducedWord

theorem HNNExtension.NormalWord.of_smul_eq_smul {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : TransversalPair G A B} (g : G) (w : NormalWord d) : of g • w = g • w

theorem HNNExtension.NormalWord.t_smul_eq_unitsSMul {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : TransversalPair G A B} (w : NormalWord d) : t • w = unitsSMul φ 1 w

theorem HNNExtension.NormalWord.t_pow_smul_eq_unitsSMul {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : TransversalPair G A B} (u : ℤˣ) (w : NormalWord d) : t ^ ↑u • w = unitsSMul φ u w

@[simp]

theorem HNNExtension.NormalWord.prod_cons {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : TransversalPair G A B} (g : G) (u : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u) (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u') : ReducedWord.prod φ (cons g u w h1 h2).toReducedWord = of g * (t ^ ↑u * ReducedWord.prod φ w.toReducedWord)

theorem HNNExtension.NormalWord.prod_unitsSMul {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : TransversalPair G A B} (u : ℤˣ) (w : NormalWord d) : ReducedWord.prod φ (unitsSMul φ u w).toReducedWord = t ^ ↑u * ReducedWord.prod φ w.toReducedWord

@[simp]

theorem HNNExtension.NormalWord.prod_empty {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : TransversalPair G A B} : ReducedWord.prod φ empty.toReducedWord = 1

@[simp]

theorem HNNExtension.NormalWord.prod_smul {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : TransversalPair G A B} (g : HNNExtension G A B φ) (w : NormalWord d) : ReducedWord.prod φ (g • w).toReducedWord = g * ReducedWord.prod φ w.toReducedWord

@[simp]

theorem HNNExtension.NormalWord.prod_smul_empty {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : TransversalPair G A B} (w : NormalWord d) : ReducedWord.prod φ w.toReducedWord • empty = w

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

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 B : Subgroup G} (φ : ↥A ≃* ↥B) (d : TransversalPair G A B) : Function.Injective fun (w : NormalWord d) => ReducedWord.prod φ w.toReducedWord

instance HNNExtension.NormalWord.instFaithfulSMul_1 {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) (d : TransversalPair G A B) : FaithfulSMul (HNNExtension G A B φ) (NormalWord d)

theorem HNNExtension.of_injective {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) : Function.Injective ⇑of

theorem HNNExtension.ReducedWord.exists_normalWord_prod_eq {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) (d : NormalWord.TransversalPair G A B) (w : NormalWord.ReducedWord G A B) : ∃ (w' : NormalWord d), NormalWord.ReducedWord.prod φ w'.toReducedWord = NormalWord.ReducedWord.prod φ w ∧ List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧ ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head ∈ toSubgroup A B (-u)

theorem HNNExtension.ReducedWord.map_fst_eq_and_of_prod_eq {G : Type u_1} [Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {w₁ w₂ : NormalWord.ReducedWord G A B} (hprod : NormalWord.ReducedWord.prod φ w₁ = NormalWord.ReducedWord.prod φ w₂) : List.map Prod.fst w₁.toList = List.map Prod.fst w₂.toList ∧ ∀ u ∈ Option.map Prod.fst w₁.toList.head?, w₁.head⁻¹ * w₂.head ∈ 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 B : Subgroup G} (φ : ↥A ≃* ↥B) (w : NormalWord.ReducedWord G A B) (hw : NormalWord.ReducedWord.prod φ w ∈ of.range) : w.toList = []

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