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 #

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 : Subgroup G) (B : Subgroup G) (φ : { x : G // x ∈ A } ≃* { x : G // x ∈ 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 : 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

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

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

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

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

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

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

@[simp]

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

HNNExtension.toSubgroup A B 1 = A

@[simp]

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

HNNExtension.toSubgroup A B (-1) = B

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

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

@[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 }) :

HNNExtension.toSubgroupEquiv φ 1 = φ

@[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 }) :

HNNExtension.toSubgroupEquiv φ (-1) = φ.symm

@[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 }) :

↑((HNNExtension.toSubgroupEquiv φ (-u)) ((HNNExtension.toSubgroupEquiv φ u) a)) = ↑a

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.

set : ℤ ˣ → Set G
The transversal of each subgroup
compl : ∀ (u : ℤ ˣ), Subgroup.IsComplement (↑(HNNExtension.toSubgroup A B u)) (self.set u)
We have exactly one element of each coset of the subgroup

Instances For

HNNExtension.NormalWord.TransversalPair.nonempty

theorem HNNExtension.NormalWord.TransversalPair.compl {G : Type u_1} [Group G] {A : Subgroup G} {B : Subgroup G} (self : HNNExtension.NormalWord.TransversalPair G A B) (u : ℤ ˣ) :

Subgroup.IsComplement (↑(HNNExtension.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 : Subgroup G) (B : Subgroup G) :

Nonempty (HNNExtension.NormalWord.TransversalPair G A B)

Equations

⋯ = ⋯

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

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

@[simp]

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

(HNNExtension.NormalWord.ReducedWord.empty G A B).toList = []

@[simp]

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

(HNNExtension.NormalWord.ReducedWord.empty G A B).head = 1

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

HNNExtension.NormalWord.ReducedWord G A B

The empty reduced word.

Equations

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

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 }) :

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

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 ∈ HNNExtension.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

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.toList → g ∈ 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

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

HNNExtension.NormalWord d

The empty word

Equations

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

@[simp]

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

(HNNExtension.NormalWord.ofGroup g).toList = []

@[simp]

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

(HNNExtension.NormalWord.ofGroup g).head = g

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

HNNExtension.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 := ⋯ }

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

Inhabited (HNNExtension.NormalWord d)

Equations

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

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

MulAction G (HNNExtension.NormalWord d)

Equations

HNNExtension.NormalWord.instMulAction = MulAction.mk ⋯ ⋯

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

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

FaithfulSMul G (HNNExtension.NormalWord d)

Equations

⋯ = ⋯

@[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 u → u = 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 u → u = 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 u → u = u') :

HNNExtension.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 := ⋯ }

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 d → Sort 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 u → u = u') → motive w → motive (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 d → Sort 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 u → u = u') → motive w → motive (HNNExtension.NormalWord.cons g u w h1 h2)) :

HNNExtension.NormalWord.consRecOn (HNNExtension.NormalWord.ofGroup g) ofGroup cons = ofGroup g

@[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 d → Sort 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 u → u = 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 u → u = u') → motive w → motive (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 u → 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} [Group G] {A : Subgroup G} {B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g₁ : G) (g₂ : G) :

g₁ • HNNExtension.NormalWord.ofGroup g₂ = HNNExtension.NormalWord.ofGroup (g₁ * g₂)

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

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

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

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 : 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.NormalWord.Cancels u w → HNNExtension.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 : 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.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 u → u = u') :

¬HNNExtension.NormalWord.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 : 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.NormalWord.Cancels (-u) (HNNExtension.NormalWord.unitsSMul φ u w) ↔ ¬HNNExtension.NormalWord.Cancels u w

theorem HNNExtension.NormalWord.unitsSMul_neg {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.NormalWord.unitsSMul φ (-u) (HNNExtension.NormalWord.unitsSMul φ u w) = w

@[simp]

theorem HNNExtension.NormalWord.unitsSMulEquiv_symm_apply {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.unitsSMulEquiv φ).symm w = HNNExtension.NormalWord.unitsSMul φ (-1) w

@[simp]

theorem HNNExtension.NormalWord.unitsSMulEquiv_apply {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.unitsSMulEquiv φ) w = HNNExtension.NormalWord.unitsSMul φ 1 w

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

HNNExtension.NormalWord d ≃ HNNExtension.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 := ⋯ }

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

HNNExtension.NormalWord.unitsSMul φ 1 (↑g • w) = ↑(φ g) • HNNExtension.NormalWord.unitsSMul φ 1 w

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

MulAction (HNNExtension G A B φ) (HNNExtension.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 : 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 u → 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} [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.NormalWord.ReducedWord.prod φ (HNNExtension.NormalWord.unitsSMul φ u w).toReducedWord = 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} (φ : { 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) :

HNNExtension.NormalWord.ReducedWord.prod φ (g • w).toReducedWord = g * HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord

@[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) :

HNNExtension G A B φ ≃ HNNExtension.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 : Subgroup G} {B : Subgroup G} (φ : { x : G // x ∈ A } ≃* { x : G // x ∈ B }) (d : HNNExtension.NormalWord.TransversalPair G A B) :

Function.Injective fun (w : HNNExtension.NormalWord d) => HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord

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

FaithfulSMul (HNNExtension G A B φ) (HNNExtension.NormalWord d)

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 ∧ ∀ u ∈ Option.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 ∧ ∀ u ∈ Option.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.