Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorReplacement
1import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.Core
3/-!
4# Reidemeister Schreier / Discrete / Presentations / Tietze / Relator Replacement
6This module supplies semantic presented-group equivalences for replacing
7relators: equal normal closures, mutual relator maps, generator maps, and
8compositions of these transformations.
9-/
11universe u v w
13namespace ReidemeisterSchreier.Discrete.Presentations
15namespace Presented
17variable {X Y : Type*}
19/-- The identity equivalence of a presented group. -/
20noncomputable def refl (R : Set (FreeGroup X)) :
21 PresentedGroup R ≃* PresentedGroup R :=
22 MulEquiv.refl (PresentedGroup R)
24/-- Reverse an equivalence between two presented groups. -/
25noncomputable def symm
26 {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
27 (e : PresentedGroup R ≃* PresentedGroup S) :
28 PresentedGroup S ≃* PresentedGroup R :=
29 e.symm
31/-- Compose equivalences of presented groups through an intermediate presentation. -/
32noncomputable def trans
33 {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)} {Z : Type*}
34 {T : Set (FreeGroup Z)}
35 (e₁ : PresentedGroup R ≃* PresentedGroup S)
36 (e₂ : PresentedGroup S ≃* PresentedGroup T) :
37 PresentedGroup R ≃* PresentedGroup T :=
38 e₁.trans e₂
40/-- Mutual relator-quotient map data induces an equivalence between the two presented groups. -/
41noncomputable def ofMutualMapData
42 (R : Set (FreeGroup X)) (S : Set (FreeGroup Y))
43 (D : RelatorQuotientMutualMapData R S) :
44 PresentedGroup R ≃* PresentedGroup S :=
45 quotientEquivOfRelatorQuotientMutualMapData R S D
47/-- A Tietze equivalence induces an isomorphism between the corresponding presented groups. -/
48noncomputable def ofTietzeEquiv
49 {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
50 (D : TietzeEquiv R S) :
51 PresentedGroup R ≃* PresentedGroup S :=
52 D.presentedEquiv
54/--
55Equal normal closures give a Tietze equivalence between presentations with the same generators.
56-/
57noncomputable def ofNormalClosureEq
58 {R S : Set (FreeGroup X)}
59 (h : Subgroup.normalClosure R = Subgroup.normalClosure S) :
60 PresentedGroup R ≃* PresentedGroup S :=
61 QuotientGroup.congr
62 (Subgroup.normalClosure R)
63 (Subgroup.normalClosure S)
64 (MulEquiv.refl (FreeGroup X))
65 (by simpa using h)
67/--
68Compatible generator maps in both directions induce an equivalence between the two presented
69groups.
70-/
71noncomputable def ofGeneratorMaps
72 {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
73 (toGenerator : X → FreeGroup Y)
74 (invGenerator : Y → FreeGroup X)
75 (hR :
76 ∀ r ∈ R,
77 FreeGroup.lift toGenerator r ∈ Subgroup.normalClosure S)
78 (hS :
79 ∀ s ∈ S,
80 FreeGroup.lift invGenerator s ∈ Subgroup.normalClosure R)
81 (hinv_to :
82 ∀ x : X,
83 RelatorEquivalent R
84 (FreeGroup.lift invGenerator (toGenerator x))
85 (FreeGroup.of x))
86 (hto_inv :
87 ∀ y : Y,
88 RelatorEquivalent S
89 (FreeGroup.lift toGenerator (invGenerator y))
90 (FreeGroup.of y)) :
91 PresentedGroup R ≃* PresentedGroup S :=
92 (TietzeEquiv.ofGeneratorMaps
93 toGenerator invGenerator hR hS hinv_to hto_inv).presentedEquiv
95/--
96Generator maps that preserve relators up to relator equivalence induce the corresponding
97presented-group map.
98-/
99noncomputable def ofGeneratorMapsRelatorEquivalent
100 {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
101 (toGenerator : X → FreeGroup Y)
102 (invGenerator : Y → FreeGroup X)
103 (hR :
104 ∀ r ∈ R,
105 RelatorEquivalent S (FreeGroup.lift toGenerator r) 1)
106 (hS :
107 ∀ s ∈ S,
108 RelatorEquivalent R (FreeGroup.lift invGenerator s) 1)
109 (hinv_to :
110 ∀ x : X,
111 RelatorEquivalent R
112 (FreeGroup.lift invGenerator (toGenerator x))
113 (FreeGroup.of x))
114 (hto_inv :
115 ∀ y : Y,
116 RelatorEquivalent S
117 (FreeGroup.lift toGenerator (invGenerator y))
118 (FreeGroup.of y)) :
119 PresentedGroup R ≃* PresentedGroup S :=
120 (TietzeEquiv.ofGeneratorMapsRelatorEquivalent
121 toGenerator invGenerator hR hS hinv_to hto_inv).presentedEquiv
123/-- Replace a family of relators by equivalent relators in a presented group. -/
124noncomputable def replaceRelators
125 {R S : Set (FreeGroup X)}
126 (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
127 (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
128 PresentedGroup R ≃* PresentedGroup S :=
129 ofNormalClosureEq (normalClosure_eq_of_relatorEquivalent hR_to_S hS_to_R)
131/--
132Replacing the relator set by another set with the same normal closure is a Tietze equivalence.
133-/
134def replaceRelatorsTietzeEquiv
135 {R S : Set (FreeGroup X)}
136 (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
137 (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
138 TietzeEquiv R S :=
139 TietzeEquiv.ofRelatorEquivalent hR_to_S hS_to_R
141/-- Replace one relator by an equivalent relator in a presented group. -/
142noncomputable def replaceRelator
143 {R : Set (FreeGroup X)} {oldRelator newRelator : FreeGroup X}
144 (holdRelator :
145 RelatorEquivalent (insert newRelator (R \ {oldRelator})) oldRelator 1)
146 (hnewRelator : RelatorEquivalent R newRelator 1) :
147 PresentedGroup R ≃*
148 PresentedGroup (insert newRelator (R \ {oldRelator})) :=
149 replaceRelators
150 (S := insert newRelator (R \ {oldRelator}))
151 (by
152 intro r hr
153 by_cases hrold : r = oldRelator
154 · simpa [hrold] using holdRelator
155 · exact RelatorEquivalent.of_mem
156 (R := insert newRelator (R \ {oldRelator}))
157 (Or.inr ⟨hr, by simpa [Set.mem_singleton_iff] using hrold⟩))
158 (by
159 intro s hs
160 rcases hs with rfl | hs
161 · exact hnewRelator
162 · exact RelatorEquivalent.of_mem (R := R) hs.1)
164/-- Replacing one relator by another without changing the normal closure is a Tietze equivalence. -/
165def replaceRelatorTietzeEquiv
166 {R : Set (FreeGroup X)} {oldRelator newRelator : FreeGroup X}
167 (holdRelator :
168 RelatorEquivalent (insert newRelator (R \ {oldRelator})) oldRelator 1)
169 (hnewRelator : RelatorEquivalent R newRelator 1) :
170 TietzeEquiv R (insert newRelator (R \ {oldRelator})) :=
171 replaceRelatorsTietzeEquiv
172 (S := insert newRelator (R \ {oldRelator}))
173 (by
174 intro r hr
175 by_cases hrold : r = oldRelator
176 · simpa [hrold] using holdRelator
177 · exact RelatorEquivalent.of_mem
178 (R := insert newRelator (R \ {oldRelator}))
179 (Or.inr ⟨hr, by simpa [Set.mem_singleton_iff] using hrold⟩))
180 (by
181 intro s hs
182 rcases hs with rfl | hs
183 · exact hnewRelator
184 · exact RelatorEquivalent.of_mem (R := R) hs.1)
186/-- Adjoining relators already contained in the original normal closure does not change it. -/
187theorem normalClosure_union_eq_left_of_subset
188 {R S : Set (FreeGroup X)}
189 (hS : S ⊆ Subgroup.normalClosure R) :
190 Subgroup.normalClosure (R ∪ S) = Subgroup.normalClosure R := by
191 apply normalClosure_eq_of_subset_normalClosure
192 · intro x hx
193 rcases hx with hx | hx
194 · exact Subgroup.subset_normalClosure hx
195 · exact hS hx
196 · intro x hx
197 exact Subgroup.subset_normalClosure (Or.inl hx)
199/--
200Removing relators already contained in the normal closure of the remaining relators does not
201change that normal closure.
202-/
203theorem normalClosure_sdiff_eq_of_subset
204 {R D : Set (FreeGroup X)}
205 (hD : ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure (R \ D)) :
206 Subgroup.normalClosure R = Subgroup.normalClosure (R \ D) := by
207 apply normalClosure_eq_of_subset_normalClosure
208 · intro r hr
209 by_cases hd : r ∈ D
210 · exact hD r hd hr
211 · exact Subgroup.subset_normalClosure ⟨hr, hd⟩
212 · intro r hr
213 exact Subgroup.subset_normalClosure hr.1
215/--
216Adding a family of redundant relators to a presented group does not change the presented group.
217-/
218noncomputable def addRedundantRelators
219 {R S : Set (FreeGroup X)}
220 (hS : S ⊆ Subgroup.normalClosure R) :
221 PresentedGroup (R ∪ S) ≃* PresentedGroup R :=
222 ofNormalClosureEq (normalClosure_union_eq_left_of_subset hS)
224/-- Adding redundant relators preserves relator equivalence in the presented group. -/
225noncomputable def addRedundantRelatorsRelatorEquivalent
226 {R S : Set (FreeGroup X)}
227 (hS : ∀ s ∈ S, RelatorEquivalent R s 1) :
228 PresentedGroup (R ∪ S) ≃* PresentedGroup R :=
229 addRedundantRelators
230 (R := R) (S := S)
231 (fun s hs => RelatorEquivalent.mem_normalClosure_of_eq_one (hS s hs))
233/-- Adding a set of relators already in the normal closure is a Tietze equivalence. -/
234def addRedundantRelatorsTietzeEquiv
235 {R S : Set (FreeGroup X)}
236 (hS : S ⊆ Subgroup.normalClosure R) :
237 TietzeEquiv (R ∪ S) R :=
238 TietzeEquiv.ofNormalClosureEq
239 (normalClosure_union_eq_left_of_subset hS)
241/-- Adding redundant relators gives a Tietze equivalence of presentations. -/
242def addRedundantRelatorsRelatorEquivalentTietzeEquiv
243 {R S : Set (FreeGroup X)}
244 (hS : ∀ s ∈ S, RelatorEquivalent R s 1) :
245 TietzeEquiv (R ∪ S) R :=
246 addRedundantRelatorsTietzeEquiv
247 (R := R) (S := S)
248 (fun s hs => RelatorEquivalent.mem_normalClosure_of_eq_one (hS s hs))
250/-- Remove a previously added family of redundant relators from a presented group. -/
251noncomputable def addRedundantRelatorsInverse
252 {R S : Set (FreeGroup X)}
253 (hS : S ⊆ Subgroup.normalClosure R) :
254 PresentedGroup R ≃* PresentedGroup (R ∪ S) :=
255 (addRedundantRelators (R := R) (S := S) hS).symm
257/-- The inverse direction after adding redundant relators preserves relator equivalence. -/
258noncomputable def addRedundantRelatorsRelatorEquivalentInverse
259 {R S : Set (FreeGroup X)}
260 (hS : ∀ s ∈ S, RelatorEquivalent R s 1) :
261 PresentedGroup R ≃* PresentedGroup (R ∪ S) :=
262 (addRedundantRelatorsRelatorEquivalent (R := R) (S := S) hS).symm
264/-- Remove a subset of relators already generated by the remaining relators. -/
265noncomputable def removeRelatorSubset
266 {R D : Set (FreeGroup X)}
267 (hD : ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure (R \ D)) :
268 PresentedGroup R ≃* PresentedGroup (R \ D) :=
269 ofNormalClosureEq (normalClosure_sdiff_eq_of_subset hD)
271/--
272Removing a relator subset preserves relator equivalence under the stated normal-closure
273hypothesis.
274-/
275noncomputable def removeRelatorSubsetRelatorEquivalent
276 {R D : Set (FreeGroup X)}
277 (hD : ∀ d ∈ D, d ∈ R → RelatorEquivalent (R \ D) d 1) :
278 PresentedGroup R ≃* PresentedGroup (R \ D) :=
279 removeRelatorSubset
280 (R := R) (D := D)
281 (fun d hd hR =>
282 RelatorEquivalent.mem_normalClosure_of_eq_one (hD d hd hR))
284/--
285Removing a subset of redundant relators is a Tietze equivalence when the normal closure is
286unchanged.
287-/
288def removeRelatorSubsetTietzeEquiv
289 {R D : Set (FreeGroup X)}
290 (hD : ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure (R \ D)) :
291 TietzeEquiv R (R \ D) :=
292 TietzeEquiv.ofNormalClosureEq
293 (normalClosure_sdiff_eq_of_subset hD)
295/-- Removing a redundant relator subset gives a Tietze equivalence of presentations. -/
296def removeRelatorSubsetRelatorEquivalentTietzeEquiv
297 {R D : Set (FreeGroup X)}
298 (hD : ∀ d ∈ D, d ∈ R → RelatorEquivalent (R \ D) d 1) :
299 TietzeEquiv R (R \ D) :=
300 removeRelatorSubsetTietzeEquiv
301 (R := R) (D := D)
302 (fun d hd hR =>
303 RelatorEquivalent.mem_normalClosure_of_eq_one (hD d hd hR))
305/-- Add back a relator subset previously removed as redundant. -/
306noncomputable def removeRelatorSubsetInverse
307 {R D : Set (FreeGroup X)}
308 (hD : ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure (R \ D)) :
309 PresentedGroup (R \ D) ≃* PresentedGroup R :=
310 (removeRelatorSubset (R := R) (D := D) hD).symm
312/-- The inverse direction after removing a relator subset preserves relator equivalence. -/
313noncomputable def removeRelatorSubsetRelatorEquivalentInverse
314 {R D : Set (FreeGroup X)}
315 (hD : ∀ d ∈ D, d ∈ R → RelatorEquivalent (R \ D) d 1) :
316 PresentedGroup (R \ D) ≃* PresentedGroup R :=
317 (removeRelatorSubsetRelatorEquivalent (R := R) (D := D) hD).symm
319/--
320Replace a whole subfamily \(D\) of relators by a new family \(E\). Relators outside \(D\) are
321kept unchanged.
322-/
323noncomputable def replaceRelatorSubset
324 {R D E : Set (FreeGroup X)}
325 (hD :
326 ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure ((R \ D) ∪ E))
327 (hE : E ⊆ Subgroup.normalClosure R) :
328 PresentedGroup R ≃* PresentedGroup ((R \ D) ∪ E) :=
329 replaceRelators
330 (S := (R \ D) ∪ E)
331 (by
332 intro r hr
333 by_cases hd : r ∈ D
334 · exact RelatorEquivalent.of_mem_normalClosure (hD r hd hr)
335 · exact RelatorEquivalent.of_mem (R := (R \ D) ∪ E)
336 (Or.inl ⟨hr, hd⟩))
337 (by
338 intro s hs
339 rcases hs with hs | hs
340 · exact RelatorEquivalent.of_mem (R := R) hs.1
341 · exact RelatorEquivalent.of_mem_normalClosure (hE hs))
343/-- Replacing a relator subset by relator-equivalent relators preserves relator equivalence. -/
344noncomputable def replaceRelatorSubsetRelatorEquivalent
345 {R D E : Set (FreeGroup X)}
346 (hD :
347 ∀ d ∈ D, d ∈ R → RelatorEquivalent ((R \ D) ∪ E) d 1)
348 (hE : ∀ e ∈ E, RelatorEquivalent R e 1) :
349 PresentedGroup R ≃* PresentedGroup ((R \ D) ∪ E) :=
350 replaceRelatorSubset
351 (R := R) (D := D) (E := E)
352 (fun d hd hR =>
353 RelatorEquivalent.mem_normalClosure_of_eq_one (hD d hd hR))
354 (fun e he => RelatorEquivalent.mem_normalClosure_of_eq_one (hE e he))
356/--
357Replacing a subset of relators by another subset with the same normal closure is a Tietze
358equivalence.
359-/
360def replaceRelatorSubsetTietzeEquiv
361 {R D E : Set (FreeGroup X)}
362 (hD :
363 ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure ((R \ D) ∪ E))
364 (hE : E ⊆ Subgroup.normalClosure R) :
365 TietzeEquiv R ((R \ D) ∪ E) :=
366 replaceRelatorsTietzeEquiv
367 (S := (R \ D) ∪ E)
368 (by
369 intro r hr
370 by_cases hd : r ∈ D
371 · exact RelatorEquivalent.of_mem_normalClosure (hD r hd hr)
372 · exact RelatorEquivalent.of_mem (R := (R \ D) ∪ E)
373 (Or.inl ⟨hr, hd⟩))
374 (by
375 intro s hs
376 rcases hs with hs | hs
377 · exact RelatorEquivalent.of_mem (R := R) hs.1
378 · exact RelatorEquivalent.of_mem_normalClosure (hE hs))
380/-- Replacing a relator subset by relator-equivalent relators gives a Tietze equivalence. -/
381def replaceRelatorSubsetRelatorEquivalentTietzeEquiv
382 {R D E : Set (FreeGroup X)}
383 (hD :
384 ∀ d ∈ D, d ∈ R → RelatorEquivalent ((R \ D) ∪ E) d 1)
385 (hE : ∀ e ∈ E, RelatorEquivalent R e 1) :
386 TietzeEquiv R ((R \ D) ∪ E) :=
387 replaceRelatorSubsetTietzeEquiv
388 (R := R) (D := D) (E := E)
389 (fun d hd hR =>
390 RelatorEquivalent.mem_normalClosure_of_eq_one (hD d hd hR))
391 (fun e he => RelatorEquivalent.mem_normalClosure_of_eq_one (hE e he))
393/-- Adding one redundant relator to a presented group does not change the presented group. -/
394noncomputable def addRedundantRelator
395 {R : Set (FreeGroup X)} {r : FreeGroup X}
396 (hr : r ∈ Subgroup.normalClosure R) :
397 PresentedGroup (insert r R) ≃* PresentedGroup R :=
398 ofNormalClosureEq (normalClosure_insert_eq_of_mem (R := R) hr)
400/-- Adding one relator already in the normal closure is a Tietze equivalence. -/
401def addRedundantRelatorTietzeEquiv
402 {R : Set (FreeGroup X)} {r : FreeGroup X}
403 (hr : r ∈ Subgroup.normalClosure R) :
404 TietzeEquiv (insert r R) R :=
405 TietzeEquiv.ofNormalClosureEq
406 (normalClosure_insert_eq_of_mem (R := R) hr)
408/-- Remove one redundant relator from a presented group without changing the presented group. -/
409noncomputable def removeRedundantRelator
410 {R : Set (FreeGroup X)} {r : FreeGroup X}
411 (hr : r ∈ Subgroup.normalClosure (R \ {r})) :
412 PresentedGroup R ≃* PresentedGroup (R \ {r}) :=
413 ofNormalClosureEq (normalClosure_diff_singleton_eq_of_mem (R := R) hr)
415/--
416Removing one relator whose normal closure is generated by the remaining relators is a Tietze
417equivalence.
418-/
419def removeRedundantRelatorTietzeEquiv
420 {R : Set (FreeGroup X)} {r : FreeGroup X}
421 (hr : r ∈ Subgroup.normalClosure (R \ {r})) :
422 TietzeEquiv R (R \ {r}) :=
423 TietzeEquiv.ofNormalClosureEq
424 (normalClosure_diff_singleton_eq_of_mem (R := R) hr)
426/-- Rename the generators of a presented group. -/
427noncomputable def renameGenerators
428 (R : Set (FreeGroup X)) (e : X ≃ Y) :
429 PresentedGroup R ≃*
430 PresentedGroup (FreeGroup.freeGroupCongr e '' R) :=
431 PresentedGroup.equivPresentedGroup R e
433/-- Renaming generators along an equivalence gives a Tietze equivalence. -/
434def renameGeneratorsTietzeEquiv
435 (R : Set (FreeGroup X)) (e : X ≃ Y) :
436 TietzeEquiv R (FreeGroup.freeGroupCongr e '' R) :=
437 TietzeEquiv.ofMutualMapData
438 (relatorQuotientMutualMapDataOfRelatorImagesMemNormalClosure
439 (FreeGroup.freeGroupCongr e)
440 R (FreeGroup.freeGroupCongr e '' R)
441 (by
442 intro r hr
443 exact Subgroup.subset_normalClosure ⟨r, hr, rfl⟩)
444 (by
445 intro s hs
446 rcases hs with ⟨r, hr, rfl⟩
447 have hback :
448 (FreeGroup.freeGroupCongr e).symm
449 ((FreeGroup.freeGroupCongr e) r) = r :=
450 (FreeGroup.freeGroupCongr e).left_inv r
451 rw [hback]
452 exact Subgroup.subset_normalClosure hr))
454end Presented
456end ReidemeisterSchreier.Discrete.Presentations