Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.FreeGroupLift
1import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Basic
3/-!
4# Free-group lifts modulo relators
6This module relates reduced words and FreeGroup.mk, then proves that lifts
7whose generator images agree modulo a relator normal closure agree on every
8free-group word.
9-/
11namespace ReidemeisterSchreier.Discrete.Presentations
13variable {G H : Type*} [Group G] [Group H]
15section NormalClosure
17variable {R S : Set G} {r a b : G}
19section FreeGroupLift
21variable {X : Type*}
23/--
24A free-group element is relator-equivalent to the word built from a list when its word
25representation reduces to that list.
26-/
27theorem freeGroup_relatorEquivalent_of_toWord_eq_reduce
28 [DecidableEq X]
29 {R : Set (FreeGroup X)} {u : FreeGroup X} {w : List (X × Bool)}
30 (h : u.toWord = FreeGroup.reduce w) :
31 RelatorEquivalent R u (FreeGroup.mk w) := by
32 apply RelatorEquivalent.of_eq
33 rw [← FreeGroup.toWord_inj]
34 simp only [h, FreeGroup.toWord_mk]
36/--
37A free-group word is relator-equivalent to the word built from a list when their reduced words
38agree.
39-/
40theorem freeGroup_relatorEquivalent_mk_of_reduce_eq
41 [DecidableEq X]
42 {R : Set (FreeGroup X)} {u : FreeGroup X} {w : List (X × Bool)}
43 (h : FreeGroup.reduce w = u.toWord) :
44 RelatorEquivalent R (FreeGroup.mk w) u :=
45 (freeGroup_relatorEquivalent_of_toWord_eq_reduce
46 (R := R) (u := u) (w := w) h.symm).symm
48/-- Expand each signed source letter to the reduced word of its image, reversing and inverting negative letters. -/
49def freeGroupSubstitutionWord {Y : Type*} [DecidableEq Y]
50 (f : X → FreeGroup Y) :
51 List (X × Bool) → List (Y × Bool)
52 | [] => []
53 | (x, true) :: xs => (f x).toWord ++ freeGroupSubstitutionWord f xs
54 | (x, false) :: xs => FreeGroup.invRev (f x).toWord ++ freeGroupSubstitutionWord f xs
56/-- Substitution sends the empty word to the empty word. -/
57@[simp]
58theorem freeGroupSubstitutionWord_nil {Y : Type*} [DecidableEq Y]
59 (f : X → FreeGroup Y) :
60 freeGroupSubstitutionWord f [] = [] :=
61 rfl
63/-- Substitution of a positive letter prepends the reduced word of its image. -/
64@[simp]
65theorem freeGroupSubstitutionWord_cons_true {Y : Type*} [DecidableEq Y]
66 (f : X → FreeGroup Y) (x : X) (xs : List (X × Bool)) :
67 freeGroupSubstitutionWord f ((x, true) :: xs) =
68 (f x).toWord ++ freeGroupSubstitutionWord f xs :=
69 rfl
71/-- Substitution of a negative letter prepends the inverse-reversal of its image word. -/
72@[simp]
73theorem freeGroupSubstitutionWord_cons_false {Y : Type*} [DecidableEq Y]
74 (f : X → FreeGroup Y) (x : X) (xs : List (X × Bool)) :
75 freeGroupSubstitutionWord f ((x, false) :: xs) =
76 FreeGroup.invRev (f x).toWord ++ freeGroupSubstitutionWord f xs :=
77 rfl
79/-- Substitution preserves concatenation of signed words. -/
80theorem freeGroupSubstitutionWord_append {Y : Type*} [DecidableEq Y]
81 (f : X → FreeGroup Y) (xs ys : List (X × Bool)) :
82 freeGroupSubstitutionWord f (xs ++ ys) =
83 freeGroupSubstitutionWord f xs ++ freeGroupSubstitutionWord f ys := by
84 induction xs with
85 | nil => simp
86 | cons xb xs ih =>
87 rcases xb with ⟨x, b⟩
88 cases b
89 · simp only [List.cons_append, freeGroupSubstitutionWord_cons_false, ih, List.append_assoc]
90 · simp only [List.cons_append, freeGroupSubstitutionWord_cons_true, ih, List.append_assoc]
92/-- Evaluating a substitution word agrees with applying the free-group lift. -/
93theorem freeGroup_mk_substitutionWord {Y : Type*} [DecidableEq Y]
94 (f : X → FreeGroup Y) (xs : List (X × Bool)) :
95 FreeGroup.mk (freeGroupSubstitutionWord f xs) =
96 FreeGroup.lift f (FreeGroup.mk xs) := by
97 induction xs with
98 | nil => exact FreeGroup.one_eq_mk.symm
99 | cons xb xs ih =>
100 rcases xb with ⟨x, b⟩
101 cases b
102 · rw [freeGroupSubstitutionWord_cons_false, ← FreeGroup.mul_mk,
103 ← FreeGroup.inv_mk, FreeGroup.mk_toWord, ih]
104 simp only [FreeGroup.lift_mk, List.map_cons, cond_false, List.prod_cons]
105 · rw [freeGroupSubstitutionWord_cons_true, ← FreeGroup.mul_mk,
106 FreeGroup.mk_toWord, ih]
107 simp only [FreeGroup.lift_mk, List.map_cons, cond_true, List.prod_cons]
109/-- The lifted generator maps to the corresponding word in the free-group presentation. -/
110theorem freeGroup_toWord_lift_mk {Y : Type*} [DecidableEq Y]
111 (f : X → FreeGroup Y) (xs : List (X × Bool)) :
112 (FreeGroup.lift f (FreeGroup.mk xs)).toWord =
113 FreeGroup.reduce (freeGroupSubstitutionWord f xs) := by
114 rw [← freeGroup_mk_substitutionWord (f := f) (xs := xs)]
115 simp only [FreeGroup.toWord_mk]
117/-- The free-group lift of a reduced substitution word agrees with the corresponding generator. -/
118theorem freeGroup_lift_mk_eq_mk_of_substitutionWord_reduce_eq
119 {Y : Type*} [DecidableEq Y]
120 {f : X → FreeGroup Y} {xs : List (X × Bool)}
121 {ys : List (Y × Bool)}
122 (h :
123 FreeGroup.reduce (freeGroupSubstitutionWord f xs) =
124 FreeGroup.reduce ys) :
125 FreeGroup.lift f (FreeGroup.mk xs) = FreeGroup.mk ys := by
126 rw [← FreeGroup.toWord_inj]
127 rw [freeGroup_toWord_lift_mk, FreeGroup.toWord_mk, h]
129/--
130A lifted generator word is relator-equivalent to the corresponding word when the substitution
131word has the stated reduction.
132-/
133theorem freeGroup_relatorEquivalent_lift_mk_of_substitutionWord_reduce_eq
134 {Y : Type*} [DecidableEq Y]
135 {R : Set (FreeGroup Y)}
136 {f : X → FreeGroup Y} {xs : List (X × Bool)}
137 {ys : List (Y × Bool)}
138 (h :
139 FreeGroup.reduce (freeGroupSubstitutionWord f xs) =
140 FreeGroup.reduce ys) :
141 RelatorEquivalent R (FreeGroup.lift f (FreeGroup.mk xs))
142 (FreeGroup.mk ys) :=
143 RelatorEquivalent.of_eq
144 (freeGroup_lift_mk_eq_mk_of_substitutionWord_reduce_eq h)
146/--
147A lifted generator word is relator-equivalent to the identity when its substitution word reduces
148to the empty word.
149-/
150theorem freeGroup_relatorEquivalent_lift_mk_one_of_substitutionWord_reduce_eq
151 {Y : Type*} [DecidableEq Y]
152 {R : Set (FreeGroup Y)}
153 {f : X → FreeGroup Y} {xs : List (X × Bool)}
154 {ys : List (Y × Bool)}
155 (h :
156 FreeGroup.reduce (freeGroupSubstitutionWord f xs) =
157 FreeGroup.reduce ys)
158 (hy : RelatorEquivalent R (FreeGroup.mk ys) 1) :
159 RelatorEquivalent R (FreeGroup.lift f (FreeGroup.mk xs)) 1 :=
160 (freeGroup_relatorEquivalent_lift_mk_of_substitutionWord_reduce_eq
161 (R := R) h).trans hy
163/--
164A free-group lift preserves relator equivalence when the generator images are
165relator-equivalent.
166-/
167theorem freeGroup_lift_relatorEquivalent_of_generator_relatorEquivalent
168 {R : Set G} {f g : X → G}
169 (h : ∀ x : X, RelatorEquivalent R (f x) (g x))
170 (w : FreeGroup X) :
171 RelatorEquivalent R (FreeGroup.lift f w) (FreeGroup.lift g w) := by
172 let N : Subgroup G := Subgroup.normalClosure R
173 let F : FreeGroup X →* G ⧸ N :=
174 (QuotientGroup.mk' N).comp (FreeGroup.lift f)
175 let K : FreeGroup X →* G ⧸ N :=
176 (QuotientGroup.mk' N).comp (FreeGroup.lift g)
177 have hhom : F = K := by
178 ext x
179 dsimp [F, K]
180 simp only [FreeGroup.lift_apply_of]
181 rw [← relatorEquivalent_iff_eq_in_presentedQuotient]
182 exact h x
183 have hw := congrArg (fun φ : FreeGroup X →* G ⧸ N => φ w) hhom
184 change ((FreeGroup.lift f w : G) : G ⧸ N) =
185 ((FreeGroup.lift g w : G) : G ⧸ N) at hw
186 exact relatorEquivalent_iff_eq_in_presentedQuotient.2 hw
188/--
189A free-group lift sends the word to a relator-equivalent trivial word when the generator images
190are relator-equivalent to one.
191-/
192theorem freeGroup_lift_relatorEquivalent_one_of_generator_relatorEquivalent
193 {R : Set G} {f : X → G}
194 (h : ∀ x : X, RelatorEquivalent R (f x) 1)
195 (w : FreeGroup X) :
196 RelatorEquivalent R (FreeGroup.lift f w) 1 := by
197 let trivialLift : FreeGroup X →* G :=
198 FreeGroup.lift (fun _ : X => (1 : G))
199 have htrivial : trivialLift w = 1 := by
200 have hhom : trivialLift = 1 := by
201 ext x
202 simp only [FreeGroup.lift_apply_of, MonoidHom.one_apply, trivialLift]
203 exact congrArg (fun φ : FreeGroup X →* G => φ w) hhom
204 simpa [trivialLift, htrivial] using
205 freeGroup_lift_relatorEquivalent_of_generator_relatorEquivalent
206 (R := R) (f := f) (g := fun _ : X => (1 : G)) h w
208/-- A free-group lift preserves relator equivalence when the generator images are equal. -/
209theorem freeGroup_lift_relatorEquivalent_of_generator_eq
210 {R : Set G} {f g : X → G}
211 (h : ∀ x : X, f x = g x)
212 (w : FreeGroup X) :
213 RelatorEquivalent R (FreeGroup.lift f w) (FreeGroup.lift g w) :=
214 freeGroup_lift_relatorEquivalent_of_generator_relatorEquivalent
215 (R := R) (f := f) (g := g)
216 (fun x => RelatorEquivalent.of_eq (h x)) w
218end FreeGroupLift
220end NormalClosure
222end ReidemeisterSchreier.Discrete.Presentations