Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Basic
1import Mathlib.Algebra.Group.Subgroup.Basic
2import Mathlib.Algebra.BigOperators.Group.List.Basic
3import Mathlib.Data.Finset.Sort
4import Mathlib.GroupTheory.FreeGroup.Reduce
5import Mathlib.GroupTheory.QuotientGroup.Defs
7/-!
8# Relator equivalence
10This module defines equality modulo a relator normal closure and proves its
11elementary equivalence, congruence, inversion, multiplication, and quotient
12characterizations.
13-/
15namespace ReidemeisterSchreier.Discrete.Presentations
17variable {G H : Type*} [Group G] [Group H]
19/-- Equality modulo the normal closure generated by R. -/
20def RelatorEquivalent (R : Set G) (u v : G) : Prop :=
21 u * v⁻¹ ∈ Subgroup.normalClosure R
23/-- Relator equivalence is equivalent to equality in the presented quotient. -/
24theorem relatorEquivalent_iff_eq_in_presentedQuotient {R : Set G} {u v : G} :
25 RelatorEquivalent R u v ↔
26 ((u : G ⧸ Subgroup.normalClosure R) =
27 (v : G ⧸ Subgroup.normalClosure R)) := by
28 simpa [RelatorEquivalent, div_eq_mul_inv] using
29 (QuotientGroup.eq_iff_div_mem
30 (N := Subgroup.normalClosure R) (x := u) (y := v)).symm
32/-- Relator equivalence to one on the right is membership in the relator normal closure. -/
33@[simp] theorem relatorEquivalent_one_right {R : Set G} {u : G} :
34 RelatorEquivalent R u 1 ↔ u ∈ Subgroup.normalClosure R := by
35 simp only [RelatorEquivalent, inv_one, mul_one]
37/-- Relator equivalence from one on the left is membership in the relator normal closure. -/
38@[simp] theorem relatorEquivalent_one_left {R : Set G} {u : G} :
39 RelatorEquivalent R 1 u ↔ u ∈ Subgroup.normalClosure R := by
40 constructor
41 · intro h
42 have huInv : u⁻¹ ∈ Subgroup.normalClosure R := by
43 simpa [RelatorEquivalent] using h
44 simpa using Subgroup.inv_mem (Subgroup.normalClosure R) huInv
45 · intro h
46 have huInv : u⁻¹ ∈ Subgroup.normalClosure R :=
47 Subgroup.inv_mem (Subgroup.normalClosure R) h
48 simpa [RelatorEquivalent] using huInv
50/-- Relator equivalence defines a setoid on the free group. -/
51def relatorEquivalentSetoid (R : Set G) : Setoid G where
52 r := RelatorEquivalent R
53 iseqv := by
54 refine ⟨?_, ?_, ?_⟩
55 · intro u
56 rw [relatorEquivalent_iff_eq_in_presentedQuotient]
57 · intro u v h
58 rw [relatorEquivalent_iff_eq_in_presentedQuotient] at h ⊢
59 exact h.symm
60 · intro u v w huv hvw
61 rw [relatorEquivalent_iff_eq_in_presentedQuotient] at huv hvw ⊢
62 exact huv.trans hvw
64namespace RelatorEquivalent
66variable {R S : Set G} {u v w a b r : G}
68/-- Relator equivalence is reflexive. -/
69@[refl]
70theorem refl (R : Set G) (u : G) : RelatorEquivalent R u u := by
71 rw [relatorEquivalent_iff_eq_in_presentedQuotient]
73/-- Equal relators are relator-equivalent. -/
74theorem of_eq (h : u = v) : RelatorEquivalent R u v := by
75 rw [h]
77/-- Relator equivalence is symmetric. -/
78theorem symm (h : RelatorEquivalent R u v) : RelatorEquivalent R v u := by
79 rw [relatorEquivalent_iff_eq_in_presentedQuotient] at h ⊢
80 exact h.symm
82/-- Relator equivalence is transitive. -/
83theorem trans (h₁ : RelatorEquivalent R u v) (h₂ : RelatorEquivalent R v w) : RelatorEquivalent
84 R u w := by
85 rw [relatorEquivalent_iff_eq_in_presentedQuotient] at h₁ h₂ ⊢
86 exact h₁.trans h₂
88/-- Taking inverses preserves relator equivalence. -/
89theorem inv (h : RelatorEquivalent R u v) : RelatorEquivalent R u⁻¹ v⁻¹ := by
90 rw [relatorEquivalent_iff_eq_in_presentedQuotient] at h ⊢
91 simpa using congrArg Inv.inv h
93/-- Multiplication of relator-equivalent words preserves relator equivalence. -/
94theorem mul (h₁ : RelatorEquivalent R u v) (h₂ : RelatorEquivalent R a b) :
95 RelatorEquivalent R (u * a) (v * b) := by
96 rw [relatorEquivalent_iff_eq_in_presentedQuotient] at h₁ h₂ ⊢
97 calc
98 ((u * a : G) : G ⧸ Subgroup.normalClosure R) =
99 (u : G ⧸ Subgroup.normalClosure R) * (a : G ⧸ Subgroup.normalClosure R) := rfl
100 _ = (v : G ⧸ Subgroup.normalClosure R) * (b : G ⧸ Subgroup.normalClosure R) := by
101 rw [h₁, h₂]
102 _ = ((v * b : G) : G ⧸ Subgroup.normalClosure R) := rfl
104/-- Taking natural powers preserves relator equivalence. -/
105theorem pow (h : RelatorEquivalent R u v) (n : ℕ) : RelatorEquivalent R (u ^ n) (v ^ n) := by
106 rw [relatorEquivalent_iff_eq_in_presentedQuotient] at h ⊢
107 simpa using congrArg (fun z : G ⧸ Subgroup.normalClosure R => z ^ n) h
109/-- Taking integer powers preserves relator equivalence. -/
110theorem zpow (h : RelatorEquivalent R u v) (n : ℤ) : RelatorEquivalent R (u ^ n) (v ^ n) := by
111 rw [relatorEquivalent_iff_eq_in_presentedQuotient] at h ⊢
112 simpa using congrArg (fun z : G ⧸ Subgroup.normalClosure R => z ^ n) h
114/-- A product of words relator-equivalent to one is relator-equivalent to one. -/
115theorem mul_eq_one (h₁ : RelatorEquivalent R u 1) (h₂ : RelatorEquivalent R v 1) :
116 RelatorEquivalent R (u * v) 1 := by
117 simpa using mul h₁ h₂
119/--
120A natural-number power is relator-equivalent to the identity when the base word is
121relator-equivalent to the identity.
122-/
123theorem pow_eq_one (h : RelatorEquivalent R u 1) (n : ℕ) :
124 RelatorEquivalent R (u ^ n) 1 := by
125 simpa using pow h n
127/--
128An integer power is relator-equivalent to the identity when the base word is relator-equivalent
129to the identity.
130-/
131theorem zpow_eq_one (h : RelatorEquivalent R u 1) (n : ℤ) :
132 RelatorEquivalent R (u ^ n) 1 := by
133 simpa using zpow h n
135/-- The inverse of a word is relator-equivalent to one exactly when the word is. -/
136theorem inv_eq_one (h : RelatorEquivalent R u 1) :
137 RelatorEquivalent R u⁻¹ 1 := by
138 simpa using inv h
140/-- Conjugating a power relator gives an equivalent relator. -/
141theorem conjugate_pow_eq (a u : G) (n : ℕ) :
142 (a * u * a⁻¹) ^ n = a * u ^ n * a⁻¹ := by
143 induction n with
144 | zero =>
145 simp only [pow_zero, mul_one, mul_inv_cancel]
146 | succ n ih =>
147 calc
148 (a * u * a⁻¹) ^ (n + 1) =
149 a * u ^ n * a⁻¹ * (a * u * a⁻¹) := by
150 rw [pow_succ, ih]
151 _ = a * (u ^ n * u) * a⁻¹ := by
152 simp only [mul_assoc, inv_mul_cancel_left]
153 _ = a * u ^ (n + 1) * a⁻¹ := by
154 rw [pow_succ]
156/-- A product is trivial modulo the relators exactly when its first factor equals the inverse of the second. -/
157theorem mul_eq_one_iff_eq_inv :
158 RelatorEquivalent R (u * v) 1 ↔ RelatorEquivalent R u v⁻¹ := by
159 constructor
160 · intro h
161 simpa only [RelatorEquivalent, inv_inv, inv_one, mul_one] using h
162 · intro h
163 simpa only [RelatorEquivalent, inv_inv, inv_one, mul_one] using h
165/--
166If a product is relator-equivalent to one, the left factor is relator-equivalent to the inverse
167of the right factor.
168-/
169theorem eq_inv_of_mul_eq_one (h : RelatorEquivalent R (u * v) 1) :
170 RelatorEquivalent R u v⁻¹ :=
171 mul_eq_one_iff_eq_inv.1 h
173/--
174A product is relator-equivalent to the identity when one factor is relator-equivalent to the
175inverse of the other.
176-/
177theorem mul_eq_one_of_eq_inv (h : RelatorEquivalent R u v⁻¹) :
178 RelatorEquivalent R (u * v) 1 :=
179 mul_eq_one_iff_eq_inv.2 h
181/--
182If a left product is relator-equivalent to one and the left factor is trivial, the right factor
183is relator-equivalent to one.
184-/
185theorem eq_one_of_mul_eq_one_left
186 (hu : RelatorEquivalent R u 1)
187 (huv : RelatorEquivalent R (u * v) 1) :
188 RelatorEquivalent R v 1 := by
189 rw [relatorEquivalent_iff_eq_in_presentedQuotient] at hu huv ⊢
190 calc
191 (v : G ⧸ Subgroup.normalClosure R) =
192 (1 : G ⧸ Subgroup.normalClosure R) * v := by simp only [one_mul]
193 _ = (u : G ⧸ Subgroup.normalClosure R) * v := by
194 simpa using congrArg
195 (fun z : G ⧸ Subgroup.normalClosure R =>
196 z * (v : G ⧸ Subgroup.normalClosure R)) hu.symm
197 _ = ((u * v : G) : G ⧸ Subgroup.normalClosure R) := rfl
198 _ = 1 := huv
200/--
201If a right product is relator-equivalent to one and the right factor is trivial, the left factor
202is relator-equivalent to one.
203-/
204theorem eq_one_of_mul_eq_one_right
205 (huv : RelatorEquivalent R (u * v) 1)
206 (hv : RelatorEquivalent R v 1) :
207 RelatorEquivalent R u 1 := by
208 rw [relatorEquivalent_iff_eq_in_presentedQuotient] at huv hv ⊢
209 calc
210 (u : G ⧸ Subgroup.normalClosure R) =
211 (u : G ⧸ Subgroup.normalClosure R) * 1 := by simp only [mul_one]
212 _ = (u : G ⧸ Subgroup.normalClosure R) * v := by
213 simpa using congrArg
214 (fun z : G ⧸ Subgroup.normalClosure R =>
215 (u : G ⧸ Subgroup.normalClosure R) * z) hv.symm
216 _ = ((u * v : G) : G ⧸ Subgroup.normalClosure R) := rfl
217 _ = 1 := huv
219/-- Left multiplication by the same word preserves relator equivalence. -/
220theorem mul_left (h : RelatorEquivalent R u v) (a : G) : RelatorEquivalent R (a * u) (a * v) :=
221 mul (refl R a) h
223/-- Right multiplication by the same word preserves relator equivalence. -/
224theorem mul_right (h : RelatorEquivalent R u v) (a : G) : RelatorEquivalent R (u * a) (v * a) :=
225 mul h (refl R a)
227/-- Replace a subword inside a two-sided context. -/
228theorem context (h : RelatorEquivalent R u v) (a b : G) :
229 RelatorEquivalent R (a * u * b) (a * v * b) :=
230 mul_right (mul_left h a) b
232/-- Conjugating both sides preserves relator equivalence. -/
233theorem conj (h : RelatorEquivalent R u v) (a : G) :
234 RelatorEquivalent R (a * u * a⁻¹) (a * v * a⁻¹) :=
235 context h a a⁻¹
237/--
238If a word is relator-equivalent to the identity, then every conjugate of it is also
239relator-equivalent to the identity.
240-/
241theorem conj_eq_one (h : RelatorEquivalent R u 1) (a : G) :
242 RelatorEquivalent R (a * u * a⁻¹) 1 := by
243 simpa using conj h a
245/--
246If a power is relator-equivalent to the identity, then every conjugate of that power is also
247relator-equivalent to the identity.
248-/
249theorem conj_pow_eq_one
250 {n : ℕ} (h : RelatorEquivalent R (u ^ n) 1) (a : G) :
251 RelatorEquivalent R ((a * u * a⁻¹) ^ n) 1 := by
252 simpa [conjugate_pow_eq] using conj_eq_one h a
254/-- Every defining relator is equivalent to the identity. -/
255theorem of_mem (hr : r ∈ R) : RelatorEquivalent R r 1 := by
256 simpa [RelatorEquivalent] using (Subgroup.subset_normalClosure hr :
257 r ∈ Subgroup.normalClosure R)
259/-- Membership in the normal closure gives relator equivalence to the identity. -/
260theorem of_mem_normalClosure (hr : r ∈ Subgroup.normalClosure R) :
261 RelatorEquivalent R r 1 := by
262 simpa [RelatorEquivalent] using hr
264/-- Relator equivalence is monotone with respect to enlarging the relator family. -/
265theorem mono (hR_to_S : R ⊆ S) (h : RelatorEquivalent R u v) :
266 RelatorEquivalent S u v := by
267 have hx : u * v⁻¹ ∈ Subgroup.normalClosure S :=
268 Subgroup.normalClosure_mono hR_to_S
269 (by simpa [RelatorEquivalent] using h)
270 simpa [RelatorEquivalent] using hx
272/-- Relator equivalence is monotone under an indexed union of relator families. -/
273theorem mono_iUnion {ι : Sort*} (R : ι → Set G)
274 (i : ι) (h : RelatorEquivalent (R i) u v) :
275 RelatorEquivalent (Set.iUnion R) u v :=
276 mono (R := R i) (S := Set.iUnion R)
277 (fun _ hx => Set.mem_iUnion.2 ⟨i, hx⟩) h
279/-- Relator equivalence is monotone under a doubly indexed union of relator families. -/
280theorem mono_iUnion₂ {ι : Sort*} {κ : ι → Sort*}
281 (R : ∀ i : ι, κ i → Set G)
282 (i : ι) (j : κ i) (h : RelatorEquivalent (R i j) u v) :
283 RelatorEquivalent (Set.iUnion fun i : ι => Set.iUnion (R i)) u v :=
284 mono (R := R i j) (S := Set.iUnion fun i : ι => Set.iUnion (R i))
285 (fun _ hx => Set.mem_iUnion.2 ⟨i, Set.mem_iUnion.2 ⟨j, hx⟩⟩) h
287/-- A relator-equivalence certificate to the identity gives membership in the normal closure. -/
288theorem mem_normalClosure_of_eq_one (h : RelatorEquivalent R r 1) :
289 r ∈ Subgroup.normalClosure R := by
290 simpa [RelatorEquivalent] using h
292/--
293If two words are relator-equivalent, then multiplying one by the inverse of the other gives an
294element of the relator normal closure.
295-/
296theorem mul_inv_mem_normalClosure (h : RelatorEquivalent R u v) :
297 u * v⁻¹ ∈ Subgroup.normalClosure R := by
298 simpa [RelatorEquivalent] using h
300/--
301If two words are relator-equivalent, then their quotient lies in the normal closure of the
302relators.
303-/
304theorem div_mem_normalClosure (h : RelatorEquivalent R u v) :
305 u / v ∈ Subgroup.normalClosure R := by
306 simpa [div_eq_mul_inv] using h.mul_inv_mem_normalClosure
308/--
309Multiplying a word by the inverse of a relator-equivalent word gives a word relator-equivalent
310to one.
311-/
312theorem mul_inv_eq_one (h : RelatorEquivalent R u v) :
313 RelatorEquivalent R (u * v⁻¹) 1 :=
314 of_mem_normalClosure h.mul_inv_mem_normalClosure
316/--
317A quotient word is relator-equivalent to the identity when its numerator and denominator are
318relator-equivalent to each other.
319-/
320theorem div_eq_one (h : RelatorEquivalent R u v) :
321 RelatorEquivalent R (u / v) 1 := by
322 simpa [div_eq_mul_inv] using h.mul_inv_eq_one
324/-- The identity is equivalent to every defining relator. -/
325theorem one_eq_of_mem_inv (hr : r ∈ R) : RelatorEquivalent R 1 r :=
326 (of_mem hr).symm
328end RelatorEquivalent
330end ReidemeisterSchreier.Discrete.Presentations