ReidemeisterSchreier/Discrete/Presentations/Tietze/GeneratorAddition.lean
1import ReidemeisterSchreier.Discrete.Presentations.Tietze.RelatorReplacement
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ReidemeisterSchreier/Discrete/Presentations/Tietze/GeneratorAddition.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
27variable (X Y)
29/-- Include the old free group into the free group with a family of new
30generators. -/
31def includeAdjoinedGenerators : FreeGroup X →* FreeGroup (Sum X Y) :=
32 FreeGroup.map Sum.inl
34variable {X Y}
36/-- Eliminate every new generator `y` by sending it to `word y`. -/
37def eliminateAdjoinedGeneratorsHom (word : Y → FreeGroup X) :
38 FreeGroup (Sum X Y) →* FreeGroup X :=
39 FreeGroup.lift (fun z =>
40 match z with
41 | Sum.inl x => FreeGroup.of x
42 | Sum.inr y => word y)
44@[simp]
46 (word : Y → FreeGroup X) (x : X) :
47 eliminateAdjoinedGeneratorsHom word (FreeGroup.of (Sum.inl x)) =
48 FreeGroup.of x := by
49 simp only [eliminateAdjoinedGeneratorsHom, FreeGroup.lift_apply_of]
51@[simp]
53 (word : Y → FreeGroup X) (y : Y) :
54 eliminateAdjoinedGeneratorsHom word (FreeGroup.of (Sum.inr y)) =
55 word y := by
56 simp only [eliminateAdjoinedGeneratorsHom, FreeGroup.lift_apply_of]
59 (word : Y → FreeGroup X) :
60 (eliminateAdjoinedGeneratorsHom word).comp (includeAdjoinedGenerators X Y) =
61 MonoidHom.id (FreeGroup X) := by
62 ext x
63 simp only [includeAdjoinedGenerators, MonoidHom.coe_comp, Function.comp_apply, FreeGroup.map.of,
64 eliminateAdjoinedGeneratorsHom_inl, MonoidHom.id_apply]
66/-- Relators after adjoining generators `y : Y` and relations `y = word y`. -/
68 (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
69 Set (FreeGroup (Sum X Y)) :=
70 (includeAdjoinedGenerators X Y) '' R ∪
71 {q | ∃ y : Y,
72 q = FreeGroup.of (Sum.inr y) *
73 (includeAdjoinedGenerators X Y (word y))⁻¹}
75theorem adjoinGenerators_relation_mem
76 (R : Set (FreeGroup X)) (word : Y → FreeGroup X) (y : Y) :
77 FreeGroup.of (Sum.inr y) *
78 (includeAdjoinedGenerators X Y (word y))⁻¹ ∈
79 adjoinGeneratorsRelators R word := by
80 exact Or.inr ⟨y, rfl⟩
83 (R : Set (FreeGroup X)) (word : Y → FreeGroup X)
84 (z : FreeGroup (Sum X Y)) :
85 includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word z) *
86 z⁻¹ ∈
87 Subgroup.normalClosure (adjoinGeneratorsRelators R word) := by
88 let S : Set (FreeGroup (Sum X Y)) := adjoinGeneratorsRelators R word
89 let N : Subgroup (FreeGroup (Sum X Y)) := Subgroup.normalClosure S
90 let F : FreeGroup (Sum X Y) →* FreeGroup (Sum X Y) :=
91 (includeAdjoinedGenerators X Y).comp (eliminateAdjoinedGeneratorsHom word)
92 have hhom : (QuotientGroup.mk' N).comp F = QuotientGroup.mk' N := by
93 ext z
94 cases z with
95 | inl x =>
96 simp only [includeAdjoinedGenerators, MonoidHom.coe_comp, QuotientGroup.coe_mk', Function.comp_apply,
97 eliminateAdjoinedGeneratorsHom_inl, FreeGroup.map.of, QuotientGroup.mk'_apply, N, F]
98 | inr y =>
99 simp only [MonoidHom.comp_apply, F, eliminateAdjoinedGeneratorsHom,
100 FreeGroup.lift_apply_of]
101 change ((includeAdjoinedGenerators X Y (word y) : FreeGroup (Sum X Y)) :
102 FreeGroup (Sum X Y) ⧸ N) =
103 ((FreeGroup.of (Sum.inr y) : FreeGroup (Sum X Y)) :
104 FreeGroup (Sum X Y) ⧸ N)
105 apply (QuotientGroup.eq_iff_div_mem
106 (N := N)
107 (x := includeAdjoinedGenerators X Y (word y))
108 (y := FreeGroup.of (Sum.inr y))).2
109 have hrel :
110 FreeGroup.of (Sum.inr y) *
111 (includeAdjoinedGenerators X Y (word y))⁻¹ ∈ N :=
112 Subgroup.subset_normalClosure
113 (adjoinGenerators_relation_mem R word y)
114 have hinv :
115 (FreeGroup.of (Sum.inr y) *
116 (includeAdjoinedGenerators X Y (word y))⁻¹)⁻¹ ∈ N :=
117 N.inv_mem hrel
118 simpa [N, div_eq_mul_inv, mul_assoc] using hinv
119 have hz := congrArg (fun f : FreeGroup (Sum X Y) →*
120 FreeGroup (Sum X Y) ⧸ N => f z) hhom
121 change (includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word z) :
122 FreeGroup (Sum X Y) ⧸ N) = z at hz
123 exact (QuotientGroup.eq_iff_div_mem
124 (N := N)
125 (x := includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word z))
126 (y := z)).1 hz
129 (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
130 RelatorQuotientMutualMapData R (adjoinGeneratorsRelators R word) where
131 toHom := includeAdjoinedGenerators X Y
132 invHom := eliminateAdjoinedGeneratorsHom word
133 mapsRelators := by
134 intro r hr
135 exact Subgroup.subset_normalClosure (Or.inl ⟨r, hr, rfl⟩)
136 mapsTargetRelators := by
137 intro s hs
138 rcases hs with hs | hs
139 · rcases hs with ⟨r, hr, rfl⟩
140 have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f r)
142 have hrw :
143 eliminateAdjoinedGeneratorsHom word (includeAdjoinedGenerators X Y r) = r := by
144 simpa using hcomp
145 simpa [hrw] using (Subgroup.subset_normalClosure hr :
146 r ∈ Subgroup.normalClosure R)
147 · rcases hs with ⟨y, rfl⟩
148 have hw :
150 (includeAdjoinedGenerators X Y (word y)) = word y := by
151 have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f (word y))
153 simpa using hcomp
154 simp only [map_mul, map_inv, eliminateAdjoinedGeneratorsHom_inr]
155 change word y *
157 (includeAdjoinedGenerators X Y (word y)))⁻¹ ∈
158 Subgroup.normalClosure R
159 simp only [hw, mul_inv_cancel, one_mem]
160 inv_toHom := by
161 intro x
162 have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f x)
164 have hx :
165 eliminateAdjoinedGeneratorsHom word (includeAdjoinedGenerators X Y x) = x := by
166 simpa using hcomp
167 simp only [hx, mul_inv_cancel, one_mem]
168 to_invHom := by
169 intro z
170 exact include_eliminateAdjoinedGeneratorsHom_mod_relators R word z
173 (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
174 TietzeEquiv R (adjoinGeneratorsRelators R word) :=
175 TietzeEquiv.ofMutualMapData (adjoinGeneratorsMutualMapData R word)
177/-- Tietze move: add a family of generators `y : Y` with relations
178`y = word y`. -/
179noncomputable def adjoinGenerators
180 (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
181 PresentedGroup R ≃*
182 PresentedGroup (adjoinGeneratorsRelators R word) :=
183 (adjoinGeneratorsTietzeEquiv R word).presentedEquiv
185section SubstituteDefinedGenerators
187/-- Relations `y = word y` for generators that will be eliminated from an
188arbitrary presentation over `X ⊕ Y`. -/
190 (word : Y → FreeGroup X) :
191 Set (FreeGroup (Sum X Y)) :=
192 {q | ∃ y : Y,
193 q = FreeGroup.of (Sum.inr y) *
194 (includeAdjoinedGenerators X Y (word y))⁻¹}
196/-- Add defining relations `y = word y` to an arbitrary presentation over
197`X ⊕ Y`. Unlike `adjoinGeneratorsRelators`, the old relators may already
198involve the `Y` generators. -/
200 (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) :
201 Set (FreeGroup (Sum X Y)) :=
202 R ∪ definedGeneratorRelators word
204/-- Relators after substituting every `y : Y` by `word y`. -/
206 (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) :
207 Set (FreeGroup X) :=
208 eliminateAdjoinedGeneratorsHom word '' R
210theorem definedGeneratorRelator_mem
211 (word : Y → FreeGroup X) (y : Y) :
212 FreeGroup.of (Sum.inr y) *
213 (includeAdjoinedGenerators X Y (word y))⁻¹ ∈
214 definedGeneratorRelators word :=
215 ⟨y, rfl⟩
218 (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) (y : Y) :
219 FreeGroup.of (Sum.inr y) *
220 (includeAdjoinedGenerators X Y (word y))⁻¹ ∈
221 relatorsWithDefinedGenerators R word :=
222 Or.inr (definedGeneratorRelator_mem word y)
225 {R : Set (FreeGroup (Sum X Y))} {word : Y → FreeGroup X}
226 {r : FreeGroup (Sum X Y)} (hr : r ∈ R) :
227 r ∈ relatorsWithDefinedGenerators R word :=
228 Or.inl hr
231 (word : Y → FreeGroup X) (z : FreeGroup (Sum X Y)) :
232 includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word z) *
233 z⁻¹ ∈
234 Subgroup.normalClosure (definedGeneratorRelators word) := by
235 let S : Set (FreeGroup (Sum X Y)) := definedGeneratorRelators word
236 let N : Subgroup (FreeGroup (Sum X Y)) := Subgroup.normalClosure S
237 let F : FreeGroup (Sum X Y) →* FreeGroup (Sum X Y) :=
238 (includeAdjoinedGenerators X Y).comp (eliminateAdjoinedGeneratorsHom word)
239 have hhom : (QuotientGroup.mk' N).comp F = QuotientGroup.mk' N := by
240 ext z
241 cases z with
242 | inl x =>
243 simp only [includeAdjoinedGenerators, MonoidHom.coe_comp, QuotientGroup.coe_mk', Function.comp_apply,
244 eliminateAdjoinedGeneratorsHom_inl, FreeGroup.map.of, QuotientGroup.mk'_apply, N, F]
245 | inr y =>
246 simp only [MonoidHom.comp_apply, F, eliminateAdjoinedGeneratorsHom,
247 FreeGroup.lift_apply_of]
248 change ((includeAdjoinedGenerators X Y (word y) : FreeGroup (Sum X Y)) :
249 FreeGroup (Sum X Y) ⧸ N) =
250 ((FreeGroup.of (Sum.inr y) : FreeGroup (Sum X Y)) :
251 FreeGroup (Sum X Y) ⧸ N)
252 apply (QuotientGroup.eq_iff_div_mem
253 (N := N)
254 (x := includeAdjoinedGenerators X Y (word y))
255 (y := FreeGroup.of (Sum.inr y))).2
256 have hrel :
257 FreeGroup.of (Sum.inr y) *
258 (includeAdjoinedGenerators X Y (word y))⁻¹ ∈ N :=
259 Subgroup.subset_normalClosure
260 (definedGeneratorRelator_mem word y)
261 have hinv :
262 (FreeGroup.of (Sum.inr y) *
263 (includeAdjoinedGenerators X Y (word y))⁻¹)⁻¹ ∈ N :=
264 N.inv_mem hrel
265 simpa [N, div_eq_mul_inv, mul_assoc] using hinv
266 have hz := congrArg (fun f : FreeGroup (Sum X Y) →*
267 FreeGroup (Sum X Y) ⧸ N => f z) hhom
268 change (includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word z) :
269 FreeGroup (Sum X Y) ⧸ N) = z at hz
270 exact (QuotientGroup.eq_iff_div_mem
271 (N := N)
272 (x := includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word z))
273 (y := z)).1 hz
276 (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X)
277 (z : FreeGroup (Sum X Y)) :
278 includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word z) *
279 z⁻¹ ∈
280 Subgroup.normalClosure (relatorsWithDefinedGenerators R word) :=
281 Subgroup.normalClosure_mono
282 (fun _ hq => Or.inr hq)
284 (X := X) (Y := Y) word z)
287 (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) :
289 (relatorsWithDefinedGenerators R word)
290 (relatorsAfterSubstitutingDefinedGenerators R word) where
291 toHom := eliminateAdjoinedGeneratorsHom word
292 invHom := includeAdjoinedGenerators X Y
293 mapsRelators := by
294 intro r hr
295 rcases hr with hr | hr
296 · exact Subgroup.subset_normalClosure ⟨r, hr, rfl⟩
297 · rcases hr with ⟨y, rfl⟩
298 have hw :
300 (includeAdjoinedGenerators X Y (word y)) = word y := by
301 have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f (word y))
303 simpa using hcomp
304 simp only [map_mul, map_inv, eliminateAdjoinedGeneratorsHom_inr]
305 change word y *
307 (includeAdjoinedGenerators X Y (word y)))⁻¹ ∈
308 Subgroup.normalClosure (relatorsAfterSubstitutingDefinedGenerators R word)
309 simp only [hw, mul_inv_cancel, one_mem]
310 mapsTargetRelators := by
311 intro s hs
312 rcases hs with ⟨r, hr, rfl⟩
313 let N : Subgroup (FreeGroup (Sum X Y)) :=
314 Subgroup.normalClosure (relatorsWithDefinedGenerators R word)
315 have hmod :
316 includeAdjoinedGenerators X Y (eliminateAdjoinedGeneratorsHom word r) *
317 r⁻¹ ∈ N :=
319 (X := X) (Y := Y) R word r
320 have hrN : r ∈ N :=
321 Subgroup.subset_normalClosure
322 (relator_mem_relatorsWithDefinedGenerators (R := R) (word := word) hr)
323 have hprod := Subgroup.mul_mem N hmod hrN
324 convert hprod using 1
325 group
326 inv_toHom := by
327 intro z
329 (X := X) (Y := Y) R word z
330 to_invHom := by
331 intro z
332 have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f z)
334 have hz :
335 eliminateAdjoinedGeneratorsHom word (includeAdjoinedGenerators X Y z) = z := by
336 simpa using hcomp
337 simp only [hz, mul_inv_cancel, one_mem]
340 (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) :
342 (relatorsWithDefinedGenerators R word)
343 (relatorsAfterSubstitutingDefinedGenerators R word) :=
344 TietzeEquiv.ofMutualMapData
347/-- Tietze move eliminating generators `y : Y` using relations `y = word y`,
348while substituting `word y` into all remaining relators. -/
349noncomputable def substituteDefinedGenerators
350 (R : Set (FreeGroup (Sum X Y))) (word : Y → FreeGroup X) :
351 PresentedGroup (relatorsWithDefinedGenerators R word) ≃*
352 PresentedGroup (relatorsAfterSubstitutingDefinedGenerators R word) :=
353 (substituteDefinedGeneratorsTietzeEquiv R word).presentedEquiv
355end SubstituteDefinedGenerators
357end AdjoinGenerators
359end Presented
361end ReidemeisterSchreier.Discrete.Presentations