ReidemeisterSchreier/Discrete/Presentations/Tietze/Script.lean
1import ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorDeletion
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ReidemeisterSchreier/Discrete/Presentations/Tietze/Script.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 TietzeScript
23variable {X Y Z : Type*}
25def replaceRelators
26 {R S : Set (FreeGroup X)}
27 (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
28 (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
29 TietzeScript (Presentation.ofRelators R) (Presentation.ofRelators S) :=
32def replaceRelator
33 {R : Set (FreeGroup X)} {oldRelator newRelator : FreeGroup X}
34 (holdRelator :
35 RelatorEquivalent (insert newRelator (R \ {oldRelator})) oldRelator 1)
36 (hnewRelator : RelatorEquivalent R newRelator 1) :
37 TietzeScript (Presentation.ofRelators R)
38 (Presentation.ofRelators (insert newRelator (R \ {oldRelator}))) :=
41def addRedundantRelator
42 {R : Set (FreeGroup X)} {r : FreeGroup X}
43 (hr : r ∈ Subgroup.normalClosure R) :
44 TietzeScript (Presentation.ofRelators (insert r R))
45 (Presentation.ofRelators R) :=
49 {R : Set (FreeGroup X)} {r : FreeGroup X}
50 (hr : r ∈ Subgroup.normalClosure R) :
51 TietzeScript (Presentation.ofRelators R)
52 (Presentation.ofRelators (insert r R)) :=
53 (Presented.addRedundantRelatorTietzeEquiv hr).symm.toScript
55def removeRedundantRelator
56 {R : Set (FreeGroup X)} {r : FreeGroup X}
57 (hr : r ∈ Subgroup.normalClosure (R \ {r})) :
58 TietzeScript (Presentation.ofRelators R)
59 (Presentation.ofRelators (R \ {r})) :=
62def addRedundantRelators
63 {R S : Set (FreeGroup X)}
64 (hS : S ⊆ Subgroup.normalClosure R) :
65 TietzeScript (Presentation.ofRelators (R ∪ S))
66 (Presentation.ofRelators R) :=
69def addRedundantRelatorsRelatorEquivalent
70 {R S : Set (FreeGroup X)}
71 (hS : ∀ s ∈ S, RelatorEquivalent R s 1) :
72 TietzeScript (Presentation.ofRelators (R ∪ S))
73 (Presentation.ofRelators R) :=
76def addRedundantRelatorsInverse
77 {R S : Set (FreeGroup X)}
78 (hS : S ⊆ Subgroup.normalClosure R) :
79 TietzeScript (Presentation.ofRelators R)
80 (Presentation.ofRelators (R ∪ S)) :=
81 (Presented.addRedundantRelatorsTietzeEquiv hS).symm.toScript
83def addRedundantRelatorsRelatorEquivalentInverse
84 {R S : Set (FreeGroup X)}
85 (hS : ∀ s ∈ S, RelatorEquivalent R s 1) :
86 TietzeScript (Presentation.ofRelators R)
87 (Presentation.ofRelators (R ∪ S)) :=
88 (Presented.addRedundantRelatorsRelatorEquivalentTietzeEquiv hS).symm.toScript
90def removeRelatorSubset
91 {R D : Set (FreeGroup X)}
92 (hD : ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure (R \ D)) :
93 TietzeScript (Presentation.ofRelators R)
94 (Presentation.ofRelators (R \ D)) :=
97def removeRelatorSubsetRelatorEquivalent
98 {R D : Set (FreeGroup X)}
99 (hD : ∀ d ∈ D, d ∈ R → RelatorEquivalent (R \ D) d 1) :
100 TietzeScript (Presentation.ofRelators R)
101 (Presentation.ofRelators (R \ D)) :=
104def removeRelatorSubsetInverse
105 {R D : Set (FreeGroup X)}
106 (hD : ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure (R \ D)) :
107 TietzeScript (Presentation.ofRelators (R \ D))
108 (Presentation.ofRelators R) :=
109 (Presented.removeRelatorSubsetTietzeEquiv hD).symm.toScript
111def removeRelatorSubsetRelatorEquivalentInverse
112 {R D : Set (FreeGroup X)}
113 (hD : ∀ d ∈ D, d ∈ R → RelatorEquivalent (R \ D) d 1) :
114 TietzeScript (Presentation.ofRelators (R \ D))
115 (Presentation.ofRelators R) :=
116 (Presented.removeRelatorSubsetRelatorEquivalentTietzeEquiv hD).symm.toScript
118def replaceRelatorSubset
119 {R D E : Set (FreeGroup X)}
120 (hD :
121 ∀ d ∈ D, d ∈ R → d ∈ Subgroup.normalClosure ((R \ D) ∪ E))
122 (hE : E ⊆ Subgroup.normalClosure R) :
123 TietzeScript (Presentation.ofRelators R)
124 (Presentation.ofRelators ((R \ D) ∪ E)) :=
127def replaceRelatorSubsetRelatorEquivalent
128 {R D E : Set (FreeGroup X)}
129 (hD :
130 ∀ d ∈ D, d ∈ R → RelatorEquivalent ((R \ D) ∪ E) d 1)
131 (hE : ∀ e ∈ E, RelatorEquivalent R e 1) :
132 TietzeScript (Presentation.ofRelators R)
133 (Presentation.ofRelators ((R \ D) ∪ E)) :=
136def renameGenerators
137 (R : Set (FreeGroup X)) (e : X ≃ Y) :
138 TietzeScript (Presentation.ofRelators R)
139 (Presentation.ofRelators (FreeGroup.freeGroupCongr e '' R)) :=
142def ofGeneratorMaps
143 {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
144 (toGenerator : X → FreeGroup Y)
145 (invGenerator : Y → FreeGroup X)
146 (hR :
147 ∀ r ∈ R,
148 FreeGroup.lift toGenerator r ∈ Subgroup.normalClosure S)
149 (hS :
150 ∀ s ∈ S,
151 FreeGroup.lift invGenerator s ∈ Subgroup.normalClosure R)
152 (hinv_to :
153 ∀ x : X,
155 (FreeGroup.lift invGenerator (toGenerator x))
156 (FreeGroup.of x))
157 (hto_inv :
158 ∀ y : Y,
160 (FreeGroup.lift toGenerator (invGenerator y))
161 (FreeGroup.of y)) :
162 TietzeScript (Presentation.ofRelators R) (Presentation.ofRelators S) :=
163 (TietzeEquiv.ofGeneratorMaps
166def ofGeneratorMapsRelatorEquivalent
167 {R : Set (FreeGroup X)} {S : Set (FreeGroup Y)}
168 (toGenerator : X → FreeGroup Y)
169 (invGenerator : Y → FreeGroup X)
170 (hR :
171 ∀ r ∈ R,
172 RelatorEquivalent S (FreeGroup.lift toGenerator r) 1)
173 (hS :
174 ∀ s ∈ S,
175 RelatorEquivalent R (FreeGroup.lift invGenerator s) 1)
176 (hinv_to :
177 ∀ x : X,
179 (FreeGroup.lift invGenerator (toGenerator x))
180 (FreeGroup.of x))
181 (hto_inv :
182 ∀ y : Y,
184 (FreeGroup.lift toGenerator (invGenerator y))
185 (FreeGroup.of y)) :
186 TietzeScript (Presentation.ofRelators R) (Presentation.ofRelators S) :=
187 (TietzeEquiv.ofGeneratorMapsRelatorEquivalent
190def adjoinGenerators
191 (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
192 TietzeScript (Presentation.ofRelators R)
193 (Presentation.ofRelators (Presented.adjoinGeneratorsRelators R word)) :=
196def substituteDefinedGenerators
197 (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) :
199 (Presentation.ofRelators (Presented.relatorsWithDefinedGenerators R word))
200 (Presentation.ofRelators
201 (Presented.relatorsAfterSubstitutingDefinedGenerators R word)) :=
204def deleteTrivialGenerators
205 (R : Set (FreeGroup (Sum X Y))) :
207 (Presentation.ofRelators (Presented.relatorsWithTrivialGenerators R))
208 (Presentation.ofRelators
209 (Presented.relatorsAfterDeletingTrivialGenerators R)) :=
212def substituteDefinedGeneratorsAlongEquiv
213 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
214 (word : Y → FreeGroup X) :
216 (Presentation.ofRelators
217 (Presented.relatorsWithDefinedGeneratorsAlongEquiv R e word))
218 (Presentation.ofRelators
219 (Presented.relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv
220 R e word)) :=
223def deleteTrivialGeneratorsAlongEquiv
224 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
226 (Presentation.ofRelators
227 (Presented.relatorsWithTrivialGeneratorsAlongEquiv R e))
228 (Presentation.ofRelators
229 (Presented.relatorsAfterDeletingTrivialGeneratorsAlongEquiv R e)) :=
232def substituteDefinedGeneratorsOfPredicate
233 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]
234 (word :
235 Presented.GeneratorPartition.Deleted delete →
236 FreeGroup (Presented.GeneratorPartition.Kept delete)) :
238 (Presentation.ofRelators
239 (Presented.relatorsWithDefinedGeneratorsOfPredicate R delete word))
240 (Presentation.ofRelators
241 (Presented.relatorsAfterSubstitutingDefinedGeneratorsOfPredicate
242 R delete word)) :=
245def deleteTrivialGeneratorsOfPredicate
246 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :
248 (Presentation.ofRelators
249 (Presented.relatorsWithTrivialGeneratorsOfPredicate R delete))
250 (Presentation.ofRelators
251 (Presented.relatorsAfterDeletingTrivialGeneratorsOfPredicate
252 R delete)) :=
255end TietzeScript
257end ReidemeisterSchreier.Discrete.Presentations