ReidemeisterSchreier/Discrete/Presentations/Tietze/RelatorReplacement.lean
1import ReidemeisterSchreier.Discrete.Presentations.Tietze.Core
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ReidemeisterSchreier/Discrete/Presentations/Tietze/RelatorReplacement.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Tietze transformations
14Presentation-level Tietze moves for adding and deleting generators, replacing relators, comparing quotient presentations, and recording executable Tietze scripts.
15-/
17universe u v w
19namespace ReidemeisterSchreier.Discrete.Presentations
21namespace Presented
23variable {X Y : Type*}
25noncomputable def refl (R : Set (FreeGroup X)) :
26 PresentedGroup R ≃* PresentedGroup R :=
27 MulEquiv.refl (PresentedGroup R)
29noncomputable def symm
30 {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
31 (e : PresentedGroup R ≃* PresentedGroup S) :
32 PresentedGroup S ≃* PresentedGroup R :=
33 e.symm
35noncomputable def trans
36 {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)} {Z : Type*}
37 {T : Set (FreeGroup Z)}
38 (e₁ : PresentedGroup R ≃* PresentedGroup S)
39 (e₂ : PresentedGroup S ≃* PresentedGroup T) :
40 PresentedGroup R ≃* PresentedGroup T :=
41 e₁.trans e₂
43noncomputable def ofMutualMapData
44 (R : Set (FreeGroup X)) (S : Set (FreeGroup Y))
45 (D : RelatorQuotientMutualMapData R S) :
46 PresentedGroup R ≃* PresentedGroup S :=
49noncomputable def ofTietzeEquiv
50 {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
51 (D : TietzeEquiv R S) :
52 PresentedGroup R ≃* PresentedGroup S :=
53 D.presentedEquiv
55noncomputable def ofNormalClosureEq
56 {R S : Set (FreeGroup X)}
57 (h : Subgroup.normalClosure R = Subgroup.normalClosure S) :
58 PresentedGroup R ≃* PresentedGroup S :=
59 QuotientGroup.congr
60 (Subgroup.normalClosure R)
61 (Subgroup.normalClosure S)
62 (MulEquiv.refl (FreeGroup X))
63 (by simpa using h)
65noncomputable def ofGeneratorMaps
66 {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
67 (toGenerator : X → FreeGroup Y)
68 (invGenerator : Y → FreeGroup X)
69 (hR :
70 ∀ r ∈ R,
71 FreeGroup.lift toGenerator r ∈ Subgroup.normalClosure S)
72 (hS :
73 ∀ s ∈ S,
74 FreeGroup.lift invGenerator s ∈ Subgroup.normalClosure R)
75 (hinv_to :
76 ∀ x : X,
78 (FreeGroup.lift invGenerator (toGenerator x))
79 (FreeGroup.of x))
80 (hto_inv :
81 ∀ y : Y,
83 (FreeGroup.lift toGenerator (invGenerator y))
84 (FreeGroup.of y)) :
85 PresentedGroup R ≃* PresentedGroup S :=
86 (TietzeEquiv.ofGeneratorMaps
87 toGenerator invGenerator hR hS hinv_to hto_inv).presentedEquiv
89noncomputable def ofGeneratorMapsRelatorEquivalent
90 {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
91 (toGenerator : X → FreeGroup Y)
92 (invGenerator : Y → FreeGroup X)
93 (hR :
94 ∀ r ∈ R,
95 RelatorEquivalent S (FreeGroup.lift toGenerator r) 1)
96 (hS :
97 ∀ s ∈ S,
98 RelatorEquivalent R (FreeGroup.lift invGenerator s) 1)
99 (hinv_to :
100 ∀ x : X,
102 (FreeGroup.lift invGenerator (toGenerator x))
103 (FreeGroup.of x))
104 (hto_inv :
105 ∀ y : Y,
107 (FreeGroup.lift toGenerator (invGenerator y))
108 (FreeGroup.of y)) :
109 PresentedGroup R ≃* PresentedGroup S :=
110 (TietzeEquiv.ofGeneratorMapsRelatorEquivalent
111 toGenerator invGenerator hR hS hinv_to hto_inv).presentedEquiv
113noncomputable def replaceRelators
114 {R S : Set (FreeGroup X)}
115 (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
116 (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
117 PresentedGroup R ≃* PresentedGroup S :=
118 ofNormalClosureEq (normalClosure_eq_of_relatorEquivalent hR_to_S hS_to_R)
121 {R S : Set (FreeGroup X)}
122 (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
123 (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
124 TietzeEquiv R S :=
125 TietzeEquiv.ofRelatorEquivalent hR_to_S hS_to_R
127noncomputable def replaceRelator
128 {R : Set (FreeGroup X)} {oldRelator newRelator : FreeGroup X}
129 (holdRelator :
130 RelatorEquivalent (insert newRelator (R \ {oldRelator})) oldRelator 1)
131 (hnewRelator : RelatorEquivalent R newRelator 1) :
132 PresentedGroup R ≃*
133 PresentedGroup (insert newRelator (R \ {oldRelator})) :=
134 replaceRelators
135 (S := insert newRelator (R \ {oldRelator}))
136 (by
137 intro r hr
138 by_cases hrold : r = oldRelator
139 · simpa [hrold] using holdRelator
140 · exact RelatorEquivalent.of_mem
141 (R := insert newRelator (R \ {oldRelator}))
142 (Or.inr ⟨hr, by simpa [Set.mem_singleton_iff] using hrold⟩))
143 (by
144 intro s hs
145 rcases hs with rfl | hs
146 · exact hnewRelator
147 · exact RelatorEquivalent.of_mem (R := R) hs.1)
150 {R : Set (FreeGroup X)} {oldRelator newRelator : FreeGroup X}
151 (holdRelator :
152 RelatorEquivalent (insert newRelator (R \ {oldRelator})) oldRelator 1)
153 (hnewRelator : RelatorEquivalent R newRelator 1) :
154 TietzeEquiv R (insert newRelator (R \ {oldRelator})) :=
156 (S := insert newRelator (R \ {oldRelator}))
157 (by
158 intro r hr
159 by_cases hrold : r = oldRelator
160 · simpa [hrold] using holdRelator
161 · exact RelatorEquivalent.of_mem
162 (R := insert newRelator (R \ {oldRelator}))
163 (Or.inr ⟨hr, by simpa [Set.mem_singleton_iff] using hrold⟩))
164 (by
165 intro s hs
166 rcases hs with rfl | hs
167 · exact hnewRelator
168 · exact RelatorEquivalent.of_mem (R := R) hs.1)
171 {R S : Set (FreeGroup X)}
172 (hS : S ⊆ Subgroup.normalClosure R) :
173 Subgroup.normalClosure (R ∪ S) = Subgroup.normalClosure R := by
175 · intro x hx
176 rcases hx with hx | hx
177 · exact Subgroup.subset_normalClosure hx
178 · exact hS hx
179 · intro x hx
180 exact Subgroup.subset_normalClosure (Or.inl hx)
183 {R D : Set (FreeGroup X)}
184 (hD : ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure (R \ D)) :
185 Subgroup.normalClosure R = Subgroup.normalClosure (R \ D) := by
187 · intro r hr
188 by_cases hd : r ∈ D
189 · exact hD r hd hr
190 · exact Subgroup.subset_normalClosure ⟨hr, hd⟩
191 · intro r hr
192 exact Subgroup.subset_normalClosure hr.1
194noncomputable def addRedundantRelators
195 {R S : Set (FreeGroup X)}
196 (hS : S ⊆ Subgroup.normalClosure R) :
197 PresentedGroup (R ∪ S) ≃* PresentedGroup R :=
198 ofNormalClosureEq (normalClosure_union_eq_left_of_subset hS)
200noncomputable def addRedundantRelatorsRelatorEquivalent
201 {R S : Set (FreeGroup X)}
202 (hS : ∀ s ∈ S, RelatorEquivalent R s 1) :
203 PresentedGroup (R ∪ S) ≃* PresentedGroup R :=
204 addRedundantRelators
205 (R := R) (S := S)
206 (fun s hs => RelatorEquivalent.mem_normalClosure_of_eq_one (hS s hs))
209 {R S : Set (FreeGroup X)}
210 (hS : S ⊆ Subgroup.normalClosure R) :
211 TietzeEquiv (R ∪ S) R :=
212 TietzeEquiv.ofNormalClosureEq
216 {R S : Set (FreeGroup X)}
217 (hS : ∀ s ∈ S, RelatorEquivalent R s 1) :
218 TietzeEquiv (R ∪ S) R :=
220 (R := R) (S := S)
221 (fun s hs => RelatorEquivalent.mem_normalClosure_of_eq_one (hS s hs))
223noncomputable def addRedundantRelatorsInverse
224 {R S : Set (FreeGroup X)}
225 (hS : S ⊆ Subgroup.normalClosure R) :
226 PresentedGroup R ≃* PresentedGroup (R ∪ S) :=
227 (addRedundantRelators (R := R) (S := S) hS).symm
229noncomputable def addRedundantRelatorsRelatorEquivalentInverse
230 {R S : Set (FreeGroup X)}
231 (hS : ∀ s ∈ S, RelatorEquivalent R s 1) :
232 PresentedGroup R ≃* PresentedGroup (R ∪ S) :=
233 (addRedundantRelatorsRelatorEquivalent (R := R) (S := S) hS).symm
235noncomputable def removeRelatorSubset
236 {R D : Set (FreeGroup X)}
237 (hD : ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure (R \ D)) :
238 PresentedGroup R ≃* PresentedGroup (R \ D) :=
239 ofNormalClosureEq (normalClosure_sdiff_eq_of_subset hD)
241noncomputable def removeRelatorSubsetRelatorEquivalent
242 {R D : Set (FreeGroup X)}
243 (hD : ∀ d ∈ D, d ∈ R → RelatorEquivalent (R \ D) d 1) :
244 PresentedGroup R ≃* PresentedGroup (R \ D) :=
245 removeRelatorSubset
246 (R := R) (D := D)
247 (fun d hd hR =>
248 RelatorEquivalent.mem_normalClosure_of_eq_one (hD d hd hR))
251 {R D : Set (FreeGroup X)}
252 (hD : ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure (R \ D)) :
253 TietzeEquiv R (R \ D) :=
254 TietzeEquiv.ofNormalClosureEq
258 {R D : Set (FreeGroup X)}
259 (hD : ∀ d ∈ D, d ∈ R → RelatorEquivalent (R \ D) d 1) :
260 TietzeEquiv R (R \ D) :=
262 (R := R) (D := D)
263 (fun d hd hR =>
264 RelatorEquivalent.mem_normalClosure_of_eq_one (hD d hd hR))
266noncomputable def removeRelatorSubsetInverse
267 {R D : Set (FreeGroup X)}
268 (hD : ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure (R \ D)) :
269 PresentedGroup (R \ D) ≃* PresentedGroup R :=
270 (removeRelatorSubset (R := R) (D := D) hD).symm
272noncomputable def removeRelatorSubsetRelatorEquivalentInverse
273 {R D : Set (FreeGroup X)}
274 (hD : ∀ d ∈ D, d ∈ R → RelatorEquivalent (R \ D) d 1) :
275 PresentedGroup (R \ D) ≃* PresentedGroup R :=
276 (removeRelatorSubsetRelatorEquivalent (R := R) (D := D) hD).symm
278/-- Replace a whole subfamily `D` of relators by a new family `E`. Relators
279outside `D` are kept unchanged. -/
280noncomputable def replaceRelatorSubset
281 {R D E : Set (FreeGroup X)}
282 (hD :
283 ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure ((R \ D) ∪ E))
284 (hE : E ⊆ Subgroup.normalClosure R) :
285 PresentedGroup R ≃* PresentedGroup ((R \ D) ∪ E) :=
286 replaceRelators
287 (S := (R \ D) ∪ E)
288 (by
289 intro r hr
290 by_cases hd : r ∈ D
291 · exact RelatorEquivalent.of_mem_normalClosure (hD r hd hr)
292 · exact RelatorEquivalent.of_mem (R := (R \ D) ∪ E)
293 (Or.inl ⟨hr, hd⟩))
294 (by
295 intro s hs
296 rcases hs with hs | hs
297 · exact RelatorEquivalent.of_mem (R := R) hs.1
298 · exact RelatorEquivalent.of_mem_normalClosure (hE hs))
300noncomputable def replaceRelatorSubsetRelatorEquivalent
301 {R D E : Set (FreeGroup X)}
302 (hD :
303 ∀ d ∈ D, d ∈ R → RelatorEquivalent ((R \ D) ∪ E) d 1)
304 (hE : ∀ e ∈ E, RelatorEquivalent R e 1) :
305 PresentedGroup R ≃* PresentedGroup ((R \ D) ∪ E) :=
306 replaceRelatorSubset
307 (R := R) (D := D) (E := E)
308 (fun d hd hR =>
309 RelatorEquivalent.mem_normalClosure_of_eq_one (hD d hd hR))
310 (fun e he => RelatorEquivalent.mem_normalClosure_of_eq_one (hE e he))
313 {R D E : Set (FreeGroup X)}
314 (hD :
315 ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure ((R \ D) ∪ E))
316 (hE : E ⊆ Subgroup.normalClosure R) :
317 TietzeEquiv R ((R \ D) ∪ E) :=
319 (S := (R \ D) ∪ E)
320 (by
321 intro r hr
322 by_cases hd : r ∈ D
323 · exact RelatorEquivalent.of_mem_normalClosure (hD r hd hr)
324 · exact RelatorEquivalent.of_mem (R := (R \ D) ∪ E)
325 (Or.inl ⟨hr, hd⟩))
326 (by
327 intro s hs
328 rcases hs with hs | hs
329 · exact RelatorEquivalent.of_mem (R := R) hs.1
330 · exact RelatorEquivalent.of_mem_normalClosure (hE hs))
333 {R D E : Set (FreeGroup X)}
334 (hD :
335 ∀ d ∈ D, d ∈ R → RelatorEquivalent ((R \ D) ∪ E) d 1)
336 (hE : ∀ e ∈ E, RelatorEquivalent R e 1) :
337 TietzeEquiv R ((R \ D) ∪ E) :=
339 (R := R) (D := D) (E := E)
340 (fun d hd hR =>
341 RelatorEquivalent.mem_normalClosure_of_eq_one (hD d hd hR))
342 (fun e he => RelatorEquivalent.mem_normalClosure_of_eq_one (hE e he))
344noncomputable def addRedundantRelator
345 {R : Set (FreeGroup X)} {r : FreeGroup X}
346 (hr : r ∈ Subgroup.normalClosure R) :
347 PresentedGroup (insert r R) ≃* PresentedGroup R :=
348 ofNormalClosureEq (normalClosure_insert_eq_of_mem (R := R) hr)
351 {R : Set (FreeGroup X)} {r : FreeGroup X}
352 (hr : r ∈ Subgroup.normalClosure R) :
353 TietzeEquiv (insert r R) R :=
354 TietzeEquiv.ofNormalClosureEq
355 (normalClosure_insert_eq_of_mem (R := R) hr)
357noncomputable def removeRedundantRelator
358 {R : Set (FreeGroup X)} {r : FreeGroup X}
359 (hr : r ∈ Subgroup.normalClosure (R \ {r})) :
360 PresentedGroup R ≃* PresentedGroup (R \ {r}) :=
361 ofNormalClosureEq (normalClosure_diff_singleton_eq_of_mem (R := R) hr)
364 {R : Set (FreeGroup X)} {r : FreeGroup X}
365 (hr : r ∈ Subgroup.normalClosure (R \ {r})) :
366 TietzeEquiv R (R \ {r}) :=
367 TietzeEquiv.ofNormalClosureEq
368 (normalClosure_diff_singleton_eq_of_mem (R := R) hr)
370noncomputable def renameGenerators
371 (R : Set (FreeGroup X)) (e : X ≃ Y) :
372 PresentedGroup R ≃*
373 PresentedGroup (FreeGroup.freeGroupCongr e '' R) :=
374 PresentedGroup.equivPresentedGroup R e
377 (R : Set (FreeGroup X)) (e : X ≃ Y) :
378 TietzeEquiv R (FreeGroup.freeGroupCongr e '' R) :=
379 TietzeEquiv.ofMutualMapData
381 (FreeGroup.freeGroupCongr e)
382 R (FreeGroup.freeGroupCongr e '' R)
383 (by
384 intro r hr
385 exact Subgroup.subset_normalClosure ⟨r, hr, rfl⟩)
386 (by
387 intro s hs
388 rcases hs with ⟨r, hr, rfl⟩
389 have hback :
390 (FreeGroup.freeGroupCongr e).symm
391 ((FreeGroup.freeGroupCongr e) r) = r :=
392 (FreeGroup.freeGroupCongr e).left_inv r
393 rw [hback]
394 exact Subgroup.subset_normalClosure hr))
396end Presented
398end ReidemeisterSchreier.Discrete.Presentations