From 53bf23227c21af21ebe645aea0331fd519c6807a Mon Sep 17 00:00:00 2001 From: Chris Hughes Date: Thu, 31 Aug 2023 15:28:34 +0100 Subject: [PATCH 01/10] feat(GroupTheory/Complement): the equivalence and some corresponding lemmas --- Mathlib/GroupTheory/Complement.lean | 134 ++++++++++++++++++++++++++++ 1 file changed, 134 insertions(+) diff --git a/Mathlib/GroupTheory/Complement.lean b/Mathlib/GroupTheory/Complement.lean index 2286326f133eb..edcdbdde649f5 100644 --- a/Mathlib/GroupTheory/Complement.lean +++ b/Mathlib/GroupTheory/Complement.lean @@ -333,6 +333,140 @@ theorem exists_right_transversal (g : G) : ∃ S ∈ rightTransversals (H : Set #align subgroup.exists_right_transversal Subgroup.exists_right_transversal #align add_subgroup.exists_right_transversal AddSubgroup.exists_right_transversal +namespace IsComplement + +/-- The equivalence `G ≃ S × T`, such that the inverse is `(*) : S × T → G` -/ +noncomputable def equiv {S T : Set G} (hST : IsComplement S T) : G ≃ S × T := + (Equiv.ofBijective (fun x : S × T => x.1.1 * x.2.1) hST).symm + +variable (hST : IsComplement S T) (hHT : IsComplement H T) (hSK : IsComplement S K) + +theorem equiv_symm_apply (x : S × T) : (hST.equiv.symm x : G) = x.1.1 * x.2.1 := rfl + +@[simp] +theorem equiv_fst_mul_equiv_snd (g : G) : ↑(hST.equiv g).fst * (hST.equiv g).snd = g := + (Equiv.ofBijective (fun x : S × T => x.1.1 * x.2.1) hST).right_inv g + +theorem equiv_fst_eq_mul_inv (g : G) : ↑(hST.equiv g).fst = g * ((hST.equiv g).snd : G)⁻¹ := + eq_mul_inv_of_mul_eq (hST.equiv_fst_mul_equiv_snd g) + +theorem equiv_snd_eq_inv_mul (g : G) : ↑(hST.equiv g).snd = ((hST.equiv g).fst : G)⁻¹ * g := + eq_inv_mul_of_mul_eq (hST.equiv_fst_mul_equiv_snd g) + +theorem equiv_fst_eq_of_leftCosetEquivalence {g₁ g₂ : G} + (h : LeftCosetEquivalence K g₁ g₂) : (hSK.equiv g₁).fst = (hSK.equiv g₂).fst := by + apply Subtype.val_injective + rcases mem_leftTransversals_iff_existsUnique_inv_mul_mem.1 hSK g₁ with ⟨x, hx⟩ + dsimp at hx + rw [hx.2 (hSK.equiv g₁).fst (hSK.equiv_snd_eq_inv_mul g₁ ▸ (hSK.equiv g₁).snd.prop), + hx.2 (hSK.equiv g₂).fst] + simp only [LeftCosetEquivalence, leftCoset, Set.image_mul_left, Set.ext_iff, + Set.mem_preimage, SetLike.mem_coe] at h + rw [SetLike.mem_coe, ← Subgroup.inv_mem_iff, mul_inv_rev, inv_inv, h, + ← Subgroup.inv_mem_iff, mul_inv_rev, inv_inv, ← hSK.equiv_snd_eq_inv_mul g₂] + exact Subtype.property _ + +theorem equiv_snd_eq_of_rightCosetEquivalence {g₁ g₂ : G} + (h : RightCosetEquivalence H g₁ g₂) : (hHT.equiv g₁).snd = (hHT.equiv g₂).snd := by + apply Subtype.val_injective + rcases mem_rightTransversals_iff_existsUnique_mul_inv_mem.1 hHT g₁ with ⟨x, hx⟩ + dsimp at hx + rw [hx.2 (hHT.equiv g₁).snd (hHT.equiv_fst_eq_mul_inv g₁ ▸ (hHT.equiv g₁).fst.prop), + hx.2 (hHT.equiv g₂).snd] + simp only [RightCosetEquivalence, rightCoset, Set.image_mul_right, Set.ext_iff, + Set.mem_preimage, SetLike.mem_coe] at h + rw [SetLike.mem_coe, ← Subgroup.inv_mem_iff, mul_inv_rev, inv_inv, h, + ← Subgroup.inv_mem_iff, mul_inv_rev, inv_inv, ← hHT.equiv_fst_eq_mul_inv g₂] + exact Subtype.property _ + +theorem leftCosetEquivalence_equiv_fst (g : G) : + LeftCosetEquivalence K g ((hSK.equiv g).fst : G) := by + simp [LeftCosetEquivalence, leftCoset_eq_iff, equiv_fst_eq_mul_inv] + +theorem rightCosetEquivalence_equiv_snd (g : G) : + RightCosetEquivalence H g ((hHT.equiv g).snd : G) := by + simp [RightCosetEquivalence, rightCoset_eq_iff, equiv_snd_eq_inv_mul] + +theorem equiv_fst_eq_self_of_mem_of_one_mem {g : G} (h1 : 1 ∈ T) (hg : g ∈ S) : + (hST.equiv g).fst = g := by + have : hST.equiv.symm (⟨g, hg⟩, ⟨1, h1⟩) = g := by + rw [equiv, Equiv.ofBijective]; simp + conv_lhs => rw [← this, Equiv.apply_symm_apply] + +theorem equiv_snd_eq_self_of_mem_of_one_mem {g : G} (h1 : 1 ∈ S) (hg : g ∈ T) : + (hST.equiv g).snd = g := by + have : hST.equiv.symm (⟨1, h1⟩, ⟨g, hg⟩) = g := by + rw [equiv, Equiv.ofBijective]; simp + conv_lhs => rw [← this, Equiv.apply_symm_apply] + +theorem equiv_snd_eq_one_of_mem_of_one_mem {g : G} (h1 : 1 ∈ T) (hg : g ∈ S) : + (hST.equiv g).snd = ⟨1, h1⟩ := by + ext + rw [equiv_snd_eq_inv_mul, equiv_fst_eq_self_of_mem_of_one_mem _ h1 hg, inv_mul_self] + +theorem equiv_fst_eq_one_of_mem_of_one_mem {g : G} (h1 : 1 ∈ S) (hg : g ∈ T) : + (hST.equiv g).fst = ⟨1, h1⟩ := by + ext + rw [equiv_fst_eq_mul_inv, equiv_snd_eq_self_of_mem_of_one_mem _ h1 hg, mul_inv_self] + +@[simp] +theorem equiv_mul_right (g : G) (k : K) : + (hSK.equiv (g * k)) = ((hSK.equiv g).fst, (hSK.equiv g).snd * k) := by + have : (hSK.equiv (g * k)).fst = (hSK.equiv g).fst := + hSK.equiv_fst_eq_of_leftCosetEquivalence + (by simp [LeftCosetEquivalence, leftCoset_eq_iff]) + ext + · rw [this] + · rw [coe_mul, equiv_snd_eq_inv_mul, this, equiv_snd_eq_inv_mul, mul_assoc] + +theorem equiv_mul_right_of_mem {g k : G} (h : k ∈ K) : + (hSK.equiv (g * k)) = ((hSK.equiv g).fst, (hSK.equiv g).snd * ⟨k, h⟩) := + equiv_mul_right _ g ⟨k, h⟩ + +@[simp] +theorem equiv_mul_left (h : H) (g : G) : + (hHT.equiv (h * g)) = (h * (hHT.equiv g).fst, (hHT.equiv g).snd) := by + have : (hHT.equiv (h * g)).snd = (hHT.equiv g).snd := + hHT.equiv_snd_eq_of_rightCosetEquivalence + (by simp [RightCosetEquivalence, rightCoset_eq_iff]) + ext + · rw [coe_mul, equiv_fst_eq_mul_inv, this, equiv_fst_eq_mul_inv, mul_assoc] + · rw [this] + +theorem equiv_mul_left_of_mem {h g : G} (hh : h ∈ H) : + (hHT.equiv (h * g)) = (⟨h, hh⟩ * (hHT.equiv g).fst, (hHT.equiv g).snd) := + equiv_mul_left _ ⟨h, hh⟩ g + +theorem equiv_one (hs1 : 1 ∈ S) (ht1 : 1 ∈ T) : + hST.equiv 1 = (⟨1, hs1⟩, ⟨1, ht1⟩) := by + rw [Equiv.apply_eq_iff_eq_symm_apply]; simp [equiv] + +theorem equiv_fst_eq_self_iff_mem {g : G} (h1 : 1 ∈ T) : + ((hST.equiv g).fst : G) = g ↔ g ∈ S := by + constructor + · intro h + rw [← h] + exact Subtype.prop _ + · exact hST.equiv_fst_eq_self_of_mem_of_one_mem h1 + +theorem equiv_snd_eq_self_iff_mem {g : G} (h1 : 1 ∈ S) : + ((hST.equiv g).snd : G) = g ↔ g ∈ T := by + constructor + · intro h + rw [← h] + exact Subtype.prop _ + · exact hST.equiv_snd_eq_self_of_mem_of_one_mem h1 + +theorem equiv_fst_eq_one_iff_mem {g : G} (h1 : 1 ∈ S) : + ((hST.equiv g).fst : G) = 1 ↔ g ∈ T := by + rw [equiv_fst_eq_mul_inv, mul_inv_eq_one, eq_comm, equiv_snd_eq_self_iff_mem _ h1] + +theorem equiv_snd_eq_one_iff_mem {g : G} (h1 : 1 ∈ T) : + ((hST.equiv g).snd : G) = 1 ↔ g ∈ S := by + rw [equiv_snd_eq_inv_mul, inv_mul_eq_one, equiv_fst_eq_self_iff_mem _ h1] + +end IsComplement + namespace MemLeftTransversals /-- A left transversal is in bijection with left cosets. -/ From 003094aa5e05b9b59fcb37aaf452aeb6d1875eb6 Mon Sep 17 00:00:00 2001 From: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Date: Sat, 2 Sep 2023 11:58:22 +0100 Subject: [PATCH 02/10] Update Mathlib/GroupTheory/Complement.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- Mathlib/GroupTheory/Complement.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/GroupTheory/Complement.lean b/Mathlib/GroupTheory/Complement.lean index edcdbdde649f5..e7fc95816152a 100644 --- a/Mathlib/GroupTheory/Complement.lean +++ b/Mathlib/GroupTheory/Complement.lean @@ -341,7 +341,7 @@ noncomputable def equiv {S T : Set G} (hST : IsComplement S T) : G ≃ S × T := variable (hST : IsComplement S T) (hHT : IsComplement H T) (hSK : IsComplement S K) -theorem equiv_symm_apply (x : S × T) : (hST.equiv.symm x : G) = x.1.1 * x.2.1 := rfl +@[simp] theorem equiv_symm_apply (x : S × T) : (hST.equiv.symm x : G) = x.1.1 * x.2.1 := rfl @[simp] theorem equiv_fst_mul_equiv_snd (g : G) : ↑(hST.equiv g).fst * (hST.equiv g).snd = g := From 63017b75479f59ad40067c79a408fd72dbab223c Mon Sep 17 00:00:00 2001 From: Chris Hughes Date: Sat, 2 Sep 2023 12:08:40 +0100 Subject: [PATCH 03/10] golfing --- Mathlib/GroupTheory/Complement.lean | 30 ++++++++++------------------- 1 file changed, 10 insertions(+), 20 deletions(-) diff --git a/Mathlib/GroupTheory/Complement.lean b/Mathlib/GroupTheory/Complement.lean index e7fc95816152a..e022745073711 100644 --- a/Mathlib/GroupTheory/Complement.lean +++ b/Mathlib/GroupTheory/Complement.lean @@ -355,29 +355,19 @@ theorem equiv_snd_eq_inv_mul (g : G) : ↑(hST.equiv g).snd = ((hST.equiv g).fst theorem equiv_fst_eq_of_leftCosetEquivalence {g₁ g₂ : G} (h : LeftCosetEquivalence K g₁ g₂) : (hSK.equiv g₁).fst = (hSK.equiv g₂).fst := by - apply Subtype.val_injective - rcases mem_leftTransversals_iff_existsUnique_inv_mul_mem.1 hSK g₁ with ⟨x, hx⟩ - dsimp at hx - rw [hx.2 (hSK.equiv g₁).fst (hSK.equiv_snd_eq_inv_mul g₁ ▸ (hSK.equiv g₁).snd.prop), - hx.2 (hSK.equiv g₂).fst] - simp only [LeftCosetEquivalence, leftCoset, Set.image_mul_left, Set.ext_iff, - Set.mem_preimage, SetLike.mem_coe] at h - rw [SetLike.mem_coe, ← Subgroup.inv_mem_iff, mul_inv_rev, inv_inv, h, - ← Subgroup.inv_mem_iff, mul_inv_rev, inv_inv, ← hSK.equiv_snd_eq_inv_mul g₂] - exact Subtype.property _ + rw [LeftCosetEquivalence, leftCoset_eq_iff] at h + apply (mem_leftTransversals_iff_existsUnique_inv_mul_mem.1 hSK g₁).unique + · simp [equiv_fst_eq_mul_inv] + · rw [SetLike.mem_coe, ← mul_mem_cancel_right h] + simp [equiv_fst_eq_mul_inv, mul_assoc] theorem equiv_snd_eq_of_rightCosetEquivalence {g₁ g₂ : G} (h : RightCosetEquivalence H g₁ g₂) : (hHT.equiv g₁).snd = (hHT.equiv g₂).snd := by - apply Subtype.val_injective - rcases mem_rightTransversals_iff_existsUnique_mul_inv_mem.1 hHT g₁ with ⟨x, hx⟩ - dsimp at hx - rw [hx.2 (hHT.equiv g₁).snd (hHT.equiv_fst_eq_mul_inv g₁ ▸ (hHT.equiv g₁).fst.prop), - hx.2 (hHT.equiv g₂).snd] - simp only [RightCosetEquivalence, rightCoset, Set.image_mul_right, Set.ext_iff, - Set.mem_preimage, SetLike.mem_coe] at h - rw [SetLike.mem_coe, ← Subgroup.inv_mem_iff, mul_inv_rev, inv_inv, h, - ← Subgroup.inv_mem_iff, mul_inv_rev, inv_inv, ← hHT.equiv_fst_eq_mul_inv g₂] - exact Subtype.property _ + rw [RightCosetEquivalence, rightCoset_eq_iff] at h + apply (mem_rightTransversals_iff_existsUnique_mul_inv_mem.1 hHT g₁).unique + · simp [equiv_snd_eq_inv_mul] + · rw [SetLike.mem_coe, ← mul_mem_cancel_left h] + simp [equiv_snd_eq_inv_mul, mul_assoc] theorem leftCosetEquivalence_equiv_fst (g : G) : LeftCosetEquivalence K g ((hSK.equiv g).fst : G) := by From 9ca663c2f96794ac916d0e51d763bc8fbfcc1d2c Mon Sep 17 00:00:00 2001 From: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Date: Sat, 2 Sep 2023 12:09:32 +0100 Subject: [PATCH 04/10] Update Mathlib/GroupTheory/Complement.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Yaël Dillies --- Mathlib/GroupTheory/Complement.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/GroupTheory/Complement.lean b/Mathlib/GroupTheory/Complement.lean index e022745073711..66c9954bdeedf 100644 --- a/Mathlib/GroupTheory/Complement.lean +++ b/Mathlib/GroupTheory/Complement.lean @@ -401,7 +401,7 @@ theorem equiv_fst_eq_one_of_mem_of_one_mem {g : G} (h1 : 1 ∈ S) (hg : g ∈ T) @[simp] theorem equiv_mul_right (g : G) (k : K) : - (hSK.equiv (g * k)) = ((hSK.equiv g).fst, (hSK.equiv g).snd * k) := by + hSK.equiv (g * k) = ((hSK.equiv g).fst, (hSK.equiv g).snd * k) := by have : (hSK.equiv (g * k)).fst = (hSK.equiv g).fst := hSK.equiv_fst_eq_of_leftCosetEquivalence (by simp [LeftCosetEquivalence, leftCoset_eq_iff]) From ca754a1fc4b11f319559cb3e6b01910e883d13d7 Mon Sep 17 00:00:00 2001 From: Chris Hughes Date: Sat, 2 Sep 2023 12:10:02 +0100 Subject: [PATCH 05/10] too many brackets --- Mathlib/GroupTheory/Complement.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/GroupTheory/Complement.lean b/Mathlib/GroupTheory/Complement.lean index e022745073711..fe1a1d995ebab 100644 --- a/Mathlib/GroupTheory/Complement.lean +++ b/Mathlib/GroupTheory/Complement.lean @@ -401,7 +401,7 @@ theorem equiv_fst_eq_one_of_mem_of_one_mem {g : G} (h1 : 1 ∈ S) (hg : g ∈ T) @[simp] theorem equiv_mul_right (g : G) (k : K) : - (hSK.equiv (g * k)) = ((hSK.equiv g).fst, (hSK.equiv g).snd * k) := by + hSK.equiv (g * k) = ((hSK.equiv g).fst, (hSK.equiv g).snd * k) := by have : (hSK.equiv (g * k)).fst = (hSK.equiv g).fst := hSK.equiv_fst_eq_of_leftCosetEquivalence (by simp [LeftCosetEquivalence, leftCoset_eq_iff]) @@ -410,12 +410,12 @@ theorem equiv_mul_right (g : G) (k : K) : · rw [coe_mul, equiv_snd_eq_inv_mul, this, equiv_snd_eq_inv_mul, mul_assoc] theorem equiv_mul_right_of_mem {g k : G} (h : k ∈ K) : - (hSK.equiv (g * k)) = ((hSK.equiv g).fst, (hSK.equiv g).snd * ⟨k, h⟩) := + hSK.equiv (g * k) = ((hSK.equiv g).fst, (hSK.equiv g).snd * ⟨k, h⟩) := equiv_mul_right _ g ⟨k, h⟩ @[simp] theorem equiv_mul_left (h : H) (g : G) : - (hHT.equiv (h * g)) = (h * (hHT.equiv g).fst, (hHT.equiv g).snd) := by + hHT.equiv (h * g) = (h * (hHT.equiv g).fst, (hHT.equiv g).snd) := by have : (hHT.equiv (h * g)).snd = (hHT.equiv g).snd := hHT.equiv_snd_eq_of_rightCosetEquivalence (by simp [RightCosetEquivalence, rightCoset_eq_iff]) @@ -424,7 +424,7 @@ theorem equiv_mul_left (h : H) (g : G) : · rw [this] theorem equiv_mul_left_of_mem {h g : G} (hh : h ∈ H) : - (hHT.equiv (h * g)) = (⟨h, hh⟩ * (hHT.equiv g).fst, (hHT.equiv g).snd) := + hHT.equiv (h * g) = (⟨h, hh⟩ * (hHT.equiv g).fst, (hHT.equiv g).snd) := equiv_mul_left _ ⟨h, hh⟩ g theorem equiv_one (hs1 : 1 ∈ S) (ht1 : 1 ∈ T) : From 0b86d8c5d7f081d24498148128590db6ab39bb67 Mon Sep 17 00:00:00 2001 From: Chris Hughes Date: Sat, 2 Sep 2023 21:05:47 +0100 Subject: [PATCH 06/10] add coe to name --- Mathlib/GroupTheory/Complement.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/GroupTheory/Complement.lean b/Mathlib/GroupTheory/Complement.lean index fe1a1d995ebab..c32f3050cef06 100644 --- a/Mathlib/GroupTheory/Complement.lean +++ b/Mathlib/GroupTheory/Complement.lean @@ -447,11 +447,11 @@ theorem equiv_snd_eq_self_iff_mem {g : G} (h1 : 1 ∈ S) : exact Subtype.prop _ · exact hST.equiv_snd_eq_self_of_mem_of_one_mem h1 -theorem equiv_fst_eq_one_iff_mem {g : G} (h1 : 1 ∈ S) : +theorem coe_equiv_fst_eq_one_iff_mem {g : G} (h1 : 1 ∈ S) : ((hST.equiv g).fst : G) = 1 ↔ g ∈ T := by rw [equiv_fst_eq_mul_inv, mul_inv_eq_one, eq_comm, equiv_snd_eq_self_iff_mem _ h1] -theorem equiv_snd_eq_one_iff_mem {g : G} (h1 : 1 ∈ T) : +theorem coe_equiv_snd_eq_one_iff_mem {g : G} (h1 : 1 ∈ T) : ((hST.equiv g).snd : G) = 1 ↔ g ∈ S := by rw [equiv_snd_eq_inv_mul, inv_mul_eq_one, equiv_fst_eq_self_iff_mem _ h1] From c60dc085ef0c35a46c9b1ae5dee87fb9ac84f9c1 Mon Sep 17 00:00:00 2001 From: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Date: Sun, 3 Sep 2023 12:54:44 +0100 Subject: [PATCH 07/10] Upgrade some lemmas to iff --- Mathlib/GroupTheory/Complement.lean | 56 ++++++++++++++++++----------- 1 file changed, 35 insertions(+), 21 deletions(-) diff --git a/Mathlib/GroupTheory/Complement.lean b/Mathlib/GroupTheory/Complement.lean index c32f3050cef06..d95280717a0ef 100644 --- a/Mathlib/GroupTheory/Complement.lean +++ b/Mathlib/GroupTheory/Complement.lean @@ -353,21 +353,33 @@ theorem equiv_fst_eq_mul_inv (g : G) : ↑(hST.equiv g).fst = g * ((hST.equiv g) theorem equiv_snd_eq_inv_mul (g : G) : ↑(hST.equiv g).snd = ((hST.equiv g).fst : G)⁻¹ * g := eq_inv_mul_of_mul_eq (hST.equiv_fst_mul_equiv_snd g) -theorem equiv_fst_eq_of_leftCosetEquivalence {g₁ g₂ : G} - (h : LeftCosetEquivalence K g₁ g₂) : (hSK.equiv g₁).fst = (hSK.equiv g₂).fst := by - rw [LeftCosetEquivalence, leftCoset_eq_iff] at h - apply (mem_leftTransversals_iff_existsUnique_inv_mul_mem.1 hSK g₁).unique - · simp [equiv_fst_eq_mul_inv] - · rw [SetLike.mem_coe, ← mul_mem_cancel_right h] - simp [equiv_fst_eq_mul_inv, mul_assoc] - -theorem equiv_snd_eq_of_rightCosetEquivalence {g₁ g₂ : G} - (h : RightCosetEquivalence H g₁ g₂) : (hHT.equiv g₁).snd = (hHT.equiv g₂).snd := by - rw [RightCosetEquivalence, rightCoset_eq_iff] at h - apply (mem_rightTransversals_iff_existsUnique_mul_inv_mem.1 hHT g₁).unique - · simp [equiv_snd_eq_inv_mul] - · rw [SetLike.mem_coe, ← mul_mem_cancel_left h] - simp [equiv_snd_eq_inv_mul, mul_assoc] +theorem equiv_fst_eq_iff_leftCosetEquivalence {g₁ g₂ : G} : + LeftCosetEquivalence K g₁ g₂ ↔ (hSK.equiv g₁).fst = (hSK.equiv g₂).fst := by + rw [LeftCosetEquivalence, leftCoset_eq_iff] + constructor + · intro h + apply (mem_leftTransversals_iff_existsUnique_inv_mul_mem.1 hSK g₁).unique + · simp [equiv_fst_eq_mul_inv] + · rw [SetLike.mem_coe, ← mul_mem_cancel_right h] + simp [equiv_fst_eq_mul_inv, ← mul_assoc] + · intro h + rw [← hSK.equiv_fst_mul_equiv_snd g₂, ←hSK.equiv_fst_mul_equiv_snd g₁, ← h, + mul_inv_rev, ← mul_assoc, inv_mul_cancel_right, ← coe_inv, ← coe_mul] + exact Subtype.property _ + +theorem equiv_snd_eq_iff_rightCosetEquivalence {g₁ g₂ : G} : + RightCosetEquivalence H g₁ g₂ ↔ (hHT.equiv g₁).snd = (hHT.equiv g₂).snd := by + rw [RightCosetEquivalence, rightCoset_eq_iff] + constructor + · intro h + apply (mem_rightTransversals_iff_existsUnique_mul_inv_mem.1 hHT g₁).unique + · simp [equiv_snd_eq_inv_mul] + · rw [SetLike.mem_coe, ← mul_mem_cancel_left h] + simp [equiv_snd_eq_inv_mul, mul_assoc] + · intro h + rw [← hHT.equiv_fst_mul_equiv_snd g₂, ←hHT.equiv_fst_mul_equiv_snd g₁, ← h, + mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← coe_inv, ← coe_mul] + exact Subtype.property _ theorem leftCosetEquivalence_equiv_fst (g : G) : LeftCosetEquivalence K g ((hSK.equiv g).fst : G) := by @@ -378,13 +390,13 @@ theorem rightCosetEquivalence_equiv_snd (g : G) : simp [RightCosetEquivalence, rightCoset_eq_iff, equiv_snd_eq_inv_mul] theorem equiv_fst_eq_self_of_mem_of_one_mem {g : G} (h1 : 1 ∈ T) (hg : g ∈ S) : - (hST.equiv g).fst = g := by + (hST.equiv g).fst = ⟨g, hg⟩ := by have : hST.equiv.symm (⟨g, hg⟩, ⟨1, h1⟩) = g := by rw [equiv, Equiv.ofBijective]; simp conv_lhs => rw [← this, Equiv.apply_symm_apply] theorem equiv_snd_eq_self_of_mem_of_one_mem {g : G} (h1 : 1 ∈ S) (hg : g ∈ T) : - (hST.equiv g).snd = g := by + (hST.equiv g).snd = ⟨g, hg⟩ := by have : hST.equiv.symm (⟨1, h1⟩, ⟨g, hg⟩) = g := by rw [equiv, Equiv.ofBijective]; simp conv_lhs => rw [← this, Equiv.apply_symm_apply] @@ -403,7 +415,7 @@ theorem equiv_fst_eq_one_of_mem_of_one_mem {g : G} (h1 : 1 ∈ S) (hg : g ∈ T) theorem equiv_mul_right (g : G) (k : K) : hSK.equiv (g * k) = ((hSK.equiv g).fst, (hSK.equiv g).snd * k) := by have : (hSK.equiv (g * k)).fst = (hSK.equiv g).fst := - hSK.equiv_fst_eq_of_leftCosetEquivalence + hSK.equiv_fst_eq_iff_leftCosetEquivalence.1 (by simp [LeftCosetEquivalence, leftCoset_eq_iff]) ext · rw [this] @@ -417,7 +429,7 @@ theorem equiv_mul_right_of_mem {g k : G} (h : k ∈ K) : theorem equiv_mul_left (h : H) (g : G) : hHT.equiv (h * g) = (h * (hHT.equiv g).fst, (hHT.equiv g).snd) := by have : (hHT.equiv (h * g)).snd = (hHT.equiv g).snd := - hHT.equiv_snd_eq_of_rightCosetEquivalence + hHT.equiv_snd_eq_iff_rightCosetEquivalence.1 (by simp [RightCosetEquivalence, rightCoset_eq_iff]) ext · rw [coe_mul, equiv_fst_eq_mul_inv, this, equiv_fst_eq_mul_inv, mul_assoc] @@ -437,7 +449,8 @@ theorem equiv_fst_eq_self_iff_mem {g : G} (h1 : 1 ∈ T) : · intro h rw [← h] exact Subtype.prop _ - · exact hST.equiv_fst_eq_self_of_mem_of_one_mem h1 + · intro h + rw [hST.equiv_fst_eq_self_of_mem_of_one_mem h1 h] theorem equiv_snd_eq_self_iff_mem {g : G} (h1 : 1 ∈ S) : ((hST.equiv g).snd : G) = g ↔ g ∈ T := by @@ -445,7 +458,8 @@ theorem equiv_snd_eq_self_iff_mem {g : G} (h1 : 1 ∈ S) : · intro h rw [← h] exact Subtype.prop _ - · exact hST.equiv_snd_eq_self_of_mem_of_one_mem h1 + · intro h + rw [hST.equiv_snd_eq_self_of_mem_of_one_mem h1 h] theorem coe_equiv_fst_eq_one_iff_mem {g : G} (h1 : 1 ∈ S) : ((hST.equiv g).fst : G) = 1 ↔ g ∈ T := by From a050fb589b4b682e16dad937ddc7d1cd8a2f61a3 Mon Sep 17 00:00:00 2001 From: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Date: Sun, 3 Sep 2023 13:00:14 +0100 Subject: [PATCH 08/10] fix the names --- Mathlib/GroupTheory/Complement.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/GroupTheory/Complement.lean b/Mathlib/GroupTheory/Complement.lean index d95280717a0ef..a34d5569a48a4 100644 --- a/Mathlib/GroupTheory/Complement.lean +++ b/Mathlib/GroupTheory/Complement.lean @@ -353,7 +353,7 @@ theorem equiv_fst_eq_mul_inv (g : G) : ↑(hST.equiv g).fst = g * ((hST.equiv g) theorem equiv_snd_eq_inv_mul (g : G) : ↑(hST.equiv g).snd = ((hST.equiv g).fst : G)⁻¹ * g := eq_inv_mul_of_mul_eq (hST.equiv_fst_mul_equiv_snd g) -theorem equiv_fst_eq_iff_leftCosetEquivalence {g₁ g₂ : G} : +theorem leftCosetEquivalence_iff_equiv_fst_eq {g₁ g₂ : G} : LeftCosetEquivalence K g₁ g₂ ↔ (hSK.equiv g₁).fst = (hSK.equiv g₂).fst := by rw [LeftCosetEquivalence, leftCoset_eq_iff] constructor @@ -367,10 +367,10 @@ theorem equiv_fst_eq_iff_leftCosetEquivalence {g₁ g₂ : G} : mul_inv_rev, ← mul_assoc, inv_mul_cancel_right, ← coe_inv, ← coe_mul] exact Subtype.property _ -theorem equiv_snd_eq_iff_rightCosetEquivalence {g₁ g₂ : G} : +theorem rightCosetEquivalence_iff_equiv_snd_eq {g₁ g₂ : G} : RightCosetEquivalence H g₁ g₂ ↔ (hHT.equiv g₁).snd = (hHT.equiv g₂).snd := by rw [RightCosetEquivalence, rightCoset_eq_iff] - constructor + constructor · intro h apply (mem_rightTransversals_iff_existsUnique_mul_inv_mem.1 hHT g₁).unique · simp [equiv_snd_eq_inv_mul] @@ -415,7 +415,7 @@ theorem equiv_fst_eq_one_of_mem_of_one_mem {g : G} (h1 : 1 ∈ S) (hg : g ∈ T) theorem equiv_mul_right (g : G) (k : K) : hSK.equiv (g * k) = ((hSK.equiv g).fst, (hSK.equiv g).snd * k) := by have : (hSK.equiv (g * k)).fst = (hSK.equiv g).fst := - hSK.equiv_fst_eq_iff_leftCosetEquivalence.1 + hSK.leftCosetEquivalence_iff_equiv_fst_eq.1 (by simp [LeftCosetEquivalence, leftCoset_eq_iff]) ext · rw [this] @@ -429,7 +429,7 @@ theorem equiv_mul_right_of_mem {g k : G} (h : k ∈ K) : theorem equiv_mul_left (h : H) (g : G) : hHT.equiv (h * g) = (h * (hHT.equiv g).fst, (hHT.equiv g).snd) := by have : (hHT.equiv (h * g)).snd = (hHT.equiv g).snd := - hHT.equiv_snd_eq_iff_rightCosetEquivalence.1 + hHT.rightCosetEquivalence_iff_equiv_snd_eq.1 (by simp [RightCosetEquivalence, rightCoset_eq_iff]) ext · rw [coe_mul, equiv_fst_eq_mul_inv, this, equiv_fst_eq_mul_inv, mul_assoc] From c57ebb3b83d2aa6d93c2d85a88b7f390eed58cca Mon Sep 17 00:00:00 2001 From: Chris Hughes Date: Sun, 3 Sep 2023 13:51:53 +0100 Subject: [PATCH 09/10] line length --- .../SpecificGroups/HNNExtension.lean | 652 ++++++++++++++++++ 1 file changed, 652 insertions(+) create mode 100644 Mathlib/GroupTheory/SpecificGroups/HNNExtension.lean diff --git a/Mathlib/GroupTheory/SpecificGroups/HNNExtension.lean b/Mathlib/GroupTheory/SpecificGroups/HNNExtension.lean new file mode 100644 index 0000000000000..292b9a2bb6c75 --- /dev/null +++ b/Mathlib/GroupTheory/SpecificGroups/HNNExtension.lean @@ -0,0 +1,652 @@ +/- +Copyright (c) 2023 Chris Hughes. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Hughes +-/ + +import Mathlib.GroupTheory.SpecificGroups.Coprod +import Mathlib.GroupTheory.Complement + +/-! + +## HNN Extensions of Groups + +This file defines the HNN extensions of groups. + +## 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`. + +-/ + +open Monoid Coprod Multiplicative Subgroup Function + +/-- The relation we quotient the coproduct by to form an `HNNExtension`. -/ +def HNNExtension.con (G : Type*) [Group G] (A B : Subgroup G) (φ : A ≃* B) : + Con (G ∗ Multiplicative ℤ) := + conGen (fun x y => ∃ (a : A), + x = inr (ofAdd 1) * inl (a : G) ∧ + y = inl (φ a : G) * inr (ofAdd 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 canoncial +map from `G` into the `HNNExtension`. -/ +def HNNExtension (G : Type*) [Group G] (A B : Subgroup G) (φ : A ≃* B) : Type _ := + (HNNExtension.con G A B φ).Quotient + +variable {G : Type*} [Group G] {A B : Subgroup G} {φ : A ≃* B} {H : Type*} + [Group H] {M : Type*} [Monoid M] + +instance : Group (HNNExtension G A B φ) := by + delta HNNExtension; infer_instance + +namespace HNNExtension + +/-- The canonical embedding `G →* HNNExtension G A B φ` -/ +def of : G →* HNNExtension G A B φ := + (HNNExtension.con G A B φ).mk'.comp inl + +/-- The stable letter of the `HNNExtension` -/ +def t : HNNExtension G A B φ := + (HNNExtension.con G A B φ).mk'.comp inr (ofAdd 1) + +theorem t_mul_of (a : A) : + t * (of (a : G) : HNNExtension G A B φ) = of (φ a : G) * t := + (Con.eq _).2 <| ConGen.Rel.of _ _ <| ⟨a, by simp⟩ + +theorem of_mul_t (b : B) : + (of (b : G) : HNNExtension G A B φ) * t = t * of (φ.symm b : G) := by + rw [t_mul_of]; simp + +theorem equiv_eq_conj (a : A) : + (of (φ a : G) : HNNExtension G A B φ) = t * of (a : G) * t⁻¹ := by + rw [t_mul_of]; simp + +theorem equiv_symm_eq_conj (b : B) : + (of (φ.symm b : G) : HNNExtension G A B φ) = t⁻¹ * of (b : G) * t := by + rw [mul_assoc, of_mul_t]; simp + +theorem inv_t_mul_of (b : B) : + t⁻¹ * (of (b : G) : HNNExtension G A B φ) = of (φ.symm b : G) * t⁻¹ := by + rw [equiv_symm_eq_conj]; simp + +theorem of_mul_inv_t (a : A) : + (of (a : G) : HNNExtension G A B φ) * t⁻¹ = t⁻¹ * of (φ a : G) := by + rw [equiv_eq_conj]; simp [mul_assoc] + +/-- Define a function `HNNExtension G A B φ →* H`, by defining it on `G` and `t` -/ +def lift (f : G →* H) (x : H) (hx : ∀ a : A, x * f ↑a = f (φ a : G) * x) : + HNNExtension G A B φ →* H := + Con.lift _ (Coprod.lift f (zpowersHom H x)) (Con.conGen_le <| by + rintro _ _ ⟨a, rfl, rfl⟩ + simp [hx]) + +@[simp] +theorem lift_t (f : G →* H) (x : H) (hx : ∀ a : A, x * f ↑a = f (φ a : G) * x) : + lift f x hx t = x := by + delta HNNExtension; simp [lift, t] + +@[simp] +theorem lift_of (f : G →* H) (x : H) (hx : ∀ a : A, x * f ↑a = f (φ a : G) * x) (g : G) : + lift f x hx (of g) = f g := by + delta HNNExtension; simp [lift, of] + +@[ext high] +theorem hom_ext {f g : HNNExtension G A B φ →* M} + (hg : f.comp of = g.comp of) (ht : f t = g t) : f = g := + (MonoidHom.cancel_right Con.mk'_surjective).mp <| + Coprod.ext_hom _ _ hg (MonoidHom.ext_mint ht) + +@[elab_as_elim] +theorem induction_on {motive : HNNExtension G A B φ → Prop} + (x : HNNExtension G A B φ) (of : ∀ g, motive (of g)) + (t : motive t) (mul : ∀ x y, motive x → motive y → motive (x * y)) + (inv : ∀ x, motive x → motive x⁻¹) : motive x := by + let S : Subgroup (HNNExtension G A B φ) := + { carrier := setOf motive + one_mem' := by simpa using of 1 + mul_mem' := mul _ _ + inv_mem' := inv _ } + let f : HNNExtension G A B φ →* S := + lift (HNNExtension.of.codRestrict S of) + ⟨HNNExtension.t, t⟩ (by intro a; ext; simp [equiv_eq_conj, mul_assoc]) + have hf : S.subtype.comp f = MonoidHom.id _ := + hom_ext (by ext; simp) (by simp) + show motive (MonoidHom.id _ x) + rw [← hf] + exact (f x).2 + +variable (A B φ) + +/-- 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 : ℤ)`. -/ +def toSubgroup (u : ℤˣ) : Subgroup G := + if u = 1 then A else B + +@[simp] +theorem toSubgroup_one : toSubgroup A B 1 = A := rfl + +@[simp] +theorem toSubgroup_neg_one : toSubgroup A B (-1) = B := rfl + +variable {A B} + +/-- 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`. -/ +def toSubgroupEquiv (u : ℤˣ) : toSubgroup A B u ≃* toSubgroup A B (-u) := + if hu : u = 1 then hu ▸ φ else by + convert φ.symm <;> + cases Int.units_eq_one_or u <;> simp_all + +@[simp] +theorem toSubgroupEquiv_one : toSubgroupEquiv φ 1 = φ := rfl + +@[simp] +theorem toSubgroupEquiv_neg_one : toSubgroupEquiv φ (-1) = φ.symm := rfl + +@[simp] +theorem toSubgroupEquiv_neg_apply (u : ℤˣ) (a : toSubgroup A B u) : + (toSubgroupEquiv φ (-u) (toSubgroupEquiv φ u a) : G) = a := by + rcases Int.units_eq_one_or u with rfl | rfl + · simp + · simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, SetLike.coe_eq_coe] + exact φ.apply_symm_apply a + +namespace NormalWord + +variable (G A B) +/-- 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`. -/ +structure TransversalPair : Type _ := + /-- The transversal of each subgroup -/ + ( set : ℤˣ → Set G ) + -- /-- The chosen element of the subgroup itself is the identity -/ + -- ( one_mem : ∀u, 1 ∈ set u ) + /-- We have exactly one element of each coset of the subgroup -/ + ( compl : ∀ u, IsComplement (toSubgroup A B u : Subgroup G) (set u) ) + +instance TransversalPair.nonempty : Nonempty (TransversalPair G A B) := by + have := fun u => exists_right_transversal (H := toSubgroup A B u) (1 : G) + simp only [Classical.skolem] at this + rcases this with ⟨t, ht⟩ + apply Nonempty.intro + exact + { set := t + -- one_mem := fun i => (ht i).2 + compl := fun i => (ht i).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`. -/ +structure ReducedWord : Type _ := + /-- Every `ReduceddWord` 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. -/ + ( head : G ) + /-- The list of pairs `(ℤˣ × G)`, where each pair `(u, g)` represents the element `t^u * g` of + `HNNExtension G A B φ` -/ + ( toList : List (ℤˣ × G) ) + /-- There are no sequences of the form `t^u * g * t^-u` where `g ∈ toSubgroup A B u` -/ + ( chain : toList.Chain' (fun a b => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) ) + +/-- The empty reduced word. -/ +@[simps] +def ReducedWord.empty : ReducedWord G A B := + { head := 1 + toList := [] + chain := List.chain'_nil } + +variable {G A B} +/-- The product of a `ReducedWord` as an element of the `HNNExtension` -/ +def ReducedWord.prod : ReducedWord G A B → HNNExtension G A B φ := + fun w => of w.head * (w.toList.map (fun x => t ^ (x.1 : ℤ) * of x.2)).prod + +/-- 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` -/ +structure _root_.HNNExtension.NormalWord (d : TransversalPair G A B) + extends ReducedWord G A B : Type _ := + /-- Every element `g : G` in the list is the chosen element of its coset -/ + ( mem_set : ∀ (u : ℤˣ) (g : G), (u, g) ∈ toList → g ∈ d.set u ) + +variable {d : TransversalPair G A B} + +@[ext] +theorem ext {w w' : NormalWord d} + (h1 : w.head = w'.head) (h2 : w.toList = w'.toList): w = w' := by + rcases w with ⟨⟨⟩, _⟩; cases w'; simp_all + +/-- The empty word -/ +@[simps] +def empty : NormalWord d := + { head := 1 + toList := [] + mem_set := by simp + chain := List.chain'_nil } + +/-- The `NormalWord` representing an element `g` of the group `G`, which is just the element `g` +itself. -/ +@[simps] +def ofGroup (g : G) : NormalWord d := + { head := g + toList := [] + mem_set := by simp + chain := List.chain'_nil } + +instance : Inhabited (NormalWord d) := ⟨empty⟩ + +instance : MulAction G (NormalWord d) := + { smul := fun g w => { w with head := g * w.head } + one_smul := by simp [instHSMul] + mul_smul := by simp [instHSMul, mul_assoc] } + +theorem group_smul_def (g : G) (w : NormalWord d) : + g • w = { w with head := g * w.head } := rfl + +@[simp] +theorem group_smul_head (g : G) (w : NormalWord d) : (g • w).head = g * w.head := rfl + +@[simp] +theorem group_smul_toList (g : G) (w : NormalWord d) : (g • w).toList = w.toList := rfl + +instance : FaithfulSMul G (NormalWord d) := ⟨by simp [group_smul_def]⟩ + +/-- 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 +-/ +@[simps] +def 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') : + NormalWord d := + { head := g, + toList := (u, w.head) :: w.toList, + mem_set := by + intro u' g' h' + simp only [List.mem_cons, Prod.mk.injEq] at h' + rcases h' with ⟨rfl, rfl⟩ | h' + · exact h1 + · exact w.mem_set _ _ h' + chain := by + refine List.chain'_cons'.2 ⟨?_, w.chain⟩ + rintro ⟨ u', g'⟩ hu' hw1 + exact h2 _ (by simp_all) hw1 } + +/-- A recursor to induct on a `NormalWord`, by proving the propert is preserved under `cons` -/ +@[elab_as_elim] +def consRecOn {motive : NormalWord d → Sort*} (w : NormalWord d) + (ofGroup : ∀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 := by + rcases w with ⟨⟨g, l, chain⟩, mem_set⟩ + induction l generalizing g with + | nil => exact ofGroup _ + | cons a l ih => + exact cons g a.1 + { head := a.2 + toList := l + mem_set := fun _ _ h => mem_set _ _ (List.mem_cons_of_mem _ h), + chain := (List.chain'_cons'.1 chain).2 } + (mem_set a.1 a.2 (List.mem_cons_self _ _)) + (by simpa using (List.chain'_cons'.1 chain).1) + (ih _ _ _) + +@[simp] +theorem consRecOn_ofGroup {motive : NormalWord d → Sort*} + (g : G) (ofGroup : ∀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 (.ofGroup g) ofGroup cons = ofGroup g := rfl + +@[simp] +theorem consRecOn_cons {motive : NormalWord d → Sort*} + (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, 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 (.cons g u w h1 h2) ofGroup cons = cons g u w h1 h2 + (consRecOn w ofGroup cons) := rfl + +@[simp] +theorem smul_cons (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 := + rfl + +@[simp] +theorem smul_ofGroup (g₁ g₂ : G) : + g₁ • (ofGroup g₂ : NormalWord d) = ofGroup (g₁ * g₂) := rfl + +variable (d) +/-- The action of `t^u` on `ofGroup g`. The normal form will be +`a * t^u * g'` where `a ∈ toSubgroup A B (-u)` -/ +noncomputable def unitsSMulGroup (u : ℤˣ) (g : G) : + (toSubgroup A B (-u)) × d.set u := + let g' := (d.compl u).equiv g + (toSubgroupEquiv φ u g'.1, g'.2) + +theorem unitsSMulGroup_snd (u : ℤˣ) (g : G) : + (unitsSMulGroup φ d u g).2 = ((d.compl u).equiv g).2 := by + rcases Int.units_eq_one_or u with rfl | rfl <;> rfl + +variable {d} [DecidableEq G] + +/-- `Cancels u w` is a predicate expressing whether `t^u` cancels with some occurence +of `t^-u` when when we multiply `t^u` by `w`. -/ +def Cancels (u : ℤˣ) (w : NormalWord d) : Prop := + (w.head ∈ (toSubgroup A B u : Subgroup G)) ∧ w.toList.head?.map Prod.fst = some (-u) + +/-- Multiplying `t^u` by `w` in the special case where cancellation happens -/ +def unitsSMulWithCancel (u : ℤˣ) (w : NormalWord d) : Cancels u w → NormalWord d := + consRecOn w + (by simp [Cancels, ofGroup]; tauto) + (fun g u' w h1 h2 _ can => + (toSubgroupEquiv φ u ⟨g, can.1⟩ : G) • w) + +/-- Multiplying `t^u` by a `NormalWord`, `w` and putting the result in normal form. -/ +noncomputable def unitsSMul (u : ℤˣ) (w : NormalWord d) : NormalWord d := + letI := Classical.dec + if h : Cancels u w + then unitsSMulWithCancel φ u w h + else let g' := unitsSMulGroup φ d u w.head + cons g'.1 u ((g'.2 * w.head⁻¹ : G) • w) + (by simp) + (by + simp only [group_smul_toList, Option.mem_def, Option.map_eq_some', Prod.exists, + exists_and_right, exists_eq_right, group_smul_head, inv_mul_cancel_right, + forall_exists_index, unitsSMulGroup] + simp only [Cancels, Option.map_eq_some', Prod.exists, exists_and_right, exists_eq_right, + not_and, not_exists] at h + intro u' x hx hmem + have : w.head ∈ toSubgroup A B u := by + have := (d.compl u).rightCosetEquivalence_equiv_snd w.head + rw [RightCosetEquivalence, rightCoset_eq_iff, mul_mem_cancel_left hmem] at this + simp_all + have := h this x + simp_all [Int.units_ne_iff_eq_neg]) + +/-- A condition for not cancelling whose hypothese are the same as those of the `cons` function. -/ +theorem not_cancels_of_cons_hyp (u : ℤˣ) (w : NormalWord d) + (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, + w.head ∈ toSubgroup A B u → u = u') : + ¬ Cancels u w := by + simp only [Cancels, Option.map_eq_some', Prod.exists, + exists_and_right, exists_eq_right, not_and, not_exists] + intro hw x hx + rw [hx] at h2 + simpa using h2 (-u) rfl hw + +theorem unitsSMul_cancels_iff (u : ℤˣ) (w : NormalWord d) : + Cancels (-u) (unitsSMul φ u w) ↔ ¬ Cancels u w := by + by_cases h : Cancels u w + · simp only [unitsSMul, dif_pos trivial, h, iff_false] + induction w using consRecOn with + | ofGroup => simp [Cancels, unitsSMulWithCancel] + | cons g u' w h1 h2 _ => + intro hc + apply not_cancels_of_cons_hyp _ _ h2 + simp only [Cancels, cons_head, cons_toList, List.head?_cons, + Option.map_some', Option.some.injEq] at h + cases h.2 + simpa [Cancels, unitsSMulWithCancel, + Subgroup.mul_mem_cancel_left] using hc + · simp only [unitsSMul, dif_neg h] + simpa [Cancels] using h + +theorem unitsSMul_neg (u : ℤˣ) (w : NormalWord d) : + unitsSMul φ (-u) (unitsSMul φ u w) = w := by + rw [unitsSMul] + split_ifs with hcan + · have hncan : ¬ Cancels u w := (unitsSMul_cancels_iff _ _ _).1 hcan + unfold unitsSMul + simp only [dif_neg hncan] + simp [unitsSMulWithCancel, unitsSMulGroup, (d.compl u).equiv_snd_eq_inv_mul] + · have hcan2 : Cancels u w := not_not.1 (mt (unitsSMul_cancels_iff _ _ _).2 hcan) + unfold unitsSMul at hcan ⊢ + simp only [dif_pos hcan2] at hcan ⊢ + cases w using consRecOn with + | ofGroup => simp [Cancels] at hcan2 + | cons g u' w h1 h2 ih => + clear ih + simp [unitsSMulWithCancel, unitsSMulGroup] + cases hcan2.2 + have : ((d.compl (-u)).equiv w.head).1 = 1 := + (d.compl (-u)).equiv_fst_eq_one_of_mem_of_one_mem _ h1 + apply NormalWord.ext + · simp [this] + · simp [mul_assoc, Units.ext_iff, (d.compl (-u)).equiv_snd_eq_inv_mul, this] + +/-- the equivalence given by multiplication on the left by `t` -/ +@[simps] +noncomputable def unitsSMulEquiv : NormalWord d ≃ NormalWord d := +{ toFun := unitsSMul φ 1 + invFun := unitsSMul φ (-1), + left_inv := fun _ => by rw [unitsSMul_neg] + right_inv := fun w => by convert unitsSMul_neg _ _ w; simp } + +theorem unitsSMul_one_group_smul (g : A) (w : NormalWord d) : + unitsSMul φ 1 ((g : G) • w) = (φ g : G) • (unitsSMul φ 1 w) := by + unfold unitsSMul + have : Cancels 1 ((g : G) • w) ↔ Cancels 1 w := by + simp [Cancels, Subgroup.mul_mem_cancel_left] + by_cases hcan : Cancels 1 w + · simp [unitsSMulWithCancel, dif_pos (this.2 hcan), dif_pos hcan] + cases w using consRecOn + · simp [Cancels] at hcan + · simp only [smul_cons, consRecOn_cons, mul_smul] + rw [← mul_smul, ← Subgroup.coe_mul, ← map_mul φ] + rfl + · rw [dif_neg (mt this.1 hcan), dif_neg hcan] + simp [← mul_smul, mul_assoc, unitsSMulGroup] + +noncomputable instance : MulAction (HNNExtension G A B φ) (NormalWord d) := + MulAction.ofEndHom <| (MulAction.toEndHom (M := Equiv.Perm (NormalWord d))).comp + (HNNExtension.lift (MulAction.toPermHom _ _) (unitsSMulEquiv φ) <| by + intro a + ext : 1 + simp [unitsSMul_one_group_smul]) + +@[simp] +theorem prod_group_smul (g : G) (w : NormalWord d) : + (g • w).prod φ = of g * (w.prod φ) := by + simp [ReducedWord.prod, smul_def, mul_assoc] + +theorem of_smul_eq_smul (g : G) (w : NormalWord d) : + (of g : HNNExtension G A B φ) • w = g • w := by + simp [instHSMul, SMul.smul, MulAction.toEndHom] + +theorem t_smul_eq_unitsSMul (w : NormalWord d) : + (t : HNNExtension G A B φ) • w = unitsSMul φ 1 w := by + simp [instHSMul, SMul.smul, MulAction.toEndHom] + +theorem t_pow_smul_eq_unitsSMul (u : ℤˣ) (w : NormalWord d) : + (t ^ (u : ℤ) : HNNExtension G A B φ) • w = unitsSMul φ u w := by + simp [instHSMul, SMul.smul, MulAction.toEndHom] + rcases Int.units_eq_one_or u with (rfl | rfl) <;> simp [Equiv.Perm.inv_def] + +@[simp] +theorem prod_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') : + (cons g u w h1 h2).prod φ = of g * (t ^ (u : ℤ) * w.prod φ) := by + simp [ReducedWord.prod, cons, smul_def, mul_assoc] + +theorem prod_unitsSMul (u : ℤˣ) (w : NormalWord d) : + (unitsSMul φ u w).prod φ = (t^(u : ℤ) * w.prod φ : HNNExtension G A B φ) := by + rw [unitsSMul] + split_ifs with hcan + · cases w using consRecOn + · simp [Cancels] at hcan + · cases hcan.2 + simp [unitsSMulWithCancel] + rcases Int.units_eq_one_or u with (rfl | rfl) + · simp [equiv_eq_conj, mul_assoc] + · simp [equiv_symm_eq_conj, mul_assoc] + · simp [unitsSMulGroup] + rcases Int.units_eq_one_or u with (rfl | rfl) + · simp [equiv_eq_conj, mul_assoc, (d.compl _).equiv_snd_eq_inv_mul] + · simp [equiv_symm_eq_conj, mul_assoc, (d.compl _).equiv_snd_eq_inv_mul] + +@[simp] +theorem prod_empty : (empty : NormalWord d).prod φ = 1 := by + simp [ReducedWord.prod] + +@[simp] +theorem prod_smul (g : HNNExtension G A B φ) (w : NormalWord d) : + (g • w).prod φ = g * w.prod φ := by + induction g using induction_on generalizing w with + | of => simp [of_smul_eq_smul] + | t => simp [t_smul_eq_unitsSMul, prod_unitsSMul, mul_assoc] + | mul => simp_all [mul_smul, mul_assoc] + | inv x ih => + apply (mul_right_inj x).1 + rw [← ih] + simp + +@[simp] +theorem prod_smul_empty (w : NormalWord d) : + (w.prod φ) • empty = w := by + induction w using consRecOn with + | ofGroup => simp [ofGroup, ReducedWord.prod, of_smul_eq_smul, group_smul_def] + | cons g u w h1 h2 ih => + rw [prod_cons, ← mul_assoc, mul_smul, ih, mul_smul, t_pow_smul_eq_unitsSMul, + of_smul_eq_smul, unitsSMul] + rw [dif_neg (not_cancels_of_cons_hyp u w h2)] + simp [unitsSMulGroup, (d.compl u).equiv_snd_eq_inv_mul, mul_assoc, + (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1] + ext <;> simp + +variable (d) +/-- The equivalence between elements of the HNN extension and words in normal form. -/ +noncomputable def equiv : HNNExtension G A B φ ≃ NormalWord d := + { toFun := fun g => g • empty, + invFun := fun w => w.prod φ, + left_inv := fun g => by simp [prod_smul] + right_inv := fun w => by simp } + +theorem prod_injective : Injective + (fun w => w.prod φ : NormalWord d → HNNExtension G A B φ) := + (equiv φ d).symm.injective + +instance : FaithfulSMul (HNNExtension G A B φ) (NormalWord d) := + ⟨fun h => by simpa using congr_arg (fun w => w.prod φ) (h empty)⟩ + +end NormalWord + +open NormalWord + +theorem of_injective : Function.Injective (of : G → HNNExtension G A B φ) := by + rcases TransversalPair.nonempty G A B with ⟨d⟩ + refine Function.Injective.of_comp + (f := ((. • .) : HNNExtension G A B φ → NormalWord d → NormalWord d)) ?_ + intros _ _ h + exact eq_of_smul_eq_smul (fun w : NormalWord d => + by simp_all [Function.funext_iff, of_smul_eq_smul]) + +namespace ReducedWord + +theorem exists_normalWord_prod_eq + (d : TransversalPair G A B) (w : ReducedWord G A B) : + ∃ w' : NormalWord d, w'.prod φ = w.prod φ ∧ + w'.toList.map Prod.fst = w.toList.map Prod.fst ∧ + ∀ u ∈ w.toList.head?.map Prod.fst, + w'.head⁻¹ * w.head ∈ toSubgroup A B (-u) := by + suffices : ∀ w : ReducedWord G A B, + w.head = 1 → ∃ w' : NormalWord d, w'.prod φ = w.prod φ ∧ + w'.toList.map Prod.fst = w.toList.map Prod.fst ∧ + ∀ u ∈ w.toList.head?.map Prod.fst, + w'.head ∈ toSubgroup A B (-u) + · by_cases hw1 : w.head = 1 + · simp only [hw1, inv_mem_iff, mul_one] + exact this w hw1 + · rcases this ⟨1, w.toList, w.chain⟩ rfl with ⟨w', hw'⟩ + exact ⟨w.head • w', by + simpa [ReducedWord.prod, mul_assoc] using hw'⟩ + intro w hw1 + rcases w with ⟨g, l, chain⟩ + dsimp at hw1; subst hw1 + induction l with + | nil => + exact + ⟨{ head := 1 + toList := [] + mem_set := by simp + chain := List.chain'_nil }, by simp [prod]⟩ + | cons a l ih => + rcases ih (List.chain'_cons'.1 chain).2 with ⟨w', hw'1, hw'2, hw'3⟩ + clear ih + refine ⟨(t^(a.1 : ℤ) * of a.2 : HNNExtension G A B φ) • w', ?_, ?_⟩ + · rw [prod_smul, hw'1] + simp [ReducedWord.prod] + · have : ¬ Cancels a.1 (a.2 • w') := by + simp only [Cancels, group_smul_head, group_smul_toList, Option.map_eq_some', + Prod.exists, exists_and_right, exists_eq_right, not_and, not_exists] + intro hS x hx + have hx' := congr_arg (Option.map Prod.fst) hx + rw [← List.head?_map, hw'2, List.head?_map, Option.map_some'] at hx' + have : w'.head ∈ toSubgroup A B a.fst := by + simpa using hw'3 _ hx' + rw [mul_mem_cancel_right this] at hS + have : a.fst = -a.fst := by + have hl : l ≠ [] := by rintro rfl; simp_all + have : a.fst = (l.head hl).fst := (List.chain'_cons'.1 chain).1 (l.head hl) + (List.head?_eq_head _ _) hS + rwa [List.head?_eq_head _ hl, Option.map_some', ← this, Option.some_inj] at hx' + simp at this + erw [List.map_cons, mul_smul, of_smul_eq_smul, NormalWord.group_smul_def, + t_pow_smul_eq_unitsSMul, unitsSMul, dif_neg this, ← hw'2] + simp [mul_assoc, unitsSMulGroup, (d.compl _).coe_equiv_snd_eq_one_iff_mem] + +/-- Two reduced words representing the same element of the `HNNExtension G A B φ` have the same +length corresponding list, with the same pattern of occurences of `t^1` and `t^(-1)`, +and also the `head` is in the same left coset of `toSubgroup A B (-u)`, where `u : ℤˣ` +is the exponent of the first occurence of `t` in the word. -/ +theorem map_fst_eq_and_of_prod_eq {w₁ w₂ : ReducedWord G A B} + (hprod : w₁.prod φ = w₂.prod φ) : + w₁.toList.map Prod.fst = w₂.toList.map Prod.fst ∧ + ∀ u ∈ w₁.toList.head?.map Prod.fst, + w₁.head⁻¹ * w₂.head ∈ toSubgroup A B (-u) := by + rcases TransversalPair.nonempty G A B with ⟨d⟩ + rcases exists_normalWord_prod_eq φ d w₁ with ⟨w₁', hw₁'1, hw₁'2, hw₁'3⟩ + rcases exists_normalWord_prod_eq φ d w₂ with ⟨w₂', hw₂'1, hw₂'2, hw₂'3⟩ + have : w₁' = w₂' := + NormalWord.prod_injective φ d (by dsimp only; rw [hw₁'1, hw₂'1, hprod]) + subst this + refine ⟨by rw [← hw₁'2, hw₂'2], ?_⟩ + simp only [← leftCoset_eq_iff] at * + intro u hu + rw [← hw₁'3 _ hu, ← hw₂'3 _] + rwa [← List.head?_map, ← hw₂'2, hw₁'2, List.head?_map] + +/-- **Britton's Lemma**. Any reduced word whose product is an element of `G`, has no +occurences of `t`. -/ +theorem toList_eq_nil_of_mem_of_range (w : ReducedWord G A B) + (hw : w.prod φ ∈ (of.range : Subgroup (HNNExtension G A B φ))) : + w.toList = [] := by + rcases hw with ⟨g, hg⟩ + let w' : ReducedWord G A B := { ReducedWord.empty G A B with head := g } + have : w.prod φ = w'.prod φ := by simp [ReducedWord.prod, hg] + simpa using (map_fst_eq_and_of_prod_eq φ this).1 + +end ReducedWord + +end HNNExtension From 513de8fafde60abce3c8b693708df4364d8c6b76 Mon Sep 17 00:00:00 2001 From: Chris Hughes Date: Sun, 3 Sep 2023 14:16:47 +0100 Subject: [PATCH 10/10] swap direction of iff --- Mathlib/GroupTheory/Complement.lean | 28 +- .../SpecificGroups/HNNExtension.lean | 652 ------------------ 2 files changed, 14 insertions(+), 666 deletions(-) delete mode 100644 Mathlib/GroupTheory/SpecificGroups/HNNExtension.lean diff --git a/Mathlib/GroupTheory/Complement.lean b/Mathlib/GroupTheory/Complement.lean index a34d5569a48a4..de1fa1d67c19c 100644 --- a/Mathlib/GroupTheory/Complement.lean +++ b/Mathlib/GroupTheory/Complement.lean @@ -353,33 +353,33 @@ theorem equiv_fst_eq_mul_inv (g : G) : ↑(hST.equiv g).fst = g * ((hST.equiv g) theorem equiv_snd_eq_inv_mul (g : G) : ↑(hST.equiv g).snd = ((hST.equiv g).fst : G)⁻¹ * g := eq_inv_mul_of_mul_eq (hST.equiv_fst_mul_equiv_snd g) -theorem leftCosetEquivalence_iff_equiv_fst_eq {g₁ g₂ : G} : - LeftCosetEquivalence K g₁ g₂ ↔ (hSK.equiv g₁).fst = (hSK.equiv g₂).fst := by +theorem equiv_fst_eq_iff_leftCosetEquivalence {g₁ g₂ : G} : + (hSK.equiv g₁).fst = (hSK.equiv g₂).fst ↔ LeftCosetEquivalence K g₁ g₂ := by rw [LeftCosetEquivalence, leftCoset_eq_iff] constructor + · intro h + rw [← hSK.equiv_fst_mul_equiv_snd g₂, ←hSK.equiv_fst_mul_equiv_snd g₁, ← h, + mul_inv_rev, ← mul_assoc, inv_mul_cancel_right, ← coe_inv, ← coe_mul] + exact Subtype.property _ · intro h apply (mem_leftTransversals_iff_existsUnique_inv_mul_mem.1 hSK g₁).unique · simp [equiv_fst_eq_mul_inv] · rw [SetLike.mem_coe, ← mul_mem_cancel_right h] simp [equiv_fst_eq_mul_inv, ← mul_assoc] - · intro h - rw [← hSK.equiv_fst_mul_equiv_snd g₂, ←hSK.equiv_fst_mul_equiv_snd g₁, ← h, - mul_inv_rev, ← mul_assoc, inv_mul_cancel_right, ← coe_inv, ← coe_mul] - exact Subtype.property _ -theorem rightCosetEquivalence_iff_equiv_snd_eq {g₁ g₂ : G} : - RightCosetEquivalence H g₁ g₂ ↔ (hHT.equiv g₁).snd = (hHT.equiv g₂).snd := by +theorem equiv_snd_eq_iff_rightCosetEquivalence {g₁ g₂ : G} : + (hHT.equiv g₁).snd = (hHT.equiv g₂).snd ↔ RightCosetEquivalence H g₁ g₂ := by rw [RightCosetEquivalence, rightCoset_eq_iff] constructor + · intro h + rw [← hHT.equiv_fst_mul_equiv_snd g₂, ←hHT.equiv_fst_mul_equiv_snd g₁, ← h, + mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← coe_inv, ← coe_mul] + exact Subtype.property _ · intro h apply (mem_rightTransversals_iff_existsUnique_mul_inv_mem.1 hHT g₁).unique · simp [equiv_snd_eq_inv_mul] · rw [SetLike.mem_coe, ← mul_mem_cancel_left h] simp [equiv_snd_eq_inv_mul, mul_assoc] - · intro h - rw [← hHT.equiv_fst_mul_equiv_snd g₂, ←hHT.equiv_fst_mul_equiv_snd g₁, ← h, - mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← coe_inv, ← coe_mul] - exact Subtype.property _ theorem leftCosetEquivalence_equiv_fst (g : G) : LeftCosetEquivalence K g ((hSK.equiv g).fst : G) := by @@ -415,7 +415,7 @@ theorem equiv_fst_eq_one_of_mem_of_one_mem {g : G} (h1 : 1 ∈ S) (hg : g ∈ T) theorem equiv_mul_right (g : G) (k : K) : hSK.equiv (g * k) = ((hSK.equiv g).fst, (hSK.equiv g).snd * k) := by have : (hSK.equiv (g * k)).fst = (hSK.equiv g).fst := - hSK.leftCosetEquivalence_iff_equiv_fst_eq.1 + hSK.equiv_fst_eq_iff_leftCosetEquivalence.2 (by simp [LeftCosetEquivalence, leftCoset_eq_iff]) ext · rw [this] @@ -429,7 +429,7 @@ theorem equiv_mul_right_of_mem {g k : G} (h : k ∈ K) : theorem equiv_mul_left (h : H) (g : G) : hHT.equiv (h * g) = (h * (hHT.equiv g).fst, (hHT.equiv g).snd) := by have : (hHT.equiv (h * g)).snd = (hHT.equiv g).snd := - hHT.rightCosetEquivalence_iff_equiv_snd_eq.1 + hHT.equiv_snd_eq_iff_rightCosetEquivalence.2 (by simp [RightCosetEquivalence, rightCoset_eq_iff]) ext · rw [coe_mul, equiv_fst_eq_mul_inv, this, equiv_fst_eq_mul_inv, mul_assoc] diff --git a/Mathlib/GroupTheory/SpecificGroups/HNNExtension.lean b/Mathlib/GroupTheory/SpecificGroups/HNNExtension.lean deleted file mode 100644 index 292b9a2bb6c75..0000000000000 --- a/Mathlib/GroupTheory/SpecificGroups/HNNExtension.lean +++ /dev/null @@ -1,652 +0,0 @@ -/- -Copyright (c) 2023 Chris Hughes. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Chris Hughes --/ - -import Mathlib.GroupTheory.SpecificGroups.Coprod -import Mathlib.GroupTheory.Complement - -/-! - -## HNN Extensions of Groups - -This file defines the HNN extensions of groups. - -## 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`. - --/ - -open Monoid Coprod Multiplicative Subgroup Function - -/-- The relation we quotient the coproduct by to form an `HNNExtension`. -/ -def HNNExtension.con (G : Type*) [Group G] (A B : Subgroup G) (φ : A ≃* B) : - Con (G ∗ Multiplicative ℤ) := - conGen (fun x y => ∃ (a : A), - x = inr (ofAdd 1) * inl (a : G) ∧ - y = inl (φ a : G) * inr (ofAdd 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 canoncial -map from `G` into the `HNNExtension`. -/ -def HNNExtension (G : Type*) [Group G] (A B : Subgroup G) (φ : A ≃* B) : Type _ := - (HNNExtension.con G A B φ).Quotient - -variable {G : Type*} [Group G] {A B : Subgroup G} {φ : A ≃* B} {H : Type*} - [Group H] {M : Type*} [Monoid M] - -instance : Group (HNNExtension G A B φ) := by - delta HNNExtension; infer_instance - -namespace HNNExtension - -/-- The canonical embedding `G →* HNNExtension G A B φ` -/ -def of : G →* HNNExtension G A B φ := - (HNNExtension.con G A B φ).mk'.comp inl - -/-- The stable letter of the `HNNExtension` -/ -def t : HNNExtension G A B φ := - (HNNExtension.con G A B φ).mk'.comp inr (ofAdd 1) - -theorem t_mul_of (a : A) : - t * (of (a : G) : HNNExtension G A B φ) = of (φ a : G) * t := - (Con.eq _).2 <| ConGen.Rel.of _ _ <| ⟨a, by simp⟩ - -theorem of_mul_t (b : B) : - (of (b : G) : HNNExtension G A B φ) * t = t * of (φ.symm b : G) := by - rw [t_mul_of]; simp - -theorem equiv_eq_conj (a : A) : - (of (φ a : G) : HNNExtension G A B φ) = t * of (a : G) * t⁻¹ := by - rw [t_mul_of]; simp - -theorem equiv_symm_eq_conj (b : B) : - (of (φ.symm b : G) : HNNExtension G A B φ) = t⁻¹ * of (b : G) * t := by - rw [mul_assoc, of_mul_t]; simp - -theorem inv_t_mul_of (b : B) : - t⁻¹ * (of (b : G) : HNNExtension G A B φ) = of (φ.symm b : G) * t⁻¹ := by - rw [equiv_symm_eq_conj]; simp - -theorem of_mul_inv_t (a : A) : - (of (a : G) : HNNExtension G A B φ) * t⁻¹ = t⁻¹ * of (φ a : G) := by - rw [equiv_eq_conj]; simp [mul_assoc] - -/-- Define a function `HNNExtension G A B φ →* H`, by defining it on `G` and `t` -/ -def lift (f : G →* H) (x : H) (hx : ∀ a : A, x * f ↑a = f (φ a : G) * x) : - HNNExtension G A B φ →* H := - Con.lift _ (Coprod.lift f (zpowersHom H x)) (Con.conGen_le <| by - rintro _ _ ⟨a, rfl, rfl⟩ - simp [hx]) - -@[simp] -theorem lift_t (f : G →* H) (x : H) (hx : ∀ a : A, x * f ↑a = f (φ a : G) * x) : - lift f x hx t = x := by - delta HNNExtension; simp [lift, t] - -@[simp] -theorem lift_of (f : G →* H) (x : H) (hx : ∀ a : A, x * f ↑a = f (φ a : G) * x) (g : G) : - lift f x hx (of g) = f g := by - delta HNNExtension; simp [lift, of] - -@[ext high] -theorem hom_ext {f g : HNNExtension G A B φ →* M} - (hg : f.comp of = g.comp of) (ht : f t = g t) : f = g := - (MonoidHom.cancel_right Con.mk'_surjective).mp <| - Coprod.ext_hom _ _ hg (MonoidHom.ext_mint ht) - -@[elab_as_elim] -theorem induction_on {motive : HNNExtension G A B φ → Prop} - (x : HNNExtension G A B φ) (of : ∀ g, motive (of g)) - (t : motive t) (mul : ∀ x y, motive x → motive y → motive (x * y)) - (inv : ∀ x, motive x → motive x⁻¹) : motive x := by - let S : Subgroup (HNNExtension G A B φ) := - { carrier := setOf motive - one_mem' := by simpa using of 1 - mul_mem' := mul _ _ - inv_mem' := inv _ } - let f : HNNExtension G A B φ →* S := - lift (HNNExtension.of.codRestrict S of) - ⟨HNNExtension.t, t⟩ (by intro a; ext; simp [equiv_eq_conj, mul_assoc]) - have hf : S.subtype.comp f = MonoidHom.id _ := - hom_ext (by ext; simp) (by simp) - show motive (MonoidHom.id _ x) - rw [← hf] - exact (f x).2 - -variable (A B φ) - -/-- 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 : ℤ)`. -/ -def toSubgroup (u : ℤˣ) : Subgroup G := - if u = 1 then A else B - -@[simp] -theorem toSubgroup_one : toSubgroup A B 1 = A := rfl - -@[simp] -theorem toSubgroup_neg_one : toSubgroup A B (-1) = B := rfl - -variable {A B} - -/-- 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`. -/ -def toSubgroupEquiv (u : ℤˣ) : toSubgroup A B u ≃* toSubgroup A B (-u) := - if hu : u = 1 then hu ▸ φ else by - convert φ.symm <;> - cases Int.units_eq_one_or u <;> simp_all - -@[simp] -theorem toSubgroupEquiv_one : toSubgroupEquiv φ 1 = φ := rfl - -@[simp] -theorem toSubgroupEquiv_neg_one : toSubgroupEquiv φ (-1) = φ.symm := rfl - -@[simp] -theorem toSubgroupEquiv_neg_apply (u : ℤˣ) (a : toSubgroup A B u) : - (toSubgroupEquiv φ (-u) (toSubgroupEquiv φ u a) : G) = a := by - rcases Int.units_eq_one_or u with rfl | rfl - · simp - · simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, SetLike.coe_eq_coe] - exact φ.apply_symm_apply a - -namespace NormalWord - -variable (G A B) -/-- 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`. -/ -structure TransversalPair : Type _ := - /-- The transversal of each subgroup -/ - ( set : ℤˣ → Set G ) - -- /-- The chosen element of the subgroup itself is the identity -/ - -- ( one_mem : ∀u, 1 ∈ set u ) - /-- We have exactly one element of each coset of the subgroup -/ - ( compl : ∀ u, IsComplement (toSubgroup A B u : Subgroup G) (set u) ) - -instance TransversalPair.nonempty : Nonempty (TransversalPair G A B) := by - have := fun u => exists_right_transversal (H := toSubgroup A B u) (1 : G) - simp only [Classical.skolem] at this - rcases this with ⟨t, ht⟩ - apply Nonempty.intro - exact - { set := t - -- one_mem := fun i => (ht i).2 - compl := fun i => (ht i).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`. -/ -structure ReducedWord : Type _ := - /-- Every `ReduceddWord` 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. -/ - ( head : G ) - /-- The list of pairs `(ℤˣ × G)`, where each pair `(u, g)` represents the element `t^u * g` of - `HNNExtension G A B φ` -/ - ( toList : List (ℤˣ × G) ) - /-- There are no sequences of the form `t^u * g * t^-u` where `g ∈ toSubgroup A B u` -/ - ( chain : toList.Chain' (fun a b => a.2 ∈ toSubgroup A B a.1 → a.1 = b.1) ) - -/-- The empty reduced word. -/ -@[simps] -def ReducedWord.empty : ReducedWord G A B := - { head := 1 - toList := [] - chain := List.chain'_nil } - -variable {G A B} -/-- The product of a `ReducedWord` as an element of the `HNNExtension` -/ -def ReducedWord.prod : ReducedWord G A B → HNNExtension G A B φ := - fun w => of w.head * (w.toList.map (fun x => t ^ (x.1 : ℤ) * of x.2)).prod - -/-- 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` -/ -structure _root_.HNNExtension.NormalWord (d : TransversalPair G A B) - extends ReducedWord G A B : Type _ := - /-- Every element `g : G` in the list is the chosen element of its coset -/ - ( mem_set : ∀ (u : ℤˣ) (g : G), (u, g) ∈ toList → g ∈ d.set u ) - -variable {d : TransversalPair G A B} - -@[ext] -theorem ext {w w' : NormalWord d} - (h1 : w.head = w'.head) (h2 : w.toList = w'.toList): w = w' := by - rcases w with ⟨⟨⟩, _⟩; cases w'; simp_all - -/-- The empty word -/ -@[simps] -def empty : NormalWord d := - { head := 1 - toList := [] - mem_set := by simp - chain := List.chain'_nil } - -/-- The `NormalWord` representing an element `g` of the group `G`, which is just the element `g` -itself. -/ -@[simps] -def ofGroup (g : G) : NormalWord d := - { head := g - toList := [] - mem_set := by simp - chain := List.chain'_nil } - -instance : Inhabited (NormalWord d) := ⟨empty⟩ - -instance : MulAction G (NormalWord d) := - { smul := fun g w => { w with head := g * w.head } - one_smul := by simp [instHSMul] - mul_smul := by simp [instHSMul, mul_assoc] } - -theorem group_smul_def (g : G) (w : NormalWord d) : - g • w = { w with head := g * w.head } := rfl - -@[simp] -theorem group_smul_head (g : G) (w : NormalWord d) : (g • w).head = g * w.head := rfl - -@[simp] -theorem group_smul_toList (g : G) (w : NormalWord d) : (g • w).toList = w.toList := rfl - -instance : FaithfulSMul G (NormalWord d) := ⟨by simp [group_smul_def]⟩ - -/-- 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 --/ -@[simps] -def 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') : - NormalWord d := - { head := g, - toList := (u, w.head) :: w.toList, - mem_set := by - intro u' g' h' - simp only [List.mem_cons, Prod.mk.injEq] at h' - rcases h' with ⟨rfl, rfl⟩ | h' - · exact h1 - · exact w.mem_set _ _ h' - chain := by - refine List.chain'_cons'.2 ⟨?_, w.chain⟩ - rintro ⟨ u', g'⟩ hu' hw1 - exact h2 _ (by simp_all) hw1 } - -/-- A recursor to induct on a `NormalWord`, by proving the propert is preserved under `cons` -/ -@[elab_as_elim] -def consRecOn {motive : NormalWord d → Sort*} (w : NormalWord d) - (ofGroup : ∀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 := by - rcases w with ⟨⟨g, l, chain⟩, mem_set⟩ - induction l generalizing g with - | nil => exact ofGroup _ - | cons a l ih => - exact cons g a.1 - { head := a.2 - toList := l - mem_set := fun _ _ h => mem_set _ _ (List.mem_cons_of_mem _ h), - chain := (List.chain'_cons'.1 chain).2 } - (mem_set a.1 a.2 (List.mem_cons_self _ _)) - (by simpa using (List.chain'_cons'.1 chain).1) - (ih _ _ _) - -@[simp] -theorem consRecOn_ofGroup {motive : NormalWord d → Sort*} - (g : G) (ofGroup : ∀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 (.ofGroup g) ofGroup cons = ofGroup g := rfl - -@[simp] -theorem consRecOn_cons {motive : NormalWord d → Sort*} - (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, 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 (.cons g u w h1 h2) ofGroup cons = cons g u w h1 h2 - (consRecOn w ofGroup cons) := rfl - -@[simp] -theorem smul_cons (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 := - rfl - -@[simp] -theorem smul_ofGroup (g₁ g₂ : G) : - g₁ • (ofGroup g₂ : NormalWord d) = ofGroup (g₁ * g₂) := rfl - -variable (d) -/-- The action of `t^u` on `ofGroup g`. The normal form will be -`a * t^u * g'` where `a ∈ toSubgroup A B (-u)` -/ -noncomputable def unitsSMulGroup (u : ℤˣ) (g : G) : - (toSubgroup A B (-u)) × d.set u := - let g' := (d.compl u).equiv g - (toSubgroupEquiv φ u g'.1, g'.2) - -theorem unitsSMulGroup_snd (u : ℤˣ) (g : G) : - (unitsSMulGroup φ d u g).2 = ((d.compl u).equiv g).2 := by - rcases Int.units_eq_one_or u with rfl | rfl <;> rfl - -variable {d} [DecidableEq G] - -/-- `Cancels u w` is a predicate expressing whether `t^u` cancels with some occurence -of `t^-u` when when we multiply `t^u` by `w`. -/ -def Cancels (u : ℤˣ) (w : NormalWord d) : Prop := - (w.head ∈ (toSubgroup A B u : Subgroup G)) ∧ w.toList.head?.map Prod.fst = some (-u) - -/-- Multiplying `t^u` by `w` in the special case where cancellation happens -/ -def unitsSMulWithCancel (u : ℤˣ) (w : NormalWord d) : Cancels u w → NormalWord d := - consRecOn w - (by simp [Cancels, ofGroup]; tauto) - (fun g u' w h1 h2 _ can => - (toSubgroupEquiv φ u ⟨g, can.1⟩ : G) • w) - -/-- Multiplying `t^u` by a `NormalWord`, `w` and putting the result in normal form. -/ -noncomputable def unitsSMul (u : ℤˣ) (w : NormalWord d) : NormalWord d := - letI := Classical.dec - if h : Cancels u w - then unitsSMulWithCancel φ u w h - else let g' := unitsSMulGroup φ d u w.head - cons g'.1 u ((g'.2 * w.head⁻¹ : G) • w) - (by simp) - (by - simp only [group_smul_toList, Option.mem_def, Option.map_eq_some', Prod.exists, - exists_and_right, exists_eq_right, group_smul_head, inv_mul_cancel_right, - forall_exists_index, unitsSMulGroup] - simp only [Cancels, Option.map_eq_some', Prod.exists, exists_and_right, exists_eq_right, - not_and, not_exists] at h - intro u' x hx hmem - have : w.head ∈ toSubgroup A B u := by - have := (d.compl u).rightCosetEquivalence_equiv_snd w.head - rw [RightCosetEquivalence, rightCoset_eq_iff, mul_mem_cancel_left hmem] at this - simp_all - have := h this x - simp_all [Int.units_ne_iff_eq_neg]) - -/-- A condition for not cancelling whose hypothese are the same as those of the `cons` function. -/ -theorem not_cancels_of_cons_hyp (u : ℤˣ) (w : NormalWord d) - (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, - w.head ∈ toSubgroup A B u → u = u') : - ¬ Cancels u w := by - simp only [Cancels, Option.map_eq_some', Prod.exists, - exists_and_right, exists_eq_right, not_and, not_exists] - intro hw x hx - rw [hx] at h2 - simpa using h2 (-u) rfl hw - -theorem unitsSMul_cancels_iff (u : ℤˣ) (w : NormalWord d) : - Cancels (-u) (unitsSMul φ u w) ↔ ¬ Cancels u w := by - by_cases h : Cancels u w - · simp only [unitsSMul, dif_pos trivial, h, iff_false] - induction w using consRecOn with - | ofGroup => simp [Cancels, unitsSMulWithCancel] - | cons g u' w h1 h2 _ => - intro hc - apply not_cancels_of_cons_hyp _ _ h2 - simp only [Cancels, cons_head, cons_toList, List.head?_cons, - Option.map_some', Option.some.injEq] at h - cases h.2 - simpa [Cancels, unitsSMulWithCancel, - Subgroup.mul_mem_cancel_left] using hc - · simp only [unitsSMul, dif_neg h] - simpa [Cancels] using h - -theorem unitsSMul_neg (u : ℤˣ) (w : NormalWord d) : - unitsSMul φ (-u) (unitsSMul φ u w) = w := by - rw [unitsSMul] - split_ifs with hcan - · have hncan : ¬ Cancels u w := (unitsSMul_cancels_iff _ _ _).1 hcan - unfold unitsSMul - simp only [dif_neg hncan] - simp [unitsSMulWithCancel, unitsSMulGroup, (d.compl u).equiv_snd_eq_inv_mul] - · have hcan2 : Cancels u w := not_not.1 (mt (unitsSMul_cancels_iff _ _ _).2 hcan) - unfold unitsSMul at hcan ⊢ - simp only [dif_pos hcan2] at hcan ⊢ - cases w using consRecOn with - | ofGroup => simp [Cancels] at hcan2 - | cons g u' w h1 h2 ih => - clear ih - simp [unitsSMulWithCancel, unitsSMulGroup] - cases hcan2.2 - have : ((d.compl (-u)).equiv w.head).1 = 1 := - (d.compl (-u)).equiv_fst_eq_one_of_mem_of_one_mem _ h1 - apply NormalWord.ext - · simp [this] - · simp [mul_assoc, Units.ext_iff, (d.compl (-u)).equiv_snd_eq_inv_mul, this] - -/-- the equivalence given by multiplication on the left by `t` -/ -@[simps] -noncomputable def unitsSMulEquiv : NormalWord d ≃ NormalWord d := -{ toFun := unitsSMul φ 1 - invFun := unitsSMul φ (-1), - left_inv := fun _ => by rw [unitsSMul_neg] - right_inv := fun w => by convert unitsSMul_neg _ _ w; simp } - -theorem unitsSMul_one_group_smul (g : A) (w : NormalWord d) : - unitsSMul φ 1 ((g : G) • w) = (φ g : G) • (unitsSMul φ 1 w) := by - unfold unitsSMul - have : Cancels 1 ((g : G) • w) ↔ Cancels 1 w := by - simp [Cancels, Subgroup.mul_mem_cancel_left] - by_cases hcan : Cancels 1 w - · simp [unitsSMulWithCancel, dif_pos (this.2 hcan), dif_pos hcan] - cases w using consRecOn - · simp [Cancels] at hcan - · simp only [smul_cons, consRecOn_cons, mul_smul] - rw [← mul_smul, ← Subgroup.coe_mul, ← map_mul φ] - rfl - · rw [dif_neg (mt this.1 hcan), dif_neg hcan] - simp [← mul_smul, mul_assoc, unitsSMulGroup] - -noncomputable instance : MulAction (HNNExtension G A B φ) (NormalWord d) := - MulAction.ofEndHom <| (MulAction.toEndHom (M := Equiv.Perm (NormalWord d))).comp - (HNNExtension.lift (MulAction.toPermHom _ _) (unitsSMulEquiv φ) <| by - intro a - ext : 1 - simp [unitsSMul_one_group_smul]) - -@[simp] -theorem prod_group_smul (g : G) (w : NormalWord d) : - (g • w).prod φ = of g * (w.prod φ) := by - simp [ReducedWord.prod, smul_def, mul_assoc] - -theorem of_smul_eq_smul (g : G) (w : NormalWord d) : - (of g : HNNExtension G A B φ) • w = g • w := by - simp [instHSMul, SMul.smul, MulAction.toEndHom] - -theorem t_smul_eq_unitsSMul (w : NormalWord d) : - (t : HNNExtension G A B φ) • w = unitsSMul φ 1 w := by - simp [instHSMul, SMul.smul, MulAction.toEndHom] - -theorem t_pow_smul_eq_unitsSMul (u : ℤˣ) (w : NormalWord d) : - (t ^ (u : ℤ) : HNNExtension G A B φ) • w = unitsSMul φ u w := by - simp [instHSMul, SMul.smul, MulAction.toEndHom] - rcases Int.units_eq_one_or u with (rfl | rfl) <;> simp [Equiv.Perm.inv_def] - -@[simp] -theorem prod_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') : - (cons g u w h1 h2).prod φ = of g * (t ^ (u : ℤ) * w.prod φ) := by - simp [ReducedWord.prod, cons, smul_def, mul_assoc] - -theorem prod_unitsSMul (u : ℤˣ) (w : NormalWord d) : - (unitsSMul φ u w).prod φ = (t^(u : ℤ) * w.prod φ : HNNExtension G A B φ) := by - rw [unitsSMul] - split_ifs with hcan - · cases w using consRecOn - · simp [Cancels] at hcan - · cases hcan.2 - simp [unitsSMulWithCancel] - rcases Int.units_eq_one_or u with (rfl | rfl) - · simp [equiv_eq_conj, mul_assoc] - · simp [equiv_symm_eq_conj, mul_assoc] - · simp [unitsSMulGroup] - rcases Int.units_eq_one_or u with (rfl | rfl) - · simp [equiv_eq_conj, mul_assoc, (d.compl _).equiv_snd_eq_inv_mul] - · simp [equiv_symm_eq_conj, mul_assoc, (d.compl _).equiv_snd_eq_inv_mul] - -@[simp] -theorem prod_empty : (empty : NormalWord d).prod φ = 1 := by - simp [ReducedWord.prod] - -@[simp] -theorem prod_smul (g : HNNExtension G A B φ) (w : NormalWord d) : - (g • w).prod φ = g * w.prod φ := by - induction g using induction_on generalizing w with - | of => simp [of_smul_eq_smul] - | t => simp [t_smul_eq_unitsSMul, prod_unitsSMul, mul_assoc] - | mul => simp_all [mul_smul, mul_assoc] - | inv x ih => - apply (mul_right_inj x).1 - rw [← ih] - simp - -@[simp] -theorem prod_smul_empty (w : NormalWord d) : - (w.prod φ) • empty = w := by - induction w using consRecOn with - | ofGroup => simp [ofGroup, ReducedWord.prod, of_smul_eq_smul, group_smul_def] - | cons g u w h1 h2 ih => - rw [prod_cons, ← mul_assoc, mul_smul, ih, mul_smul, t_pow_smul_eq_unitsSMul, - of_smul_eq_smul, unitsSMul] - rw [dif_neg (not_cancels_of_cons_hyp u w h2)] - simp [unitsSMulGroup, (d.compl u).equiv_snd_eq_inv_mul, mul_assoc, - (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1] - ext <;> simp - -variable (d) -/-- The equivalence between elements of the HNN extension and words in normal form. -/ -noncomputable def equiv : HNNExtension G A B φ ≃ NormalWord d := - { toFun := fun g => g • empty, - invFun := fun w => w.prod φ, - left_inv := fun g => by simp [prod_smul] - right_inv := fun w => by simp } - -theorem prod_injective : Injective - (fun w => w.prod φ : NormalWord d → HNNExtension G A B φ) := - (equiv φ d).symm.injective - -instance : FaithfulSMul (HNNExtension G A B φ) (NormalWord d) := - ⟨fun h => by simpa using congr_arg (fun w => w.prod φ) (h empty)⟩ - -end NormalWord - -open NormalWord - -theorem of_injective : Function.Injective (of : G → HNNExtension G A B φ) := by - rcases TransversalPair.nonempty G A B with ⟨d⟩ - refine Function.Injective.of_comp - (f := ((. • .) : HNNExtension G A B φ → NormalWord d → NormalWord d)) ?_ - intros _ _ h - exact eq_of_smul_eq_smul (fun w : NormalWord d => - by simp_all [Function.funext_iff, of_smul_eq_smul]) - -namespace ReducedWord - -theorem exists_normalWord_prod_eq - (d : TransversalPair G A B) (w : ReducedWord G A B) : - ∃ w' : NormalWord d, w'.prod φ = w.prod φ ∧ - w'.toList.map Prod.fst = w.toList.map Prod.fst ∧ - ∀ u ∈ w.toList.head?.map Prod.fst, - w'.head⁻¹ * w.head ∈ toSubgroup A B (-u) := by - suffices : ∀ w : ReducedWord G A B, - w.head = 1 → ∃ w' : NormalWord d, w'.prod φ = w.prod φ ∧ - w'.toList.map Prod.fst = w.toList.map Prod.fst ∧ - ∀ u ∈ w.toList.head?.map Prod.fst, - w'.head ∈ toSubgroup A B (-u) - · by_cases hw1 : w.head = 1 - · simp only [hw1, inv_mem_iff, mul_one] - exact this w hw1 - · rcases this ⟨1, w.toList, w.chain⟩ rfl with ⟨w', hw'⟩ - exact ⟨w.head • w', by - simpa [ReducedWord.prod, mul_assoc] using hw'⟩ - intro w hw1 - rcases w with ⟨g, l, chain⟩ - dsimp at hw1; subst hw1 - induction l with - | nil => - exact - ⟨{ head := 1 - toList := [] - mem_set := by simp - chain := List.chain'_nil }, by simp [prod]⟩ - | cons a l ih => - rcases ih (List.chain'_cons'.1 chain).2 with ⟨w', hw'1, hw'2, hw'3⟩ - clear ih - refine ⟨(t^(a.1 : ℤ) * of a.2 : HNNExtension G A B φ) • w', ?_, ?_⟩ - · rw [prod_smul, hw'1] - simp [ReducedWord.prod] - · have : ¬ Cancels a.1 (a.2 • w') := by - simp only [Cancels, group_smul_head, group_smul_toList, Option.map_eq_some', - Prod.exists, exists_and_right, exists_eq_right, not_and, not_exists] - intro hS x hx - have hx' := congr_arg (Option.map Prod.fst) hx - rw [← List.head?_map, hw'2, List.head?_map, Option.map_some'] at hx' - have : w'.head ∈ toSubgroup A B a.fst := by - simpa using hw'3 _ hx' - rw [mul_mem_cancel_right this] at hS - have : a.fst = -a.fst := by - have hl : l ≠ [] := by rintro rfl; simp_all - have : a.fst = (l.head hl).fst := (List.chain'_cons'.1 chain).1 (l.head hl) - (List.head?_eq_head _ _) hS - rwa [List.head?_eq_head _ hl, Option.map_some', ← this, Option.some_inj] at hx' - simp at this - erw [List.map_cons, mul_smul, of_smul_eq_smul, NormalWord.group_smul_def, - t_pow_smul_eq_unitsSMul, unitsSMul, dif_neg this, ← hw'2] - simp [mul_assoc, unitsSMulGroup, (d.compl _).coe_equiv_snd_eq_one_iff_mem] - -/-- Two reduced words representing the same element of the `HNNExtension G A B φ` have the same -length corresponding list, with the same pattern of occurences of `t^1` and `t^(-1)`, -and also the `head` is in the same left coset of `toSubgroup A B (-u)`, where `u : ℤˣ` -is the exponent of the first occurence of `t` in the word. -/ -theorem map_fst_eq_and_of_prod_eq {w₁ w₂ : ReducedWord G A B} - (hprod : w₁.prod φ = w₂.prod φ) : - w₁.toList.map Prod.fst = w₂.toList.map Prod.fst ∧ - ∀ u ∈ w₁.toList.head?.map Prod.fst, - w₁.head⁻¹ * w₂.head ∈ toSubgroup A B (-u) := by - rcases TransversalPair.nonempty G A B with ⟨d⟩ - rcases exists_normalWord_prod_eq φ d w₁ with ⟨w₁', hw₁'1, hw₁'2, hw₁'3⟩ - rcases exists_normalWord_prod_eq φ d w₂ with ⟨w₂', hw₂'1, hw₂'2, hw₂'3⟩ - have : w₁' = w₂' := - NormalWord.prod_injective φ d (by dsimp only; rw [hw₁'1, hw₂'1, hprod]) - subst this - refine ⟨by rw [← hw₁'2, hw₂'2], ?_⟩ - simp only [← leftCoset_eq_iff] at * - intro u hu - rw [← hw₁'3 _ hu, ← hw₂'3 _] - rwa [← List.head?_map, ← hw₂'2, hw₁'2, List.head?_map] - -/-- **Britton's Lemma**. Any reduced word whose product is an element of `G`, has no -occurences of `t`. -/ -theorem toList_eq_nil_of_mem_of_range (w : ReducedWord G A B) - (hw : w.prod φ ∈ (of.range : Subgroup (HNNExtension G A B φ))) : - w.toList = [] := by - rcases hw with ⟨g, hg⟩ - let w' : ReducedWord G A B := { ReducedWord.empty G A B with head := g } - have : w.prod φ = w'.prod φ := by simp [ReducedWord.prod, hg] - simpa using (map_fst_eq_and_of_prod_eq φ this).1 - -end ReducedWord - -end HNNExtension