ReidemeisterSchreier/Discrete/Presentations/Tietze/GeneratorDeletion.lean
1import ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorAddition
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ReidemeisterSchreier/Discrete/Presentations/Tietze/GeneratorDeletion.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*}
25section AdjoinGenerators
27section DeleteTrivialGenerators
29variable (X Y)
31/-- Send the generators in `Y` to `1`, while keeping the old generators
32`X`. This is the substitution map used by the Tietze move deleting
34def trivializeGeneratorsHom : FreeGroup (Sum X Y) →* FreeGroup X :=
35 eliminateAdjoinedGeneratorsHom (fun _ : Y => 1)
37variable {X Y}
39@[simp]
40theorem trivializeGeneratorsHom_inl (x : X) :
41 trivializeGeneratorsHom X Y (FreeGroup.of (Sum.inl x)) =
42 FreeGroup.of x := by
43 simp only [trivializeGeneratorsHom, eliminateAdjoinedGeneratorsHom_inl]
45@[simp]
46theorem trivializeGeneratorsHom_inr (y : Y) :
47 trivializeGeneratorsHom X Y (FreeGroup.of (Sum.inr y)) = 1 := by
48 simp only [trivializeGeneratorsHom, eliminateAdjoinedGeneratorsHom_inr]
50theorem trivializeGeneratorsHom_comp_include :
51 (trivializeGeneratorsHom X Y).comp (includeAdjoinedGenerators X Y) =
52 MonoidHom.id (FreeGroup X) :=
53 eliminateAdjoinedGeneratorsHom_comp_include (fun _ : Y => 1)
55/-- Relators `y = 1` for a family of generators to be deleted. -/
57 Set (FreeGroup (Sum X Y)) :=
58 {q | ∃ y : Y, q = FreeGroup.of (Sum.inr y)}
60/-- Add the relators `y = 1` to a presentation over `X ⊕ Y`. -/
62 (R : Set (FreeGroup (Sum X Y))) :
63 Set (FreeGroup (Sum X Y)) :=
64 R ∪ trivialGeneratorRelators (X := X) (Y := Y)
66/-- Relators after deleting the `Y` generators by substituting them with `1`. -/
68 (R : Set (FreeGroup (Sum X Y))) :
69 Set (FreeGroup X) :=
70 trivializeGeneratorsHom X Y '' R
72theorem trivialGeneratorRelator_mem (y : Y) :
73 FreeGroup.of (Sum.inr y) ∈
74 trivialGeneratorRelators (X := X) (Y := Y) :=
75 ⟨y, rfl⟩
78 (R : Set (FreeGroup (Sum X Y))) (y : Y) :
79 FreeGroup.of (Sum.inr y) ∈ relatorsWithTrivialGenerators R :=
80 Or.inr (trivialGeneratorRelator_mem (X := X) (Y := Y) y)
83 {R : Set (FreeGroup (Sum X Y))} {r : FreeGroup (Sum X Y)}
84 (hr : r ∈ R) :
85 r ∈ relatorsWithTrivialGenerators R :=
86 Or.inl hr
89 (z : FreeGroup (Sum X Y)) :
90 includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y z) * z⁻¹ ∈
91 Subgroup.normalClosure (trivialGeneratorRelators (X := X) (Y := Y)) := by
92 let S : Set (FreeGroup (Sum X Y)) :=
93 trivialGeneratorRelators (X := X) (Y := Y)
94 let N : Subgroup (FreeGroup (Sum X Y)) := Subgroup.normalClosure S
95 let F : FreeGroup (Sum X Y) →* FreeGroup (Sum X Y) :=
96 (includeAdjoinedGenerators X Y).comp (trivializeGeneratorsHom X Y)
97 have hhom : (QuotientGroup.mk' N).comp F = QuotientGroup.mk' N := by
98 ext z
99 cases z with
100 | inl x =>
101 simp only [includeAdjoinedGenerators, trivializeGeneratorsHom, MonoidHom.coe_comp, QuotientGroup.coe_mk',
102 Function.comp_apply, eliminateAdjoinedGeneratorsHom_inl, FreeGroup.map.of, QuotientGroup.mk'_apply, N, F]
103 | inr y =>
104 simp only [MonoidHom.comp_apply, F, trivializeGeneratorsHom_inr,
106 change ((1 : FreeGroup (Sum X Y)) : FreeGroup (Sum X Y) ⧸ N) =
107 ((FreeGroup.of (Sum.inr y) : FreeGroup (Sum X Y)) :
108 FreeGroup (Sum X Y) ⧸ N)
109 apply (QuotientGroup.eq_iff_div_mem
110 (N := N)
111 (x := (1 : FreeGroup (Sum X Y)))
112 (y := FreeGroup.of (Sum.inr y))).2
113 have hrel :
114 FreeGroup.of (Sum.inr y) ∈ N :=
115 Subgroup.subset_normalClosure
116 (trivialGeneratorRelator_mem (X := X) (Y := Y) y)
117 simpa [N, div_eq_mul_inv] using N.inv_mem hrel
118 have hz := congrArg (fun f : FreeGroup (Sum X Y) →*
119 FreeGroup (Sum X Y) ⧸ N => f z) hhom
120 change (includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y z) :
121 FreeGroup (Sum X Y) ⧸ N) = z at hz
122 exact (QuotientGroup.eq_iff_div_mem
123 (N := N)
124 (x := includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y z))
125 (y := z)).1 hz
128 (R : Set (FreeGroup (Sum X Y))) (z : FreeGroup (Sum X Y)) :
129 includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y z) * z⁻¹ ∈
130 Subgroup.normalClosure (relatorsWithTrivialGenerators R) :=
131 Subgroup.normalClosure_mono
132 (fun _ hq => Or.inr hq)
134 (X := X) (Y := Y) z)
137 (R : Set (FreeGroup (Sum X Y))) :
140 (relatorsAfterDeletingTrivialGenerators R) where
141 toHom := trivializeGeneratorsHom X Y
142 invHom := includeAdjoinedGenerators X Y
143 mapsRelators := by
144 intro r hr
145 rcases hr with hr | hr
146 · exact Subgroup.subset_normalClosure ⟨r, hr, rfl⟩
147 · rcases hr with ⟨y, rfl⟩
148 simp only [trivializeGeneratorsHom_inr, one_mem]
149 mapsTargetRelators := by
150 intro s hs
151 rcases hs with ⟨r, hr, rfl⟩
152 let N : Subgroup (FreeGroup (Sum X Y)) :=
153 Subgroup.normalClosure (relatorsWithTrivialGenerators R)
154 have hmod :
155 includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y r) *
156 r⁻¹ ∈ N :=
158 (X := X) (Y := Y) R r
159 have hrN : r ∈ N :=
160 Subgroup.subset_normalClosure
161 (relator_mem_relatorsWithTrivialGenerators (R := R) hr)
162 have hprod := Subgroup.mul_mem N hmod hrN
163 convert hprod using 1
164 group
165 inv_toHom := by
166 intro z
168 (X := X) (Y := Y) R z
169 to_invHom := by
170 intro z
171 have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f z)
172 (trivializeGeneratorsHom_comp_include (X := X) (Y := Y))
173 have hz :
174 trivializeGeneratorsHom X Y (includeAdjoinedGenerators X Y z) = z := by
175 simpa using hcomp
176 simp only [hz, mul_inv_cancel, one_mem]
179 (R : Set (FreeGroup (Sum X Y))) :
183 TietzeEquiv.ofMutualMapData
186/-- Tietze move deleting a family of generators that have relators `y = 1`.
187Every remaining relator is pushed forward by substituting those deleted
188generators with `1`. -/
189noncomputable def deleteTrivialGenerators
190 (R : Set (FreeGroup (Sum X Y))) :
191 PresentedGroup (relatorsWithTrivialGenerators R) ≃*
192 PresentedGroup (relatorsAfterDeletingTrivialGenerators R) :=
193 (deleteTrivialGeneratorsTietzeEquiv R).presentedEquiv
195end DeleteTrivialGenerators
197section DeleteGeneratorsAlongEquiv
199variable {Z X Y : Type*}
201namespace GeneratorPartition
203/-- Generators kept after deleting the generators satisfying `delete`. -/
205 {z : Z // ¬ delete z}
207/-- Generators deleted by a predicate `delete`. -/
209 {z : Z // delete z}
211/-- Split an arbitrary generator type into the generators kept and deleted by
212a decidable predicate. -/
213def equiv (delete : Z → Prop) [DecidablePred delete] :
215 toFun z :=
216 if hz : delete z then
217 Sum.inr ⟨z, hz⟩
218 else
219 Sum.inl ⟨z, hz⟩
220 invFun z :=
221 match z with
222 | Sum.inl x => x.1
223 | Sum.inr y => y.1
224 left_inv z := by
225 by_cases hz : delete z <;> simp only [hz, ↓reduceDIte]
226 right_inv z := by
227 cases z with
228 | inl x =>
230 | inr y =>
233@[simp]
234theorem equiv_apply_of_delete
235 (delete : Z → Prop) [DecidablePred delete]
236 {z : Z} (hz : delete z) :
238 simp only [equiv, Equiv.coe_fn_mk, hz, ↓reduceDIte]
240@[simp]
241theorem equiv_apply_of_not_delete
242 (delete : Z → Prop) [DecidablePred delete]
243 {z : Z} (hz : ¬ delete z) :
245 simp only [equiv, Equiv.coe_fn_mk, hz, ↓reduceDIte]
247@[simp]
248theorem equiv_symm_inl
249 (delete : Z → Prop) [DecidablePred delete]
251 (equiv delete).symm (Sum.inl z) = z.1 :=
252 rfl
254@[simp]
255theorem equiv_symm_inr
256 (delete : Z → Prop) [DecidablePred delete]
258 (equiv delete).symm (Sum.inr z) = z.1 :=
259 rfl
261end GeneratorPartition
263/-- Pull back the defining relators `y = word y` along an equivalence that
266 (e : Z ≃ Sum X Y) (word : Y → FreeGroup X) :
267 Set (FreeGroup Z) :=
268 (FreeGroup.freeGroupCongr e).symm ''
269 definedGeneratorRelators (X := X) (Y := Y) word
271/-- Add defining relators to an arbitrary presentation whose generator type is
272identified with `X ⊕ Y`. -/
274 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
275 (word : Y → FreeGroup X) :
276 Set (FreeGroup Z) :=
277 R ∪ definedGeneratorRelatorsAlongEquiv e word
279/-- Relators after renaming by `e` and substituting every deleted generator
280`y : Y` by `word y`. -/
282 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
283 (word : Y → FreeGroup X) :
284 Set (FreeGroup X) :=
286 (FreeGroup.freeGroupCongr e '' R) word
289 (e : Z ≃ Sum X Y) (word : Y → FreeGroup X) :
290 FreeGroup.freeGroupCongr e ''
291 definedGeneratorRelatorsAlongEquiv e word =
292 definedGeneratorRelators (X := X) (Y := Y) word := by
293 ext q
294 constructor
295 · rintro ⟨z, hz, rfl⟩
296 rcases hz with ⟨p, hp, hpz⟩
297 have hpmap :
298 FreeGroup.map (fun z : Z => e z)
299 (FreeGroup.map (fun z : Sum X Y => e.symm z) p) = p := by
300 simpa [FreeGroup.freeGroupCongr] using
301 (FreeGroup.freeGroupCongr e).right_inv p
302 simpa [FreeGroup.freeGroupCongr, ← hpz, hpmap] using hp
303 · intro hq
304 exact ⟨(FreeGroup.freeGroupCongr e).symm q, ⟨q, hq, rfl⟩,
305 (FreeGroup.freeGroupCongr e).right_inv q⟩
308 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
309 (word : Y → FreeGroup X) :
310 FreeGroup.freeGroupCongr e ''
311 relatorsWithDefinedGeneratorsAlongEquiv R e word =
313 (FreeGroup.freeGroupCongr e '' R) word := by
314 ext q
315 constructor
316 · rintro ⟨z, hz, rfl⟩
317 rcases hz with hz | hz
318 · exact Or.inl ⟨z, hz, rfl⟩
319 · rcases hz with ⟨p, hp, hpz⟩
320 exact Or.inr (by
321 have hpmap :
322 FreeGroup.map (fun z : Z => e z)
323 (FreeGroup.map (fun z : Sum X Y => e.symm z) p) = p := by
324 simpa [FreeGroup.freeGroupCongr] using
325 (FreeGroup.freeGroupCongr e).right_inv p
326 simpa [FreeGroup.freeGroupCongr, ← hpz, hpmap] using hp)
327 · intro hq
328 rcases hq with hq | hq
329 · rcases hq with ⟨z, hz, hzq⟩
330 exact ⟨z, Or.inl hz, hzq⟩
331 · exact ⟨(FreeGroup.freeGroupCongr e).symm q,
332 Or.inr ⟨q, hq, rfl⟩,
333 (FreeGroup.freeGroupCongr e).right_inv q⟩
335/-- Tietze move eliminating an arbitrary family of generators after splitting
338 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
339 (word : Y → FreeGroup X) :
341 (relatorsWithDefinedGeneratorsAlongEquiv R e word)
342 (relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv R e word) :=
344 (relatorsWithDefinedGeneratorsAlongEquiv R e word) e).trans
345 ((TietzeEquiv.ofNormalClosureEq
346 (R := FreeGroup.freeGroupCongr e ''
347 relatorsWithDefinedGeneratorsAlongEquiv R e word)
349 (FreeGroup.freeGroupCongr e '' R) word)
350 (by
353 (FreeGroup.freeGroupCongr e '' R) word))
355noncomputable def substituteDefinedGeneratorsAlongEquiv
356 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
357 (word : Y → FreeGroup X) :
358 PresentedGroup (relatorsWithDefinedGeneratorsAlongEquiv R e word) ≃*
359 PresentedGroup
360 (relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv R e word) :=
361 (substituteDefinedGeneratorsAlongEquivTietzeEquiv R e word).presentedEquiv
363/-- Add defining relations for all generators satisfying `delete`. The kept
366 (delete : Z → Prop) [DecidablePred delete]
367 (word :
368 GeneratorPartition.Deleted delete →
369 FreeGroup (GeneratorPartition.Kept delete)) :
370 Set (FreeGroup Z) :=
372 (GeneratorPartition.equiv delete) word
375 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]
376 (word :
377 GeneratorPartition.Deleted delete →
378 FreeGroup (GeneratorPartition.Kept delete)) :
379 Set (FreeGroup Z) :=
381 (GeneratorPartition.equiv delete) word
384 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]
385 (word :
386 GeneratorPartition.Deleted delete →
387 FreeGroup (GeneratorPartition.Kept delete)) :
388 Set (FreeGroup (GeneratorPartition.Kept delete)) :=
390 (GeneratorPartition.equiv delete) word
393 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]
394 (word :
395 GeneratorPartition.Deleted delete →
396 FreeGroup (GeneratorPartition.Kept delete)) :
398 (relatorsWithDefinedGeneratorsOfPredicate R delete word)
399 (relatorsAfterSubstitutingDefinedGeneratorsOfPredicate R delete word) :=
401 (GeneratorPartition.equiv delete) word
403noncomputable def substituteDefinedGeneratorsOfPredicate
404 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]
405 (word :
406 GeneratorPartition.Deleted delete →
407 FreeGroup (GeneratorPartition.Kept delete)) :
408 PresentedGroup (relatorsWithDefinedGeneratorsOfPredicate R delete word) ≃*
409 PresentedGroup
410 (relatorsAfterSubstitutingDefinedGeneratorsOfPredicate R delete word) :=
411 (substituteDefinedGeneratorsOfPredicateTietzeEquiv R delete word).presentedEquiv
413/-- Pull back the trivial-generator relators `y = 1` along an equivalence that
416 (e : Z ≃ Sum X Y) :
417 Set (FreeGroup Z) :=
418 (FreeGroup.freeGroupCongr e).symm ''
419 trivialGeneratorRelators (X := X) (Y := Y)
421/-- Add trivial-generator relators to an arbitrary presentation whose generator
422type is identified with `X ⊕ Y`. -/
424 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
425 Set (FreeGroup Z) :=
428/-- Relators after renaming by `e` and deleting every generator in `Y`. -/
430 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
431 Set (FreeGroup X) :=
432 relatorsAfterDeletingTrivialGenerators (FreeGroup.freeGroupCongr e '' R)
435 (e : Z ≃ Sum X Y) :
436 FreeGroup.freeGroupCongr e ''
437 trivialGeneratorRelatorsAlongEquiv (X := X) (Y := Y) e =
438 trivialGeneratorRelators (X := X) (Y := Y) := by
439 ext q
440 constructor
441 · rintro ⟨z, hz, rfl⟩
442 rcases hz with ⟨p, hp, hpz⟩
443 have hpmap :
444 FreeGroup.map (fun z : Z => e z)
445 (FreeGroup.map (fun z : Sum X Y => e.symm z) p) = p := by
446 simpa [FreeGroup.freeGroupCongr] using
447 (FreeGroup.freeGroupCongr e).right_inv p
448 simpa [FreeGroup.freeGroupCongr, ← hpz, hpmap] using hp
449 · intro hq
450 exact ⟨(FreeGroup.freeGroupCongr e).symm q, ⟨q, hq, rfl⟩,
451 (FreeGroup.freeGroupCongr e).right_inv q⟩
454 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
455 FreeGroup.freeGroupCongr e ''
457 relatorsWithTrivialGenerators (FreeGroup.freeGroupCongr e '' R) := by
458 ext q
459 constructor
460 · rintro ⟨z, hz, rfl⟩
461 rcases hz with hz | hz
462 · exact Or.inl ⟨z, hz, rfl⟩
463 · rcases hz with ⟨p, hp, hpz⟩
464 exact Or.inr (by
465 have hpmap :
466 FreeGroup.map (fun z : Z => e z)
467 (FreeGroup.map (fun z : Sum X Y => e.symm z) p) = p := by
468 simpa [FreeGroup.freeGroupCongr] using
469 (FreeGroup.freeGroupCongr e).right_inv p
470 simpa [FreeGroup.freeGroupCongr, ← hpz, hpmap] using hp)
471 · intro hq
472 rcases hq with hq | hq
473 · rcases hq with ⟨z, hz, hzq⟩
474 exact ⟨z, Or.inl hz, hzq⟩
475 · exact ⟨(FreeGroup.freeGroupCongr e).symm q,
476 Or.inr ⟨q, hq, rfl⟩,
477 (FreeGroup.freeGroupCongr e).right_inv q⟩
479/-- Tietze move deleting an arbitrary family of generators after splitting the
482 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
487 (relatorsWithTrivialGeneratorsAlongEquiv R e) e).trans
488 ((TietzeEquiv.ofNormalClosureEq
489 (R := FreeGroup.freeGroupCongr e ''
492 (FreeGroup.freeGroupCongr e '' R))
493 (by
496 (FreeGroup.freeGroupCongr e '' R)))
498noncomputable def deleteTrivialGeneratorsAlongEquiv
499 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
500 PresentedGroup (relatorsWithTrivialGeneratorsAlongEquiv R e) ≃*
501 PresentedGroup
503 (deleteTrivialGeneratorsAlongEquivTietzeEquiv R e).presentedEquiv
505/-- Trivial-generator relators for the generators satisfying `delete`. -/
507 (delete : Z → Prop) [DecidablePred delete] :
508 Set (FreeGroup Z) :=
510 (X := GeneratorPartition.Kept delete)
511 (Y := GeneratorPartition.Deleted delete)
512 (GeneratorPartition.equiv delete)
515 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :
516 Set (FreeGroup Z) :=
518 (X := GeneratorPartition.Kept delete)
519 (Y := GeneratorPartition.Deleted delete)
520 (GeneratorPartition.equiv delete)
523 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :
524 Set (FreeGroup (GeneratorPartition.Kept delete)) :=
526 (X := GeneratorPartition.Kept delete)
527 (Y := GeneratorPartition.Deleted delete)
528 (GeneratorPartition.equiv delete)
531 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :
533 (relatorsWithTrivialGeneratorsOfPredicate R delete)
534 (relatorsAfterDeletingTrivialGeneratorsOfPredicate R delete) :=
536 (X := GeneratorPartition.Kept delete)
537 (Y := GeneratorPartition.Deleted delete)
538 (GeneratorPartition.equiv delete)
540noncomputable def deleteTrivialGeneratorsOfPredicate
541 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :
542 PresentedGroup (relatorsWithTrivialGeneratorsOfPredicate R delete) ≃*
543 PresentedGroup
544 (relatorsAfterDeletingTrivialGeneratorsOfPredicate R delete) :=
545 (deleteTrivialGeneratorsOfPredicateTietzeEquiv R delete).presentedEquiv
547end DeleteGeneratorsAlongEquiv
549end AdjoinGenerators
551end Presented
553end ReidemeisterSchreier.Discrete.Presentations