Yamaguchi Lean 4 Library
ReidemeisterSchreier/Discrete/Presentations/Relators.lean
ReidemeisterSchreier/Discrete/Presentations/Relators/Source

ReidemeisterSchreier/Discrete/Presentations/Relators.lean

1import Mathlib.GroupTheory.FreeGroup.Reduce
2import Mathlib.Tactic.NormNum.LegendreSymbol
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ReidemeisterSchreier/Discrete/Presentations/Relators.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Relators modulo normal closure
15This file contains the elementary discrete API for working modulo the normal
16closure of a relator set. It is independent of the project libraries outside
17mathlib.
19`RelatorEquivalent R u v` means that `u * v⁻¹` lies in
20`Subgroup.normalClosure R`. Equivalently, `u` and `v` define the same element in
21the quotient by that normal closure. In presentation proofs, do relator
22calculations with `RelatorEquivalent` first, use the paired normal-closure
23membership lemmas when needed, and convert to quotient equality only at the
24boundary.
25-/
27namespace ReidemeisterSchreier.Discrete.Presentations
29variable {G H : Type*} [Group G] [Group H]
31/-- Equality modulo the normal closure generated by `R`. -/
32def RelatorEquivalent (R : Set G) (u v : G) : Prop :=
33 u * v⁻¹ ∈ Subgroup.normalClosure R
35theorem relatorEquivalent_iff_eq_in_presentedQuotient {R : Set G} {u v : G} :
37 ((u : G ⧸ Subgroup.normalClosure R) =
38 (v : G ⧸ Subgroup.normalClosure R)) := by
39 simpa [RelatorEquivalent, div_eq_mul_inv] using
40 (QuotientGroup.eq_iff_div_mem
41 (N := Subgroup.normalClosure R) (x := u) (y := v)).symm
43@[simp] theorem relatorEquivalent_one_right {R : Set G} {u : G} :
44 RelatorEquivalent R u 1 ↔ u ∈ Subgroup.normalClosure R := by
45 simp only [RelatorEquivalent, inv_one, mul_one]
47@[simp] theorem relatorEquivalent_one_left {R : Set G} {u : G} :
48 RelatorEquivalent R 1 u ↔ u ∈ Subgroup.normalClosure R := by
49 constructor
50 · intro h
51 have huInv : u⁻¹ ∈ Subgroup.normalClosure R := by
52 simpa [RelatorEquivalent] using h
53 simpa using Subgroup.inv_mem (Subgroup.normalClosure R) huInv
54 · intro h
55 have huInv : u⁻¹ ∈ Subgroup.normalClosure R :=
56 Subgroup.inv_mem (Subgroup.normalClosure R) h
57 simpa [RelatorEquivalent] using huInv
59def relatorEquivalentSetoid (R : Set G) : Setoid G where
61 iseqv := by
62 refine ⟨?_, ?_, ?_⟩
63 · intro u
65 · intro u v h
67 exact h.symm
68 · intro u v w huv hvw
70 exact huv.trans hvw
74variable {R S : Set G} {u v w a b r : G}
76@[refl]
77theorem refl (R : Set G) (u : G) : RelatorEquivalent R u u := by
80theorem of_eq (h : u = v) : RelatorEquivalent R u v := by
81 rw [h]
83theorem symm (h : RelatorEquivalent R u v) : RelatorEquivalent R v u := by
85 exact h.symm
87theorem trans (h₁ : RelatorEquivalent R u v) (h₂ : RelatorEquivalent R v w) : RelatorEquivalent R u w := by
89 exact h₁.trans h₂
91theorem inv (h : RelatorEquivalent R u v) : RelatorEquivalent R u⁻¹ v⁻¹ := by
93 simpa using congrArg Inv.inv h
95theorem mul (h₁ : RelatorEquivalent R u v) (h₂ : RelatorEquivalent R a b) :
96 RelatorEquivalent R (u * a) (v * b) := by
98 calc
99 ((u * a : G) : G ⧸ Subgroup.normalClosure R) =
100 (u : G ⧸ Subgroup.normalClosure R) * (a : G ⧸ Subgroup.normalClosure R) := rfl
101 _ = (v : G ⧸ Subgroup.normalClosure R) * (b : G ⧸ Subgroup.normalClosure R) := by
102 rw [h₁, h₂]
103 _ = ((v * b : G) : G ⧸ Subgroup.normalClosure R) := rfl
105theorem pow (h : RelatorEquivalent R u v) (n : ℕ) : RelatorEquivalent R (u ^ n) (v ^ n) := by
107 simpa using congrArg (fun z : G ⧸ Subgroup.normalClosure R => z ^ n) h
109theorem zpow (h : RelatorEquivalent R u v) (n : ℤ) : RelatorEquivalent R (u ^ n) (v ^ n) := by
111 simpa using congrArg (fun z : G ⧸ Subgroup.normalClosure R => z ^ n) h
113theorem mul_eq_one (h₁ : RelatorEquivalent R u 1) (h₂ : RelatorEquivalent R v 1) :
114 RelatorEquivalent R (u * v) 1 := by
115 simpa using mul h₁ h₂
117theorem pow_eq_one (h : RelatorEquivalent R u 1) (n : ℕ) :
118 RelatorEquivalent R (u ^ n) 1 := by
119 simpa using pow h n
121theorem zpow_eq_one (h : RelatorEquivalent R u 1) (n : ℤ) :
122 RelatorEquivalent R (u ^ n) 1 := by
123 simpa using zpow h n
125theorem inv_eq_one (h : RelatorEquivalent R u 1) :
126 RelatorEquivalent R u⁻¹ 1 := by
127 simpa using inv h
129theorem conjugate_pow_eq (a u : G) (n : ℕ) :
130 (a * u * a⁻¹) ^ n = a * u ^ n * a⁻¹ := by
131 induction n with
132 | zero =>
133 simp only [pow_zero, mul_one, mul_inv_cancel]
134 | succ n ih =>
135 calc
136 (a * u * a⁻¹) ^ (n + 1) =
137 a * u ^ n * a⁻¹ * (a * u * a⁻¹) := by
138 rw [pow_succ, ih]
139 _ = a * (u ^ n * u) * a⁻¹ := by
140 simp only [mul_assoc, inv_mul_cancel_left]
141 _ = a * u ^ (n + 1) * a⁻¹ := by
142 rw [pow_succ]
145 RelatorEquivalent R (u * v) 1 ↔ RelatorEquivalent R u v⁻¹ := by
146 constructor
147 · intro h
148 simpa only [RelatorEquivalent, inv_inv, inv_one, mul_one] using h
149 · intro h
150 simpa only [RelatorEquivalent, inv_inv, inv_one, mul_one] using h
152theorem eq_inv_of_mul_eq_one (h : RelatorEquivalent R (u * v) 1) :
153 RelatorEquivalent R u v⁻¹ :=
154 mul_eq_one_iff_eq_inv.1 h
156theorem mul_eq_one_of_eq_inv (h : RelatorEquivalent R u v⁻¹) :
157 RelatorEquivalent R (u * v) 1 :=
158 mul_eq_one_iff_eq_inv.2 h
161 (hu : RelatorEquivalent R u 1)
162 (huv : RelatorEquivalent R (u * v) 1) :
165 calc
166 (v : G ⧸ Subgroup.normalClosure R) =
167 (1 : G ⧸ Subgroup.normalClosure R) * v := by simp only [one_mul]
168 _ = (u : G ⧸ Subgroup.normalClosure R) * v := by
169 simpa using congrArg
170 (fun z : G ⧸ Subgroup.normalClosure R =>
171 z * (v : G ⧸ Subgroup.normalClosure R)) hu.symm
172 _ = ((u * v : G) : G ⧸ Subgroup.normalClosure R) := rfl
173 _ = 1 := huv
176 (huv : RelatorEquivalent R (u * v) 1)
177 (hv : RelatorEquivalent R v 1) :
180 calc
181 (u : G ⧸ Subgroup.normalClosure R) =
182 (u : G ⧸ Subgroup.normalClosure R) * 1 := by simp only [mul_one]
183 _ = (u : G ⧸ Subgroup.normalClosure R) * v := by
184 simpa using congrArg
185 (fun z : G ⧸ Subgroup.normalClosure R =>
186 (u : G ⧸ Subgroup.normalClosure R) * z) hv.symm
187 _ = ((u * v : G) : G ⧸ Subgroup.normalClosure R) := rfl
188 _ = 1 := huv
190theorem mul_left (h : RelatorEquivalent R u v) (a : G) : RelatorEquivalent R (a * u) (a * v) :=
191 mul (refl R a) h
193theorem mul_right (h : RelatorEquivalent R u v) (a : G) : RelatorEquivalent R (u * a) (v * a) :=
194 mul h (refl R a)
196/-- Replace a subword inside a two-sided context. -/
197theorem context (h : RelatorEquivalent R u v) (a b : G) :
198 RelatorEquivalent R (a * u * b) (a * v * b) :=
199 mul_right (mul_left h a) b
201theorem conj (h : RelatorEquivalent R u v) (a : G) :
202 RelatorEquivalent R (a * u * a⁻¹) (a * v * a⁻¹) :=
203 context h a a⁻¹
205theorem conj_eq_one (h : RelatorEquivalent R u 1) (a : G) :
206 RelatorEquivalent R (a * u * a⁻¹) 1 := by
207 simpa using conj h a
210 {n : ℕ} (h : RelatorEquivalent R (u ^ n) 1) (a : G) :
211 RelatorEquivalent R ((a * u * a⁻¹) ^ n) 1 := by
212 simpa [conjugate_pow_eq] using conj_eq_one h a
214theorem of_mem (hr : r ∈ R) : RelatorEquivalent R r 1 := by
215 simpa [RelatorEquivalent] using (Subgroup.subset_normalClosure hr :
216 r ∈ Subgroup.normalClosure R)
218theorem of_mem_normalClosure (hr : r ∈ Subgroup.normalClosure R) :
220 simpa [RelatorEquivalent] using hr
222theorem mono (hR_to_S : R ⊆ S) (h : RelatorEquivalent R u v) :
224 have hx : u * v⁻¹ ∈ Subgroup.normalClosure S :=
225 Subgroup.normalClosure_mono hR_to_S
226 (by simpa [RelatorEquivalent] using h)
227 simpa [RelatorEquivalent] using hx
229theorem mono_iUnion {ι : Sort*} (R : ι → Set G)
230 (i : ι) (h : RelatorEquivalent (R i) u v) :
231 RelatorEquivalent (Set.iUnion R) u v :=
232 mono (R := R i) (S := Set.iUnion R)
233 (fun _ hx => Set.mem_iUnion.2 ⟨i, hx⟩) h
235theorem mono_iUnion₂ {ι : Sort*} {κ : ι → Sort*}
236 (R : ∀ i : ι, κ i → Set G)
237 (i : ι) (j : κ i) (h : RelatorEquivalent (R i j) u v) :
238 RelatorEquivalent (Set.iUnion fun i : ι => Set.iUnion (R i)) u v :=
239 mono (R := R i j) (S := Set.iUnion fun i : ι => Set.iUnion (R i))
240 (fun _ hx => Set.mem_iUnion.2 ⟨i, Set.mem_iUnion.2 ⟨j, hx⟩⟩) h
243 r ∈ Subgroup.normalClosure R := by
244 simpa [RelatorEquivalent] using h
247 u * v⁻¹ ∈ Subgroup.normalClosure R := by
248 simpa [RelatorEquivalent] using h
251 u / v ∈ Subgroup.normalClosure R := by
252 simpa [div_eq_mul_inv] using h.mul_inv_mem_normalClosure
254theorem mul_inv_eq_one (h : RelatorEquivalent R u v) :
255 RelatorEquivalent R (u * v⁻¹) 1 :=
256 of_mem_normalClosure h.mul_inv_mem_normalClosure
258theorem div_eq_one (h : RelatorEquivalent R u v) :
259 RelatorEquivalent R (u / v) 1 := by
260 simpa [div_eq_mul_inv] using h.mul_inv_eq_one
262theorem one_eq_of_mem_inv (hr : r ∈ R) : RelatorEquivalent R 1 r :=
263 (of_mem hr).symm
267section NormalClosure
269variable {R S : Set G} {r a b : G}
272 (hR_to_S : R ⊆ S) {x : G}
273 (hx : x ∈ Subgroup.normalClosure R) :
274 x ∈ Subgroup.normalClosure S :=
275 Subgroup.normalClosure_mono hR_to_S hx
278 {x : G} (hx : x ∈ Subgroup.normalClosure R) :
279 x ∈ Subgroup.normalClosure (R ∪ S) :=
280 mem_normalClosure_of_subset (R := R) (S := R ∪ S)
281 (Set.subset_union_left) hx
284 {x : G} (hx : x ∈ Subgroup.normalClosure S) :
285 x ∈ Subgroup.normalClosure (R ∪ S) :=
286 mem_normalClosure_of_subset (R := S) (S := R ∪ S)
287 (Set.subset_union_right) hx
290 {ι : Sort*} (R : ι → Set G) (i : ι)
291 {x : G} (hx : x ∈ Subgroup.normalClosure (R i)) :
292 x ∈ Subgroup.normalClosure (Set.iUnion R) :=
293 mem_normalClosure_of_subset (R := R i) (S := Set.iUnion R)
294 (fun _ hy => Set.mem_iUnion.2 ⟨i, hy⟩) hx
297 {ι : Sort*} {κ : ι → Sort*}
298 (R : ∀ i : ι, κ i → Set G) (i : ι) (j : κ i)
299 {x : G} (hx : x ∈ Subgroup.normalClosure (R i j)) :
300 x ∈ Subgroup.normalClosure
301 (Set.iUnion fun i : ι => Set.iUnion (R i)) :=
303 (R := R i j)
304 (S := Set.iUnion fun i : ι => Set.iUnion (R i))
305 (fun _ hy => Set.mem_iUnion.2 ⟨i, Set.mem_iUnion.2 ⟨j, hy⟩⟩) hx
308 {ι : Sort*} {κ : ι → Sort*}
309 (R : ∀ i : ι, κ i → Set G)
310 {x : G} (hx : ∃ i : ι, ∃ j : κ i,
311 x ∈ Subgroup.normalClosure (R i j)) :
312 x ∈ Subgroup.normalClosure
313 (Set.iUnion fun i : ι => Set.iUnion (R i)) := by
314 rcases hx with ⟨i, j, hij⟩
315 exact mem_normalClosure_iUnion₂ (R := R) i j hij
318 {ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
319 (hR : ∀ i : ι, ∀ r ∈ R i, f r ∈ Subgroup.normalClosure S) :
320 ∀ r ∈ Set.iUnion R, f r ∈ Subgroup.normalClosure S := by
321 intro r hr
322 rcases Set.mem_iUnion.1 hr with ⟨i, hi⟩
323 exact hR i r hi
326 {ι : Sort*} {κ : ι → Sort*}
327 (f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
328 (hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
329 f r ∈ Subgroup.normalClosure S) :
330 ∀ r ∈ Set.iUnion (fun i : ι => Set.iUnion (R i)),
331 f r ∈ Subgroup.normalClosure S := by
332 intro r hr
333 rcases Set.mem_iUnion.1 hr with ⟨i, hi⟩
334 rcases Set.mem_iUnion.1 hi with ⟨j, hj⟩
335 exact hR i j r hj
338 (f : G →* H) {R : Set G} {S : Set H}
339 (hR : ∀ r ∈ R, f r ∈ Subgroup.normalClosure S)
340 {x : G} (hx : x ∈ Subgroup.normalClosure R) :
341 f x ∈ Subgroup.normalClosure S := by
342 let N : Subgroup G := Subgroup.comap f (Subgroup.normalClosure S)
343 have hle : Subgroup.normalClosure R ≤ N := by
344 refine Subgroup.normalClosure_le_normal ?_
345 intro r hr
346 exact hR r hr
347 exact hle hx
350 (f : G →* H) {R : Set G} {S : Set H}
351 (hR : ∀ r ∈ R, f r ∈ Subgroup.normalClosure S)
352 {u v : G} (h : RelatorEquivalent R u v) :
353 RelatorEquivalent S (f u) (f v) := by
354 have hx :
355 f (u * v⁻¹) ∈ Subgroup.normalClosure S :=
357 simpa [RelatorEquivalent, map_mul] using hx
360 (f : G →* H) {R : Set G} {S : Set H}
361 (hR : ∀ r ∈ R, RelatorEquivalent S (f r) 1)
362 {u v : G} (h : RelatorEquivalent R u v) :
363 RelatorEquivalent S (f u) (f v) :=
365 (fun r hr => RelatorEquivalent.mem_normalClosure_of_eq_one (hR r hr)) h
368 {ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
369 (hR : ∀ i : ι, ∀ r ∈ R i, f r ∈ Subgroup.normalClosure S)
370 {x : G} (hx : x ∈ Subgroup.normalClosure (Set.iUnion R)) :
371 f x ∈ Subgroup.normalClosure S :=
376 {ι : Sort*} {κ : ι → Sort*}
377 (f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
378 (hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
379 f r ∈ Subgroup.normalClosure S)
380 {x : G}
381 (hx : x ∈ Subgroup.normalClosure
382 (Set.iUnion fun i : ι => Set.iUnion (R i))) :
383 f x ∈ Subgroup.normalClosure S :=
388 {ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
389 (hR : ∀ i : ι, ∀ r ∈ R i, f r ∈ Subgroup.normalClosure S)
390 {u v : G} (h : RelatorEquivalent (Set.iUnion R) u v) :
391 RelatorEquivalent S (f u) (f v) :=
396 {ι : Sort*} (f : G →* H) {R : ι → Set G} {S : Set H}
397 (hR : ∀ i : ι, ∀ r ∈ R i, RelatorEquivalent S (f r) 1)
398 {u v : G} (h : RelatorEquivalent (Set.iUnion R) u v) :
399 RelatorEquivalent S (f u) (f v) :=
401 (fun i r hr => RelatorEquivalent.mem_normalClosure_of_eq_one (hR i r hr)) h
404 {ι : Sort*} {κ : ι → Sort*}
405 (f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
406 (hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
407 f r ∈ Subgroup.normalClosure S)
408 {u v : G}
410 (Set.iUnion fun i : ι => Set.iUnion (R i)) u v) :
411 RelatorEquivalent S (f u) (f v) :=
416 {ι : Sort*} {κ : ι → Sort*}
417 (f : G →* H) {R : ∀ i : ι, κ i → Set G} {S : Set H}
418 (hR : ∀ i : ι, ∀ j : κ i, ∀ r ∈ R i j,
420 {u v : G}
422 (Set.iUnion fun i : ι => Set.iUnion (R i)) u v) :
423 RelatorEquivalent S (f u) (f v) :=
425 (fun i j r hr => RelatorEquivalent.mem_normalClosure_of_eq_one (hR i j r hr)) h
427section FreeGroupLift
429variable {X : Type*}
432 [DecidableEq X]
433 {R : Set (FreeGroup X)} {u : FreeGroup X} {w : List (X × Bool)}
434 (h : u.toWord = FreeGroup.reduce w) :
435 RelatorEquivalent R u (FreeGroup.mk w) := by
436 apply RelatorEquivalent.of_eq
437 rw [← FreeGroup.toWord_inj]
438 simp only [h, FreeGroup.toWord_mk]
441 [DecidableEq X]
442 {R : Set (FreeGroup X)} {u : FreeGroup X} {w : List (X × Bool)}
443 (h : FreeGroup.reduce w = u.toWord) :
444 RelatorEquivalent R (FreeGroup.mk w) u :=
446 (R := R) (u := u) (w := w) h.symm).symm
448def freeGroupSubstitutionWord {Y : Type*} [DecidableEq Y]
449 (f : X → FreeGroup Y) :
450 List (X × Bool) → List (Y × Bool)
451 | [] => []
452 | (x, true) :: xs => (f x).toWord ++ freeGroupSubstitutionWord f xs
453 | (x, false) :: xs => FreeGroup.invRev (f x).toWord ++ freeGroupSubstitutionWord f xs
455@[simp]
456theorem freeGroupSubstitutionWord_nil {Y : Type*} [DecidableEq Y]
457 (f : X → FreeGroup Y) :
459 rfl
461@[simp]
462theorem freeGroupSubstitutionWord_cons_true {Y : Type*} [DecidableEq Y]
463 (f : X → FreeGroup Y) (x : X) (xs : List (X × Bool)) :
464 freeGroupSubstitutionWord f ((x, true) :: xs) =
465 (f x).toWord ++ freeGroupSubstitutionWord f xs :=
466 rfl
468@[simp]
469theorem freeGroupSubstitutionWord_cons_false {Y : Type*} [DecidableEq Y]
470 (f : X → FreeGroup Y) (x : X) (xs : List (X × Bool)) :
471 freeGroupSubstitutionWord f ((x, false) :: xs) =
472 FreeGroup.invRev (f x).toWord ++ freeGroupSubstitutionWord f xs :=
473 rfl
475theorem freeGroupSubstitutionWord_append {Y : Type*} [DecidableEq Y]
476 (f : X → FreeGroup Y) (xs ys : List (X × Bool)) :
479 induction xs with
480 | nil => simp
481 | cons xb xs ih =>
482 rcases xb with ⟨x, b⟩
483 cases b
484 · simp only [List.cons_append, freeGroupSubstitutionWord_cons_false, ih, List.append_assoc]
485 · simp only [List.cons_append, freeGroupSubstitutionWord_cons_true, ih, List.append_assoc]
487theorem freeGroup_mk_substitutionWord {Y : Type*} [DecidableEq Y]
488 (f : X → FreeGroup Y) (xs : List (X × Bool)) :
489 FreeGroup.mk (freeGroupSubstitutionWord f xs) =
490 FreeGroup.lift f (FreeGroup.mk xs) := by
491 induction xs with
492 | nil => exact FreeGroup.one_eq_mk.symm
493 | cons xb xs ih =>
494 rcases xb with ⟨x, b⟩
495 cases b
496 · rw [freeGroupSubstitutionWord_cons_false, ← FreeGroup.mul_mk,
497 ← FreeGroup.inv_mk, FreeGroup.mk_toWord, ih]
498 simp only [FreeGroup.lift_mk, List.map_cons, cond_false, List.prod_cons]
499 · rw [freeGroupSubstitutionWord_cons_true, ← FreeGroup.mul_mk,
500 FreeGroup.mk_toWord, ih]
501 simp only [FreeGroup.lift_mk, List.map_cons, cond_true, List.prod_cons]
503theorem freeGroup_toWord_lift_mk {Y : Type*} [DecidableEq Y]
504 (f : X → FreeGroup Y) (xs : List (X × Bool)) :
505 (FreeGroup.lift f (FreeGroup.mk xs)).toWord =
506 FreeGroup.reduce (freeGroupSubstitutionWord f xs) := by
507 rw [← freeGroup_mk_substitutionWord (f := f) (xs := xs)]
508 simp only [FreeGroup.toWord_mk]
511 {Y : Type*} [DecidableEq Y]
512 {f : X → FreeGroup Y} {xs : List (X × Bool)}
513 {ys : List (Y × Bool)}
514 (h :
515 FreeGroup.reduce (freeGroupSubstitutionWord f xs) =
516 FreeGroup.reduce ys) :
517 FreeGroup.lift f (FreeGroup.mk xs) = FreeGroup.mk ys := by
518 rw [← FreeGroup.toWord_inj]
519 rw [freeGroup_toWord_lift_mk, FreeGroup.toWord_mk, h]
522 {Y : Type*} [DecidableEq Y]
523 {R : Set (FreeGroup Y)}
524 {f : X → FreeGroup Y} {xs : List (X × Bool)}
525 {ys : List (Y × Bool)}
526 (h :
527 FreeGroup.reduce (freeGroupSubstitutionWord f xs) =
528 FreeGroup.reduce ys) :
529 RelatorEquivalent R (FreeGroup.lift f (FreeGroup.mk xs))
530 (FreeGroup.mk ys) :=
531 RelatorEquivalent.of_eq
535 {Y : Type*} [DecidableEq Y]
536 {R : Set (FreeGroup Y)}
537 {f : X → FreeGroup Y} {xs : List (X × Bool)}
538 {ys : List (Y × Bool)}
539 (h :
540 FreeGroup.reduce (freeGroupSubstitutionWord f xs) =
541 FreeGroup.reduce ys)
542 (hy : RelatorEquivalent R (FreeGroup.mk ys) 1) :
543 RelatorEquivalent R (FreeGroup.lift f (FreeGroup.mk xs)) 1 :=
545 (R := R) h).trans hy
548 {R : Set G} {f g : X → G}
549 (h : ∀ x : X, RelatorEquivalent R (f x) (g x))
550 (w : FreeGroup X) :
551 RelatorEquivalent R (FreeGroup.lift f w) (FreeGroup.lift g w) := by
552 let N : Subgroup G := Subgroup.normalClosure R
553 let F : FreeGroup X →* G ⧸ N :=
554 (QuotientGroup.mk' N).comp (FreeGroup.lift f)
555 let K : FreeGroup X →* G ⧸ N :=
556 (QuotientGroup.mk' N).comp (FreeGroup.lift g)
557 have hhom : F = K := by
558 ext x
559 dsimp [F, K]
560 simp only [FreeGroup.lift_apply_of]
562 exact h x
563 have hw := congrArg (fun φ : FreeGroup X →* G ⧸ N => φ w) hhom
564 change ((FreeGroup.lift f w : G) : G ⧸ N) =
565 ((FreeGroup.lift g w : G) : G ⧸ N) at hw
566 exact relatorEquivalent_iff_eq_in_presentedQuotient.2 hw
569 {R : Set G} {f : X → G}
570 (h : ∀ x : X, RelatorEquivalent R (f x) 1)
571 (w : FreeGroup X) :
572 RelatorEquivalent R (FreeGroup.lift f w) 1 := by
573 let trivialLift : FreeGroup X →* G :=
574 FreeGroup.lift (fun _ : X => (1 : G))
575 have htrivial : trivialLift w = 1 := by
576 have hhom : trivialLift = 1 := by
577 ext x
578 simp only [FreeGroup.lift_apply_of, MonoidHom.one_apply, trivialLift]
579 exact congrArg (fun φ : FreeGroup X →* G => φ w) hhom
580 simpa [trivialLift, htrivial] using
582 (R := R) (f := f) (g := fun _ : X => (1 : G)) h w
585 {R : Set G} {f g : X → G}
586 (h : ∀ x : X, f x = g x)
587 (w : FreeGroup X) :
588 RelatorEquivalent R (FreeGroup.lift f w) (FreeGroup.lift g w) :=
590 (R := R) (f := f) (g := g)
591 (fun x => RelatorEquivalent.of_eq (h x)) w
593end FreeGroupLift
595/-- If every relator on each side is trivial modulo the other side, the normal
596closures are equal. -/
598 (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
599 (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
600 Subgroup.normalClosure R = Subgroup.normalClosure S := by
601 apply le_antisymm
602 · refine Subgroup.normalClosure_le_normal ?_
603 intro r hr
604 exact RelatorEquivalent.mem_normalClosure_of_eq_one (hR_to_S r hr)
605 · refine Subgroup.normalClosure_le_normal ?_
606 intro s hs
607 exact RelatorEquivalent.mem_normalClosure_of_eq_one (hS_to_R s hs)
610 (hr : r ∈ Subgroup.normalClosure R) :
611 Subgroup.normalClosure (insert r R) = Subgroup.normalClosure R := by
612 apply le_antisymm
613 · refine Subgroup.normalClosure_le_normal ?_
614 intro x hx
615 rcases hx with rfl | hx
616 · exact hr
617 · exact Subgroup.subset_normalClosure hx
618 · exact Subgroup.normalClosure_mono (by
619 intro x hx
620 exact Set.mem_insert_of_mem r hx)
623 (hr : r ∈ Subgroup.normalClosure (R \ {r})) :
624 Subgroup.normalClosure R = Subgroup.normalClosure (R \ {r}) := by
625 apply le_antisymm
626 · refine Subgroup.normalClosure_le_normal ?_
627 intro x hx
628 by_cases hxr : x = r
629 · simpa [hxr] using hr
630 · exact Subgroup.subset_normalClosure ⟨hx, by simpa [Set.mem_singleton_iff] using hxr⟩
631 · exact Subgroup.normalClosure_mono (by
632 intro x hx
633 exact hx.1)
636 (hR_to_S : R ⊆ Subgroup.normalClosure S)
637 (hS_to_R : S ⊆ Subgroup.normalClosure R) :
638 Subgroup.normalClosure R = Subgroup.normalClosure S := by
639 apply le_antisymm
640 · exact Subgroup.normalClosure_le_normal hR_to_S
641 · exact Subgroup.normalClosure_le_normal hS_to_R
643theorem conjugate_mem_normalClosure_of_mem
644 (hr : r ∈ R) (a : G) :
645 a * r * a⁻¹ ∈ Subgroup.normalClosure R := by
646 simpa [mul_assoc] using
647 (Subgroup.normalClosure_normal.conj_mem r
648 (Subgroup.subset_normalClosure hr) a)
651 (hr : r ∈ Subgroup.normalClosure R) (a : G) :
652 a * r * a⁻¹ ∈ Subgroup.normalClosure R := by
653 simpa [mul_assoc] using
654 (Subgroup.normalClosure_normal.conj_mem r hr a)
656/-- Cyclically rotating a relator keeps it in the same normal closure. -/
658 (h : a * b ∈ Subgroup.normalClosure R) :
659 b * a ∈ Subgroup.normalClosure R := by
660 have hc := conjugate_mem_normalClosure (R := R) h b
661 simpa [mul_assoc] using hc
664 {a b : G}
665 (ha : a ∈ Subgroup.normalClosure R)
666 (hab : a * b ∈ Subgroup.normalClosure R) :
667 b ∈ Subgroup.normalClosure R := by
668 let N : Subgroup G := Subgroup.normalClosure R
669 have h : a⁻¹ * (a * b) ∈ N := N.mul_mem (N.inv_mem ha) hab
670 simpa [N, mul_assoc] using h
673 {a b : G} {n : ℕ}
674 (h : (a * b) ^ n ∈ Subgroup.normalClosure R) :
675 (b * a) ^ n ∈ Subgroup.normalClosure R := by
676 let N : Subgroup G := Subgroup.normalClosure R
677 have hconj : b * ((a * b) ^ n) * b⁻¹ ∈ N := by
678 simpa [N, MulAut.conj_apply] using
679 (Subgroup.normalClosure_normal.conj_mem ((a * b) ^ n) h b)
680 have hpow : b * ((a * b) ^ n) * b⁻¹ = (b * a) ^ n := by
681 clear h hconj
682 induction n with
683 | zero =>
684 simp only [pow_zero, mul_one, mul_inv_cancel]
685 | succ n ih =>
686 rw [pow_succ, pow_succ, ← ih]
687 group
688 simpa [hpow] using hconj
691 {u v : G} {n : ℕ}
692 (huv : u * v⁻¹ ∈ Subgroup.normalClosure R)
693 (hv : v ^ n ∈ Subgroup.normalClosure R) :
694 u ^ n ∈ Subgroup.normalClosure R := by
695 let N : Subgroup G := Subgroup.normalClosure R
696 let q : G →* G ⧸ N := QuotientGroup.mk' N
697 have hq : q u = q v := by
698 exact
699 (QuotientGroup.eq_iff_div_mem (N := N) (x := u) (y := v)).2
700 (by simpa [N, div_eq_mul_inv] using huv)
701 have hqv : q (v ^ n) = 1 :=
702 (QuotientGroup.eq_one_iff (N := N) (v ^ n)).2 hv
703 have hqu : q (u ^ n) = 1 := by
704 rw [map_pow, hq, ← map_pow]
705 exact hqv
706 exact (QuotientGroup.eq_one_iff (N := N) (u ^ n)).1 hqu
709 {l : List G}
710 (h : ∀ x ∈ l, x ∈ Subgroup.normalClosure R) :
711 l.prod ∈ Subgroup.normalClosure R := by
712 induction l with
713 | nil =>
714 simp only [List.prod_nil, one_mem]
715 | cons x xs ih =>
716 simp only [List.mem_cons] at h
717 exact Subgroup.mul_mem (Subgroup.normalClosure R)
718 (h x (Or.inl rfl))
719 (ih (by
720 intro y hy
721 exact h y (Or.inr hy)))
724 {ι : Type*} (l : List ι) {f g : ι → G}
725 (h : ∀ i ∈ l, RelatorEquivalent R (f i) (g i)) :
726 RelatorEquivalent R (l.map f).prod (l.map g).prod := by
727 induction l with
728 | nil =>
729 exact RelatorEquivalent.refl R 1
730 | cons i is ih =>
731 simp only [List.mem_cons] at h
732 simpa using RelatorEquivalent.mul
733 (h i (Or.inl rfl))
734 (ih (by
735 intro j hj
736 exact h j (Or.inr hj)))
739 {ι : Type*} (l : List ι) {f : ι → G}
740 (h : ∀ i ∈ l, RelatorEquivalent R (f i) 1) :
741 RelatorEquivalent R (l.map f).prod 1 := by
742 simpa using
744 (f := f) (g := fun _ => (1 : G)) h
746theorem list_prod_map_inv_reverse (l : List G) :
747 (l.map Inv.inv).reverse.prod = l.prod⁻¹ := by
748 induction l with
749 | nil =>
750 simp only [List.map_nil, List.reverse_nil, List.prod_nil, inv_one]
751 | cons x xs ih =>
752 simp only [List.map_cons, List.reverse_cons, List.prod_append, ih, List.prod_cons, List.prod_nil, mul_one,
753 mul_inv_rev]
755theorem list_prod_reverse_map_inv (l : List G) :
756 (l.reverse.map Inv.inv).prod = l.prod⁻¹ := by
757 simpa [List.map_reverse] using list_prod_map_inv_reverse (G := G) l
760 {l m : List G}
761 (h : RelatorEquivalent R l.prod m.prod) :
762 RelatorEquivalent R (l.reverse.map Inv.inv).prod
763 (m.reverse.map Inv.inv).prod := by
764 simpa [List.map_reverse, list_prod_map_inv_reverse] using
765 RelatorEquivalent.inv h
768 {l₁ l₂ m₁ m₂ : List G}
769 (h₁ : RelatorEquivalent R l₁.prod m₁.prod)
770 (h₂ : RelatorEquivalent R l₂.prod m₂.prod) :
771 RelatorEquivalent R (l₁ ++ l₂).prod (m₁ ++ m₂).prod := by
772 simpa using RelatorEquivalent.mul h₁ h₂
775 (l : List G) {m n : List G}
776 (h : RelatorEquivalent R m.prod n.prod) :
777 RelatorEquivalent R (l ++ m).prod (l ++ n).prod := by
779 (R := R) (l₁ := l) (l₂ := m) (m₁ := l) (m₂ := n)
780 (RelatorEquivalent.refl R l.prod) h
783 (l m : List G) {u : G}
784 (h : RelatorEquivalent R u 1) :
785 RelatorEquivalent R (l ++ u :: m).prod (l ++ m).prod := by
786 have htail :
787 RelatorEquivalent R (u :: m).prod m.prod := by
788 simpa using RelatorEquivalent.mul h (RelatorEquivalent.refl R m.prod)
789 simpa [List.singleton_append] using
793 (l m : List G) {u v : G}
794 (h : RelatorEquivalent R u v) :
795 RelatorEquivalent R (l ++ (u * v⁻¹) :: m).prod
796 (l ++ m).prod :=
798 (RelatorEquivalent.mul_inv_eq_one h)
801 {l m : List G}
802 (h : (l ++ m).prod ∈ Subgroup.normalClosure R) :
803 (m ++ l).prod ∈ Subgroup.normalClosure R := by
804 have hprod : l.prod * m.prod ∈ Subgroup.normalClosure R := by
805 simpa using h
806 have hrot :
807 m.prod * l.prod ∈ Subgroup.normalClosure R :=
809 (a := l.prod) (b := m.prod) hprod
810 simpa using hrot
813 {l m : List G}
814 (h : RelatorEquivalent R (l ++ m).prod 1) :
815 RelatorEquivalent R (m ++ l).prod 1 := by
816 exact RelatorEquivalent.of_mem_normalClosure
818 (by simpa [RelatorEquivalent] using h))
821 {l m : List G}
822 (h : RelatorEquivalent R (l ++ m).prod 1) :
823 RelatorEquivalent R (m ++ l).prod 1 :=
827 (l : List G) (n : ℕ)
828 (h : RelatorEquivalent R l.prod 1) :
829 RelatorEquivalent R ((l.drop n) ++ (l.take n)).prod 1 := by
830 have hsplit :
831 RelatorEquivalent R ((l.take n) ++ (l.drop n)).prod 1 := by
832 simpa [List.take_append_drop] using h
836 (l : List G) (n : ℕ)
837 (h : l.prod ∈ Subgroup.normalClosure R) :
838 ((l.drop n) ++ (l.take n)).prod ∈ Subgroup.normalClosure R :=
839 RelatorEquivalent.mem_normalClosure_of_eq_one
841 (RelatorEquivalent.of_mem_normalClosure (by simpa [RelatorEquivalent] using h)))
843section OrderedFinsetProduct
845variable {ι : Type*} [LinearOrder ι]
847/-- A noncommutative product indexed by a finite set, using the ambient
848`LinearOrder` to choose the order. This is the right finite-indexed dispatcher
849for relator calculations in noncommutative groups. -/
850def orderedFinsetProduct (s : Finset ι) (f : ι → G) : G :=
851 ((s.sort (· ≤ ·)).map f).prod
854 (s : Finset ι) {f : ι → G}
855 (h : ∀ i ∈ s, f i ∈ Subgroup.normalClosure R) :
856 orderedFinsetProduct s f ∈ Subgroup.normalClosure R := by
858 exact list_prod_mem_normalClosure (R := R) (by
859 intro x hx
860 rcases List.mem_map.1 hx with ⟨i, hi, rfl⟩
861 exact h i (by
862 exact (Finset.mem_sort (s := s) (r := fun a b : ι => a ≤ b)).1 hi))
865 (s : Finset ι) {f g : ι → G}
866 (h : ∀ i ∈ s, RelatorEquivalent R (f i) (g i)) :
870 exact list_prod_map_relatorEquivalent (R := R) (s.sort (· ≤ ·))
871 (f := f) (g := g) (by
872 intro i hi
873 exact h i (by
874 exact (Finset.mem_sort (s := s) (r := fun a b : ι => a ≤ b)).1 hi))
877 (s : Finset ι) {f : ι → G}
878 (h : ∀ i ∈ s, RelatorEquivalent R (f i) 1) :
881 simpa using
882 list_prod_map_relatorEquivalent_one (R := R) (s.sort (· ≤ ·))
883 (f := f) (by
884 intro i hi
885 exact h i (by
886 exact (Finset.mem_sort (s := s) (r := fun a b : ι => a ≤ b)).1 hi))
889 (s : Finset ι) {f g : ι → G}
890 (h : ∀ i ∈ s, f i = g i) :
893 congr 1
894 apply List.map_congr_left
895 intro i hi
896 exact h i ((Finset.mem_sort (s := s) (r := fun a b : ι => a ≤ b)).1 hi)
898end OrderedFinsetProduct
901theorem conjugate_list_prod {G : Type*} [Group G] (x : G) :
902 ∀ l : List G, x * l.prod * x⁻¹ = (l.map fun t => x * t * x⁻¹).prod
903 | [] => by
904 simp only [List.prod_nil, mul_one, mul_inv_cancel, List.map_nil]
905 | t :: ts => by
906 rw [List.prod_cons, List.map_cons, List.prod_cons]
907 calc
908 x * (t * ts.prod) * x⁻¹ = (x * t * x⁻¹) * (x * ts.prod * x⁻¹) := by
909 group
910 _ = x * t * x⁻¹ * (List.map (fun t => x * t * x⁻¹) ts).prod := by
913theorem nested_conjugate_list_prod {G : Type*} [Group G]
914 (x : G) {p n : ℕ} (f : Fin p → Fin n → G) :
915 (List.ofFn (fun b : Fin p =>
916 (List.ofFn (fun j : Fin n => x * f b j * x⁻¹)).prod)).prod =
917 x * (List.ofFn (fun b : Fin p =>
918 (List.ofFn (fun j : Fin n => f b j)).prod)).prod * x⁻¹ := by
919 have hinner :
920 (List.ofFn (fun b : Fin p =>
921 (List.ofFn (fun j : Fin n => x * f b j * x⁻¹)).prod)) =
922 List.ofFn (fun b : Fin p =>
923 x * (List.ofFn (fun j : Fin n => f b j)).prod * x⁻¹) := by
924 apply List.ofFn_inj.2
925 funext b
926 simpa using
927 (conjugate_list_prod x (List.ofFn (fun j : Fin n => f b j))).symm
928 rw [hinner]
929 simpa using
931 (List.ofFn (fun b : Fin p =>
932 (List.ofFn (fun j : Fin n => f b j)).prod))).symm
934theorem subgroup_list_prod_val {G : Type*} [Group G]
935 {H : Subgroup G} {n : ℕ} (f : Fin n → H) :
936 (((List.ofFn f).prod : H) : G) =
937 (List.ofFn (fun i : Fin n => ((f i : H) : G))).prod := by
938 change H.subtype ((List.ofFn f).prod) =
939 (List.ofFn (fun i : Fin n => ((f i : H) : G))).prod
940 rw [map_list_prod, List.map_ofFn]
941 apply congrArg List.prod
942 apply List.ofFn_inj.2
943 funext i
944 rfl
946theorem subgroup_nested_list_prod_val {G : Type*} [Group G]
947 {H : Subgroup G} {p n : ℕ} (f : Fin p → Fin n → H) :
948 (((List.ofFn (fun b : Fin p =>
949 (List.ofFn (fun j : Fin n => f b j)).prod)).prod : H) : G) =
950 (List.ofFn (fun b : Fin p =>
951 (List.ofFn (fun j : Fin n => ((f b j : H) : G))).prod)).prod := by
952 change H.subtype
953 ((List.ofFn (fun b : Fin p =>
954 (List.ofFn (fun j : Fin n => f b j)).prod)).prod) =
955 (List.ofFn (fun b : Fin p =>
956 (List.ofFn (fun j : Fin n => ((f b j : H) : G))).prod)).prod
957 rw [map_list_prod, List.map_ofFn]
958 apply congrArg List.prod
959 apply List.ofFn_inj.2
960 funext b
961 exact subgroup_list_prod_val (fun j : Fin n => f b j)
966 {Y : Type*} (R : Set (FreeGroup Y)) (F : FreeGroup Y →* FreeGroup Y)
967 (hgen :
968 ∀ y : Y,
969 F (FreeGroup.of y) * (FreeGroup.of y)⁻¹ ∈ Subgroup.normalClosure R) :
970 ∀ w : FreeGroup Y, F w * w⁻¹ ∈ Subgroup.normalClosure R := by
971 classical
972 let N : Subgroup (FreeGroup Y) := Subgroup.normalClosure R
973 let q : FreeGroup Y →* FreeGroup Y ⧸ N := QuotientGroup.mk' N
974 have hq : q.comp F = q := by
975 apply FreeGroup.ext_hom
976 intro y
977 change q (F (FreeGroup.of y)) = q (FreeGroup.of y)
978 exact
979 (QuotientGroup.eq_iff_div_mem
980 (N := N) (x := F (FreeGroup.of y)) (y := FreeGroup.of y)).2
981 (by simpa [N, div_eq_mul_inv] using hgen y)
982 intro w
983 have hw :
984 q (F w) = q w := by
985 simpa using congrArg (fun ψ : FreeGroup Y →* FreeGroup Y ⧸ N => ψ w) hq
986 exact
987 (QuotientGroup.eq_iff_div_mem (N := N) (x := F w) (y := w)).1
988 (by simpa [N, div_eq_mul_inv] using hw)
991end NormalClosure
993end ReidemeisterSchreier.Discrete.Presentations