Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Operations

1import Mathlib.Tactic.Group

2import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Relators.Basic

4/-!

5# Operations on relator normal closures

7This module proves invariance and closure lemmas for changing relator sets,

8conjugating and cyclically rotating words, products of lists, and ordered

9finite products.

10-/

12namespace ReidemeisterSchreier.Discrete.Presentations

14variable {G H : Type*} [Group G] [Group H]

16section NormalClosure

18variable {R S : Set G} {r a b : G}

20/--

21If every relator on each side is trivial modulo the other side, the normal closures are equal.

22-/

23theorem normalClosure_eq_of_relatorEquivalent

24 (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)

25 (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :

26 Subgroup.normalClosure R = Subgroup.normalClosure S := by

27 apply le_antisymm

28 · refine Subgroup.normalClosure_le_normal ?_

29 intro r hr

30 exact RelatorEquivalent.mem_normalClosure_of_eq_one (hR_to_S r hr)

31 · refine Subgroup.normalClosure_le_normal ?_

32 intro s hs

33 exact RelatorEquivalent.mem_normalClosure_of_eq_one (hS_to_R s hs)

35/-- Inserting an element already in the normal closure does not change the normal closure. -/

36theorem normalClosure_insert_eq_of_mem

37 (hr : r ∈ Subgroup.normalClosure R) :

38 Subgroup.normalClosure (insert r R) = Subgroup.normalClosure R := by

39 apply le_antisymm

40 · refine Subgroup.normalClosure_le_normal ?_

41 intro x hx

42 rcases hx with rfl | hx

43 · exact hr

44 · exact Subgroup.subset_normalClosure hx

45 · exact Subgroup.normalClosure_mono (by

46 intro x hx

47 exact Set.mem_insert_of_mem r hx)

49/--

50Removing a relator that already lies in the normal closure of the remaining relators does not

51change the normal closure.

52-/

53theorem normalClosure_diff_singleton_eq_of_mem

54 (hr : r ∈ Subgroup.normalClosure (R \ {r})) :

55 Subgroup.normalClosure R = Subgroup.normalClosure (R \ {r}) := by

56 apply le_antisymm

57 · refine Subgroup.normalClosure_le_normal ?_

58 intro x hx

59 by_cases hxr : x = r

60 · simpa [hxr] using hr

61 · exact Subgroup.subset_normalClosure ⟨hx, by simpa [Set.mem_singleton_iff] using hxr⟩

62 · exact Subgroup.normalClosure_mono (by

63 intro x hx

64 exact hx.1)

66/--

67Two relator normal closures are equal when each relator family is contained in the normal

68closure generated by the other.

69-/

70theorem normalClosure_eq_of_subset_normalClosure

71 (hR_to_S : R ⊆ Subgroup.normalClosure S)

72 (hS_to_R : S ⊆ Subgroup.normalClosure R) :

73 Subgroup.normalClosure R = Subgroup.normalClosure S := by

74 apply le_antisymm

75 · exact Subgroup.normalClosure_le_normal hR_to_S

76 · exact Subgroup.normalClosure_le_normal hS_to_R

78/-- Every conjugate of a relator belongs to the normal closure of the relator set. -/

79theorem conjugate_mem_normalClosure_of_mem

80 (hr : r ∈ R) (a : G) :

81 a * r * a⁻¹ ∈ Subgroup.normalClosure R := by

82 simpa [mul_assoc] using

83 (Subgroup.normalClosure_normal.conj_mem r

84 (Subgroup.subset_normalClosure hr) a)

86/-- A conjugate of a relator belongs to the normal closure of the relator set. -/

87theorem conjugate_mem_normalClosure

88 (hr : r ∈ Subgroup.normalClosure R) (a : G) :

89 a * r * a⁻¹ ∈ Subgroup.normalClosure R := by

90 simpa [mul_assoc] using

91 (Subgroup.normalClosure_normal.conj_mem r hr a)

93/-- Cyclically rotating a relator keeps it in the same normal closure. -/

94theorem cyclic_rotation_mem_normalClosure

95 (h : a * b ∈ Subgroup.normalClosure R) :

96 b * a ∈ Subgroup.normalClosure R := by

97 have hc := conjugate_mem_normalClosure (R := R) h b

98 simpa [mul_assoc] using hc

100/--

101If left multiplication by a relator-normal-closure element gives membership, then the original

102element has the same membership property.

103-/

104theorem mem_of_left_mul_mem_normalClosure

105 {a b : G}

106 (ha : a ∈ Subgroup.normalClosure R)

107 (hab : a * b ∈ Subgroup.normalClosure R) :

108 b ∈ Subgroup.normalClosure R := by

109 let N : Subgroup G := Subgroup.normalClosure R

110 have h : a⁻¹ * (a * b) ∈ N := N.mul_mem (N.inv_mem ha) hab

111 simpa [N, mul_assoc] using h

112

113/--

114A cyclic rotation of a power relator belongs to the normal closure of the original relator set.

115-/

116theorem cyclic_rotation_pow_mem_normalClosure

117 {a b : G} {n : ℕ}

118 (h : (a * b) ^ n ∈ Subgroup.normalClosure R) :

119 (b * a) ^ n ∈ Subgroup.normalClosure R := by

120 let N : Subgroup G := Subgroup.normalClosure R

121 have hconj : b * ((a * b) ^ n) * b⁻¹ ∈ N := by

122 simpa [N, MulAut.conj_apply] using

123 (Subgroup.normalClosure_normal.conj_mem ((a * b) ^ n) h b)

124 have hpow : b * ((a * b) ^ n) * b⁻¹ = (b * a) ^ n := by

125 clear h hconj

126 induction n with

127 | zero =>

128 simp only [pow_zero, mul_one, mul_inv_cancel]

129 | succ n ih =>

130 rw [pow_succ, pow_succ, ← ih]

131 group

132 simpa [hpow] using hconj

133

134/--

135If u and v are congruent modulo the normal closure and a power of v lies in it, then the same

136power of u lies in it.

137-/

138theorem pow_mem_normalClosure_of_mul_inv_mem

139 {u v : G} {n : ℕ}

140 (huv : u * v⁻¹ ∈ Subgroup.normalClosure R)

141 (hv : v ^ n ∈ Subgroup.normalClosure R) :

142 u ^ n ∈ Subgroup.normalClosure R := by

143 let N : Subgroup G := Subgroup.normalClosure R

144 let q : G →* G ⧸ N := QuotientGroup.mk' N

145 have hq : q u = q v := by

146 exact

147 (QuotientGroup.eq_iff_div_mem (N := N) (x := u) (y := v)).2

148 (by simpa [N, div_eq_mul_inv] using huv)

149 have hqv : q (v ^ n) = 1 :=

150 (QuotientGroup.eq_one_iff (N := N) (v ^ n)).2 hv

151 have hqu : q (u ^ n) = 1 := by

152 rw [map_pow, hq, ← map_pow]

153 exact hqv

154 exact (QuotientGroup.eq_one_iff (N := N) (u ^ n)).1 hqu

155

156/-- The product of a list of relators belongs to the normal closure of the relator set. -/

157theorem list_prod_mem_normalClosure

158 {l : List G}

159 (h : ∀ x ∈ l, x ∈ Subgroup.normalClosure R) :

160 l.prod ∈ Subgroup.normalClosure R := by

161 induction l with

162 | nil =>

163 simp only [List.prod_nil, one_mem]

164 | cons x xs ih =>

165 simp only [List.mem_cons] at h

166 exact Subgroup.mul_mem (Subgroup.normalClosure R)

167 (h x (Or.inl rfl))

168 (ih (by

169 intro y hy

170 exact h y (Or.inr hy)))

171

172/--

173Mapping a list through relator-equivalent entries preserves relator equivalence of the product.

174-/

175theorem list_prod_map_relatorEquivalent

176 {ι : Type*} (l : List ι) {f g : ι → G}

177 (h : ∀ i ∈ l, RelatorEquivalent R (f i) (g i)) :

178 RelatorEquivalent R (l.map f).prod (l.map g).prod := by

179 induction l with

180 | nil =>

181 exact RelatorEquivalent.refl R 1

182 | cons i is ih =>

183 simp only [List.mem_cons] at h

184 simpa using RelatorEquivalent.mul

185 (h i (Or.inl rfl))

186 (ih (by

187 intro j hj

188 exact h j (Or.inr hj)))

189

190/--

191A list product is relator-equivalent to the identity when every mapped entry is

192relator-equivalent to the identity.

193-/

194theorem list_prod_map_relatorEquivalent_one

195 {ι : Type*} (l : List ι) {f : ι → G}

196 (h : ∀ i ∈ l, RelatorEquivalent R (f i) 1) :

197 RelatorEquivalent R (l.map f).prod 1 := by

198 simpa using

199 list_prod_map_relatorEquivalent (R := R) l

200 (f := f) (g := fun _ => (1 : G)) h

201

202/-- Mapping inversion over a list and then reversing it gives a product equal to the inverse product. -/

203theorem list_prod_map_inv_reverse (l : List G) :

204 (l.map Inv.inv).reverse.prod = l.prod⁻¹ := by

205 induction l with

206 | nil =>

207 simp only [List.map_nil, List.reverse_nil, List.prod_nil, inv_one]

208 | cons x xs ih =>

209 simp only [List.map_cons, List.reverse_cons, List.prod_append, ih, List.prod_cons,

210 List.prod_nil, mul_one,

211 mul_inv_rev]

212

213/-- Reversing a list and then inverting its entries gives a product equal to the inverse product. -/

214theorem list_prod_reverse_map_inv (l : List G) :

215 (l.reverse.map Inv.inv).prod = l.prod⁻¹ := by

216 simpa [List.map_reverse] using list_prod_map_inv_reverse (G := G) l

217

218/-- A list product is relator-equivalent to the inverse of the reversed inverse list product. -/

219theorem list_prod_reverse_inv_relatorEquivalent

220 {l m : List G}

221 (h : RelatorEquivalent R l.prod m.prod) :

222 RelatorEquivalent R (l.reverse.map Inv.inv).prod

223 (m.reverse.map Inv.inv).prod := by

224 simpa [List.map_reverse, list_prod_map_inv_reverse] using

225 RelatorEquivalent.inv h

226

227/-- Appending relator-equivalent list products preserves relator equivalence. -/

228theorem list_prod_append_relatorEquivalent

229 {l₁ l₂ m₁ m₂ : List G}

230 (h₁ : RelatorEquivalent R l₁.prod m₁.prod)

231 (h₂ : RelatorEquivalent R l₂.prod m₂.prod) :

232 RelatorEquivalent R (l₁ ++ l₂).prod (m₁ ++ m₂).prod := by

233 simpa using RelatorEquivalent.mul h₁ h₂

234

235/-- Left-appending the same list product preserves relator equivalence. -/

236theorem list_prod_append_left_relatorEquivalent

237 (l : List G) {m n : List G}

238 (h : RelatorEquivalent R m.prod n.prod) :

239 RelatorEquivalent R (l ++ m).prod (l ++ n).prod := by

240 exact list_prod_append_relatorEquivalent

241 (R := R) (l₁ := l) (l₂ := m) (m₁ := l) (m₂ := n)

242 (RelatorEquivalent.refl R l.prod) h

243

244/-- Removing a middle subproduct equal to one preserves relator equivalence of the list product. -/

245theorem list_prod_middle_eq_one_relatorEquivalent

246 (l m : List G) {u : G}

247 (h : RelatorEquivalent R u 1) :

248 RelatorEquivalent R (l ++ u :: m).prod (l ++ m).prod := by

249 have htail :

250 RelatorEquivalent R (u :: m).prod m.prod := by

251 simpa using RelatorEquivalent.mul h (RelatorEquivalent.refl R m.prod)

252 simpa [List.singleton_append] using

253 list_prod_append_left_relatorEquivalent (R := R) l htail

254

255/--

256Inserting or removing a middle product multiplied by its inverse preserves relator equivalence.

257-/

258theorem list_prod_middle_mul_inv_relatorEquivalent

259 (l m : List G) {u v : G}

260 (h : RelatorEquivalent R u v) :

261 RelatorEquivalent R (l ++ (u * v⁻¹) :: m).prod

262 (l ++ m).prod :=

263 list_prod_middle_eq_one_relatorEquivalent (R := R) l m

264 (RelatorEquivalent.mul_inv_eq_one h)

265

266/-- Rotating an appended list product gives an element of the relator normal closure. -/

267theorem list_prod_append_rotate_mem_normalClosure

268 {l m : List G}

269 (h : (l ++ m).prod ∈ Subgroup.normalClosure R) :

270 (m ++ l).prod ∈ Subgroup.normalClosure R := by

271 have hprod : l.prod * m.prod ∈ Subgroup.normalClosure R := by

272 simpa using h

273 have hrot :

274 m.prod * l.prod ∈ Subgroup.normalClosure R :=

275 cyclic_rotation_mem_normalClosure (R := R)

276 (a := l.prod) (b := m.prod) hprod

277 simpa using hrot

278

279/--

280A rotated append decomposition of a list product is relator-equivalent to the original product.

281-/

282theorem list_prod_append_rotate_relatorEquivalent

283 {l m : List G}

284 (h : RelatorEquivalent R (l ++ m).prod 1) :

285 RelatorEquivalent R (m ++ l).prod 1 := by

286 exact RelatorEquivalent.of_mem_normalClosure

287 (list_prod_append_rotate_mem_normalClosure (R := R)

288 (by simpa [RelatorEquivalent] using h))

289

290/-- The take/drop rotation of a list product is relator-equivalent to the original product. -/

291theorem list_prod_take_drop_rotate_relatorEquivalent

292 (l : List G) (n : ℕ)

293 (h : RelatorEquivalent R l.prod 1) :

294 RelatorEquivalent R ((l.drop n) ++ (l.take n)).prod 1 := by

295 have hsplit :

296 RelatorEquivalent R ((l.take n) ++ (l.drop n)).prod 1 := by

297 simpa [List.take_append_drop] using h

298 exact list_prod_append_rotate_relatorEquivalent (R := R) hsplit

299

300/-- A take-drop rotation of a list product belongs to the relator normal closure. -/

301theorem list_prod_take_drop_rotate_mem_normalClosure

302 (l : List G) (n : ℕ)

303 (h : l.prod ∈ Subgroup.normalClosure R) :

304 ((l.drop n) ++ (l.take n)).prod ∈ Subgroup.normalClosure R :=

305 RelatorEquivalent.mem_normalClosure_of_eq_one

306 (list_prod_take_drop_rotate_relatorEquivalent (R := R) l n

307 (RelatorEquivalent.of_mem_normalClosure (by simpa [RelatorEquivalent] using h)))

308

309section OrderedFinsetProduct

310

311variable {ι : Type*} [LinearOrder ι]

312

313/--

314A noncommutative product indexed by a finite set, with multiplication ordered by the ambient

315\(LinearOrder\).

316-/

317def orderedFinsetProduct (s : Finset ι) (f : ι → G) : G :=

318 ((s.sort (· ≤ ·)).map f).prod

319

320/-- An ordered finite product of relators belongs to the normal closure of the relator set. -/

321theorem orderedFinsetProduct_mem_normalClosure

322 (s : Finset ι) {f : ι → G}

323 (h : ∀ i ∈ s, f i ∈ Subgroup.normalClosure R) :

324 orderedFinsetProduct s f ∈ Subgroup.normalClosure R := by

325 unfold orderedFinsetProduct

326 exact list_prod_mem_normalClosure (R := R) (by

327 intro x hx

328 rcases List.mem_map.1 hx with ⟨i, hi, rfl⟩

329 exact h i (by

330 exact (Finset.mem_sort (s := s) (r := fun a b : ι => a ≤ b)).1 hi))

331

332/--

333Replacing each term of an ordered finite product by a relator-equivalent term preserves relator

334equivalence.

335-/

336theorem orderedFinsetProduct_relatorEquivalent

337 (s : Finset ι) {f g : ι → G}

338 (h : ∀ i ∈ s, RelatorEquivalent R (f i) (g i)) :

339 RelatorEquivalent R (orderedFinsetProduct s f)

340 (orderedFinsetProduct s g) := by

341 unfold orderedFinsetProduct

342 exact list_prod_map_relatorEquivalent (R := R) (s.sort (· ≤ ·))

343 (f := f) (g := g) (by

344 intro i hi

345 exact h i (by

346 exact (Finset.mem_sort (s := s) (r := fun a b : ι => a ≤ b)).1 hi))

347

348/--

349An ordered finite product is relator-equivalent to the identity when every term is

350relator-equivalent to the identity.

351-/

352theorem orderedFinsetProduct_relatorEquivalent_one

353 (s : Finset ι) {f : ι → G}

354 (h : ∀ i ∈ s, RelatorEquivalent R (f i) 1) :

355 RelatorEquivalent R (orderedFinsetProduct s f) 1 := by

356 unfold orderedFinsetProduct

357 simpa using

358 list_prod_map_relatorEquivalent_one (R := R) (s.sort (· ≤ ·))

359 (f := f) (by

360 intro i hi

361 exact h i (by

362 exact (Finset.mem_sort (s := s) (r := fun a b : ι => a ≤ b)).1 hi))

363

364/-- Pointwise equality on a finite index set gives equality of the corresponding ordered products. -/

365theorem orderedFinsetProduct_congr

366 (s : Finset ι) {f g : ι → G}

367 (h : ∀ i ∈ s, f i = g i) :

368 orderedFinsetProduct s f = orderedFinsetProduct s g := by

369 unfold orderedFinsetProduct

370 congr 1

371 apply List.map_congr_left

372 intro i hi

373 exact h i ((Finset.mem_sort (s := s) (r := fun a b : ι => a ≤ b)).1 hi)

374

375end OrderedFinsetProduct

376

377end NormalClosure

378

379end ReidemeisterSchreier.Discrete.Presentations