Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorAddition
1import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorReplacement
3/-!
4# Reidemeister Schreier / Discrete / Presentations / Tietze / Generator Addition
6This module formalizes adjoining generators with defining words. It builds
7the inclusion and elimination homomorphisms, transforms the relators, and
8packages the resulting presented-group equivalence.
9-/
11universe u v w
13namespace ReidemeisterSchreier.Discrete.Presentations
15namespace Presented
17variable {X Y : Type*}
19section AdjoinGenerators
21variable (X Y)
23/-- Include the old free group into the free group with a family of new generators. -/
24def includeAdjoinedGenerators : FreeGroup X →* FreeGroup (Sum X Y) :=
25 FreeGroup.map Sum.inl
27variable {X Y}
29/-- The elimination homomorphism sends every new generator \(y : Y\) to \(\mathrm{word}(y)\). -/
30def eliminateAdjoinedGeneratorsHom (word : Y → FreeGroup X) :
31 FreeGroup (Sum X Y) →* FreeGroup X :=
32 FreeGroup.lift (fun z =>
33 match z with
34 | Sum.inl x => FreeGroup.of x
35 | Sum.inr y => word y)
37/-- The elimination homomorphism fixes each original generator \(x : X\). -/
38@[simp]
39theorem eliminateAdjoinedGeneratorsHom_inl
40 (word : Y → FreeGroup X) (x : X) :
41 eliminateAdjoinedGeneratorsHom word (FreeGroup.of (Sum.inl x)) =
42 FreeGroup.of x := by
43 simp only [eliminateAdjoinedGeneratorsHom, FreeGroup.lift_apply_of]
45/-- The elimination homomorphism sends each adjoined generator \(y : Y\) to its defining word. -/
46@[simp]
47theorem eliminateAdjoinedGeneratorsHom_inr
48 (word : Y → FreeGroup X) (y : Y) :
49 eliminateAdjoinedGeneratorsHom word (FreeGroup.of (Sum.inr y)) =
50 word y := by
51 simp only [eliminateAdjoinedGeneratorsHom, FreeGroup.lift_apply_of]
53/--
54Eliminating the adjoined generators after including the original free group is the identity on
55the original free group.
56-/
57theorem eliminateAdjoinedGeneratorsHom_comp_include
58 (word : Y → FreeGroup X) :
59 (eliminateAdjoinedGeneratorsHom word).comp (includeAdjoinedGenerators X Y) =
60 MonoidHom.id (FreeGroup X) := by
61 ext x
62 simp only [includeAdjoinedGenerators, MonoidHom.coe_comp, Function.comp_apply, FreeGroup.map.of,
63 eliminateAdjoinedGeneratorsHom_inl, MonoidHom.id_apply]
65/-- Relators after adjoining generators \(y : Y\) and relations \(y = \mathrm{word}(y)\). -/
66def adjoinGeneratorsRelators
67 (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
68 Set (FreeGroup (Sum X Y)) :=
69 (includeAdjoinedGenerators X Y) '' R ∪
70 {q | ∃ y : Y,
71 q = FreeGroup.of (Sum.inr y) *
72 (includeAdjoinedGenerators X Y (word y))⁻¹}
74/--
75Each defining relation \(y = \mathrm{word}(y)\) for an adjoined generator belongs to the
76adjoined-generator relator set.
77-/
78theorem adjoinGenerators_relation_mem
79 (R : Set (FreeGroup X)) (word : Y → FreeGroup X) (y : Y) :
80 FreeGroup.of (Sum.inr y) *
81 (includeAdjoinedGenerators X Y (word y))⁻¹ ∈
82 adjoinGeneratorsRelators R word := by
83 exact Or.inr ⟨y, rfl⟩
85/--
86Including the result of eliminating adjoined generators is congruent to the original word modulo
87the adjoined-generator relators.
88-/
89theorem include_eliminateAdjoinedGeneratorsHom_mod_relators
90 (R : Set (FreeGroup X)) (word : Y → FreeGroup X)
91 (z : FreeGroup (Sum X Y)) :
92 includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word z) *
93 z⁻¹ ∈
94 Subgroup.normalClosure (adjoinGeneratorsRelators R word) := by
95 let S : Set (FreeGroup (Sum X Y)) := adjoinGeneratorsRelators R word
96 let N : Subgroup (FreeGroup (Sum X Y)) := Subgroup.normalClosure S
97 let F : FreeGroup (Sum X Y) →* FreeGroup (Sum X Y) :=
98 (includeAdjoinedGenerators X Y).comp (eliminateAdjoinedGeneratorsHom word)
99 have hhom : (QuotientGroup.mk' N).comp F = QuotientGroup.mk' N := by
100 ext z
101 cases z with
102 | inl x =>
103 simp only [includeAdjoinedGenerators, MonoidHom.coe_comp, QuotientGroup.coe_mk',
104 Function.comp_apply,
105 eliminateAdjoinedGeneratorsHom_inl, FreeGroup.map.of, QuotientGroup.mk'_apply, N, F]
106 | inr y =>
107 simp only [MonoidHom.comp_apply, F, eliminateAdjoinedGeneratorsHom,
108 FreeGroup.lift_apply_of]
109 change ((includeAdjoinedGenerators X Y (word y) : FreeGroup (Sum X Y)) :
110 FreeGroup (Sum X Y) ⧸ N) =
111 ((FreeGroup.of (Sum.inr y) : FreeGroup (Sum X Y)) :
112 FreeGroup (Sum X Y) ⧸ N)
113 apply (QuotientGroup.eq_iff_div_mem
114 (N := N)
115 (x := includeAdjoinedGenerators X Y (word y))
116 (y := FreeGroup.of (Sum.inr y))).2
117 have hrel :
118 FreeGroup.of (Sum.inr y) *
119 (includeAdjoinedGenerators X Y (word y))⁻¹ ∈ N :=
120 Subgroup.subset_normalClosure
121 (adjoinGenerators_relation_mem R word y)
122 have hinv :
123 (FreeGroup.of (Sum.inr y) *
124 (includeAdjoinedGenerators X Y (word y))⁻¹)⁻¹ ∈ N :=
125 N.inv_mem hrel
126 simpa [N, div_eq_mul_inv, mul_assoc] using hinv
127 have hz := congrArg (fun f : FreeGroup (Sum X Y) →*
128 FreeGroup (Sum X Y) ⧸ N => f z) hhom
129 change (includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word z) :
130 FreeGroup (Sum X Y) ⧸ N) = z at hz
131 exact (QuotientGroup.eq_iff_div_mem
132 (N := N)
133 (x := includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word z))
134 (y := z)).1 hz
136/--
137Adding generators with defining relations gives mutual maps between the original relator
138quotient and the enlarged one.
139-/
140def adjoinGeneratorsMutualMapData
141 (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
142 RelatorQuotientMutualMapData R (adjoinGeneratorsRelators R word) where
143 toHom := includeAdjoinedGenerators X Y
144 invHom := eliminateAdjoinedGeneratorsHom word
145 mapsRelators := by
146 intro r hr
147 exact Subgroup.subset_normalClosure (Or.inl ⟨r, hr, rfl⟩)
148 mapsTargetRelators := by
149 intro s hs
150 rcases hs with hs | hs
151 · rcases hs with ⟨r, hr, rfl⟩
152 have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f r)
153 (eliminateAdjoinedGeneratorsHom_comp_include word)
154 have hrw :
155 eliminateAdjoinedGeneratorsHom word (includeAdjoinedGenerators X Y r) = r := by
156 simpa using hcomp
157 simpa [hrw] using (Subgroup.subset_normalClosure hr :
158 r ∈ Subgroup.normalClosure R)
159 · rcases hs with ⟨y, rfl⟩
160 have hw :
161 eliminateAdjoinedGeneratorsHom word
162 (includeAdjoinedGenerators X Y (word y)) = word y := by
163 have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f (word y))
164 (eliminateAdjoinedGeneratorsHom_comp_include word)
165 simpa using hcomp
166 simp only [map_mul, map_inv, eliminateAdjoinedGeneratorsHom_inr]
167 change word y *
168 (eliminateAdjoinedGeneratorsHom word
169 (includeAdjoinedGenerators X Y (word y)))⁻¹ ∈
170 Subgroup.normalClosure R
171 simp only [hw, mul_inv_cancel, one_mem]
172 inv_toHom := by
173 intro x
174 have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f x)
175 (eliminateAdjoinedGeneratorsHom_comp_include word)
176 have hx :
177 eliminateAdjoinedGeneratorsHom word (includeAdjoinedGenerators X Y x) = x := by
178 simpa using hcomp
179 simp only [hx, mul_inv_cancel, one_mem]
180 to_invHom := by
181 intro z
182 exact include_eliminateAdjoinedGeneratorsHom_mod_relators R word z
184/--
185The Tietze equivalence obtained by adjoining generators \(y : Y\) with defining relations \(y =
186\mathrm{word}(y)\).
187-/
188def adjoinGeneratorsTietzeEquiv
189 (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
190 TietzeEquiv R (adjoinGeneratorsRelators R word) :=
191 TietzeEquiv.ofMutualMapData (adjoinGeneratorsMutualMapData R word)
193/-- Tietze move: adding a family of generators \(y : Y\) with relations \(y = \mathrm{word}(y)\). -/
194noncomputable def adjoinGenerators
195 (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
196 PresentedGroup R ≃*
197 PresentedGroup (adjoinGeneratorsRelators R word) :=
198 (adjoinGeneratorsTietzeEquiv R word).presentedEquiv
200section SubstituteDefinedGenerators
202/--
203Relations \(y = \mathrm{word}(y)\) for generators that will be eliminated from an arbitrary
204presentation over \(X \oplus Y\).
205-/
206def definedGeneratorRelators
207 (word : Y → FreeGroup X) :
208 Set (FreeGroup (Sum X Y)) :=
209 {q | ∃ y : Y,
210 q = FreeGroup.of (Sum.inr y) *
211 (includeAdjoinedGenerators X Y (word y))⁻¹}
213/--
214Add defining relations \(y = \mathrm{word}(y)\) to an arbitrary presentation over \(X \oplus
215Y\). Unlike \(\mathrm{adjoinGeneratorsRelators}\), the old relators may already involve the
216\(Y\)-generators.
217-/
218def relatorsWithDefinedGenerators
219 (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) :
220 Set (FreeGroup (Sum X Y)) :=
221 R ∪ definedGeneratorRelators word
223/-- Relators after substituting every generator \(y : Y\) by \(\mathrm{word}(y)\). -/
224def relatorsAfterSubstitutingDefinedGenerators
225 (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) :
226 Set (FreeGroup X) :=
227 eliminateAdjoinedGeneratorsHom word '' R
229/--
230Each defining relation \(y = \mathrm{word}(y)\) belongs to the defining-generator relator set.
231-/
232theorem definedGeneratorRelator_mem
233 (word : Y → FreeGroup X) (y : Y) :
234 FreeGroup.of (Sum.inr y) *
235 (includeAdjoinedGenerators X Y (word y))⁻¹ ∈
236 definedGeneratorRelators word :=
237 ⟨y, rfl⟩
239/--
240Each defining relation \(y = \mathrm{word}(y)\) belongs to the relator set with defined
241generators.
242-/
243theorem definedGeneratorRelator_mem_relatorsWithDefinedGenerators
244 (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) (y : Y) :
245 FreeGroup.of (Sum.inr y) *
246 (includeAdjoinedGenerators X Y (word y))⁻¹ ∈
247 relatorsWithDefinedGenerators R word :=
248 Or.inr (definedGeneratorRelator_mem word y)
250/-- Every original relator belongs to the relator set with defined generators. -/
251theorem relator_mem_relatorsWithDefinedGenerators
252 {R : Set (FreeGroup (Sum X Y))} {word : Y → FreeGroup X}
253 {r : FreeGroup (Sum X Y)} (hr : r ∈ R) :
254 r ∈ relatorsWithDefinedGenerators R word :=
255 Or.inl hr
257/--
258Including the result of eliminating adjoined generators is congruent to the original word modulo
259the defining-generator relators.
260-/
261theorem include_eliminateAdjoinedGeneratorsHom_mod_definedGeneratorRelators
262 (word : Y → FreeGroup X) (z : FreeGroup (Sum X Y)) :
263 includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word z) *
264 z⁻¹ ∈
265 Subgroup.normalClosure (definedGeneratorRelators word) := by
266 let S : Set (FreeGroup (Sum X Y)) := definedGeneratorRelators word
267 let N : Subgroup (FreeGroup (Sum X Y)) := Subgroup.normalClosure S
268 let F : FreeGroup (Sum X Y) →* FreeGroup (Sum X Y) :=
269 (includeAdjoinedGenerators X Y).comp (eliminateAdjoinedGeneratorsHom word)
270 have hhom : (QuotientGroup.mk' N).comp F = QuotientGroup.mk' N := by
271 ext z
272 cases z with
273 | inl x =>
274 simp only [includeAdjoinedGenerators, MonoidHom.coe_comp, QuotientGroup.coe_mk',
275 Function.comp_apply,
276 eliminateAdjoinedGeneratorsHom_inl, FreeGroup.map.of, QuotientGroup.mk'_apply, N, F]
277 | inr y =>
278 simp only [MonoidHom.comp_apply, F, eliminateAdjoinedGeneratorsHom,
279 FreeGroup.lift_apply_of]
280 change ((includeAdjoinedGenerators X Y (word y) : FreeGroup (Sum X Y)) :
281 FreeGroup (Sum X Y) ⧸ N) =
282 ((FreeGroup.of (Sum.inr y) : FreeGroup (Sum X Y)) :
283 FreeGroup (Sum X Y) ⧸ N)
284 apply (QuotientGroup.eq_iff_div_mem
285 (N := N)
286 (x := includeAdjoinedGenerators X Y (word y))
287 (y := FreeGroup.of (Sum.inr y))).2
288 have hrel :
289 FreeGroup.of (Sum.inr y) *
290 (includeAdjoinedGenerators X Y (word y))⁻¹ ∈ N :=
291 Subgroup.subset_normalClosure
292 (definedGeneratorRelator_mem word y)
293 have hinv :
294 (FreeGroup.of (Sum.inr y) *
295 (includeAdjoinedGenerators X Y (word y))⁻¹)⁻¹ ∈ N :=
296 N.inv_mem hrel
297 simpa [N, div_eq_mul_inv, mul_assoc] using hinv
298 have hz := congrArg (fun f : FreeGroup (Sum X Y) →*
299 FreeGroup (Sum X Y) ⧸ N => f z) hhom
300 change (includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word z) :
301 FreeGroup (Sum X Y) ⧸ N) = z at hz
302 exact (QuotientGroup.eq_iff_div_mem
303 (N := N)
304 (x := includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word z))
305 (y := z)).1 hz
307/--
308Including the result of eliminating defined generators is congruent to the original word modulo
309the relators with defined generators.
310-/
311theorem include_eliminateAdjoinedGeneratorsHom_mod_relatorsWithDefinedGenerators
312 (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X)
313 (z : FreeGroup (Sum X Y)) :
314 includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word z) *
315 z⁻¹ ∈
316 Subgroup.normalClosure (relatorsWithDefinedGenerators R word) :=
317 Subgroup.normalClosure_mono
318 (fun _ hq => Or.inr hq)
319 (include_eliminateAdjoinedGeneratorsHom_mod_definedGeneratorRelators
320 (X := X) (Y := Y) word z)
322/--
323Substituting each defined generator by its defining word gives mutual maps for the presentation
324with those generators eliminated.
325-/
326def substituteDefinedGeneratorsMutualMapData
327 (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) :
328 RelatorQuotientMutualMapData
329 (relatorsWithDefinedGenerators R word)
330 (relatorsAfterSubstitutingDefinedGenerators R word) where
331 toHom := eliminateAdjoinedGeneratorsHom word
332 invHom := includeAdjoinedGenerators X Y
333 mapsRelators := by
334 intro r hr
335 rcases hr with hr | hr
336 · exact Subgroup.subset_normalClosure ⟨r, hr, rfl⟩
337 · rcases hr with ⟨y, rfl⟩
338 have hw :
339 eliminateAdjoinedGeneratorsHom word
340 (includeAdjoinedGenerators X Y (word y)) = word y := by
341 have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f (word y))
342 (eliminateAdjoinedGeneratorsHom_comp_include word)
343 simpa using hcomp
344 simp only [map_mul, map_inv, eliminateAdjoinedGeneratorsHom_inr]
345 change word y *
346 (eliminateAdjoinedGeneratorsHom word
347 (includeAdjoinedGenerators X Y (word y)))⁻¹ ∈
348 Subgroup.normalClosure (relatorsAfterSubstitutingDefinedGenerators R word)
349 simp only [hw, mul_inv_cancel, one_mem]
350 mapsTargetRelators := by
351 intro s hs
352 rcases hs with ⟨r, hr, rfl⟩
353 let N : Subgroup (FreeGroup (Sum X Y)) :=
354 Subgroup.normalClosure (relatorsWithDefinedGenerators R word)
355 have hmod :
356 includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word r) *
357 r⁻¹ ∈ N :=
358 include_eliminateAdjoinedGeneratorsHom_mod_relatorsWithDefinedGenerators
359 (X := X) (Y := Y) R word r
360 have hrN : r ∈ N :=
361 Subgroup.subset_normalClosure
362 (relator_mem_relatorsWithDefinedGenerators (R := R) (word := word) hr)
363 have hprod := Subgroup.mul_mem N hmod hrN
364 convert hprod using 1
365 group
366 inv_toHom := by
367 intro z
368 exact include_eliminateAdjoinedGeneratorsHom_mod_relatorsWithDefinedGenerators
369 (X := X) (Y := Y) R word z
370 to_invHom := by
371 intro z
372 have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f z)
373 (eliminateAdjoinedGeneratorsHom_comp_include word)
374 have hz :
375 eliminateAdjoinedGeneratorsHom word (includeAdjoinedGenerators X Y z) = z := by
376 simpa using hcomp
377 simp only [hz, mul_inv_cancel, one_mem]
379/-- The Tietze equivalence obtained by substituting each defined generator by its defining word. -/
380def substituteDefinedGeneratorsTietzeEquiv
381 (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) :
382 TietzeEquiv
383 (relatorsWithDefinedGenerators R word)
384 (relatorsAfterSubstitutingDefinedGenerators R word) :=
385 TietzeEquiv.ofMutualMapData
386 (substituteDefinedGeneratorsMutualMapData R word)
388/--
389Tietze move eliminating generators \(y : Y\) using relations \(y = \mathrm{word}(y)\), while
390substituting \(\mathrm{word}(y)\) into all remaining relators.
391-/
392noncomputable def substituteDefinedGenerators
393 (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) :
394 PresentedGroup (relatorsWithDefinedGenerators R word) ≃*
395 PresentedGroup (relatorsAfterSubstitutingDefinedGenerators R word) :=
396 (substituteDefinedGeneratorsTietzeEquiv R word).presentedEquiv
398end SubstituteDefinedGenerators
400end AdjoinGenerators
402end Presented
404end ReidemeisterSchreier.Discrete.Presentations