Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorDeletion

1import ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorAddition

3/-!

4# Reidemeister Schreier / Discrete / Presentations / Tietze / Generator Deletion

6This module formalizes deletion of generators forced to be trivial. It

7defines the elimination homomorphism and relator transformations and packages

8the induced equivalence of presented quotients.

9-/

11universe u v w

13namespace ReidemeisterSchreier.Discrete.Presentations

15namespace Presented

17variable {X Y : Type*}

19section AdjoinGenerators

21section DeleteTrivialGenerators

23variable (X Y)

25/--

26The substitution map sends the generators in \(Y\) to \(1\), while keeping the old generators

27\(X\). It is used by the Tietze move deleting generators with relators \(y = 1\).

28-/

29def trivializeGeneratorsHom : FreeGroup (Sum X Y) →* FreeGroup X :=

30 eliminateAdjoinedGeneratorsHom (fun _ : Y => 1)

32variable {X Y}

34/-- The trivializing homomorphism fixes each retained generator \(x : X\). -/

35@[simp]

36theorem trivializeGeneratorsHom_inl (x : X) :

37 trivializeGeneratorsHom X Y (FreeGroup.of (Sum.inl x)) =

38 FreeGroup.of x := by

39 simp only [trivializeGeneratorsHom, eliminateAdjoinedGeneratorsHom_inl]

41/-- The trivializing homomorphism sends each deleted generator \(y : Y\) to \(1\). -/

42@[simp]

43theorem trivializeGeneratorsHom_inr (y : Y) :

44 trivializeGeneratorsHom X Y (FreeGroup.of (Sum.inr y)) = 1 := by

45 simp only [trivializeGeneratorsHom, eliminateAdjoinedGeneratorsHom_inr]

47/--

48Trivializing the deleted generators after including the retained generators is the identity on

49the retained free group.

50-/

51theorem trivializeGeneratorsHom_comp_include :

52 (trivializeGeneratorsHom X Y).comp (includeAdjoinedGenerators X Y) =

53 MonoidHom.id (FreeGroup X) :=

54 eliminateAdjoinedGeneratorsHom_comp_include (fun _ : Y => 1)

56/-- Relators \(y = 1\) for a family of generators to be deleted. -/

57def trivialGeneratorRelators :

58 Set (FreeGroup (Sum X Y)) :=

59 {q | ∃ y : Y, q = FreeGroup.of (Sum.inr y)}

61/--

62Adds the relators \(y = 1\) to a presentation over \(X \oplus Y\), trivializing the auxiliary

63generators.

64-/

65def relatorsWithTrivialGenerators

66 (R : Set (FreeGroup (Sum X Y))) :

67 Set (FreeGroup (Sum X Y)) :=

68 R ∪ trivialGeneratorRelators (X := X) (Y := Y)

70/--

71The relators after deleting the \(Y\)-generators are obtained by substituting them with \(1\).

72-/

73def relatorsAfterDeletingTrivialGenerators

74 (R : Set (FreeGroup (Sum X Y))) :

75 Set (FreeGroup X) :=

76 trivializeGeneratorsHom X Y '' R

78/-- Each trivial-generator relation \(y = 1\) belongs to the trivial-generator relator set. -/

79theorem trivialGeneratorRelator_mem (y : Y) :

80 FreeGroup.of (Sum.inr y) ∈

81 trivialGeneratorRelators (X := X) (Y := Y) :=

82 ⟨y, rfl⟩

84/-- Each trivial-generator relation \(y = 1\) belongs to the relator set with trivial generators. -/

85theorem trivialGeneratorRelator_mem_relatorsWithTrivialGenerators

86 (R : Set (FreeGroup (Sum X Y))) (y : Y) :

87 FreeGroup.of (Sum.inr y) ∈ relatorsWithTrivialGenerators R :=

88 Or.inr (trivialGeneratorRelator_mem (X := X) (Y := Y) y)

90/-- Every original relator belongs to the relator set with trivial generators. -/

91theorem relator_mem_relatorsWithTrivialGenerators

92 {R : Set (FreeGroup (Sum X Y))} {r : FreeGroup (Sum X Y)}

93 (hr : r ∈ R) :

94 r ∈ relatorsWithTrivialGenerators R :=

95 Or.inl hr

97/--

98Including the result of trivializing deleted generators is congruent to the original word modulo

99the trivial-generator relators.

100-/

101theorem include_trivializeGeneratorsHom_mod_trivialGeneratorRelators

102 (z : FreeGroup (Sum X Y)) :

103 includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y z) * z⁻¹ ∈

104 Subgroup.normalClosure (trivialGeneratorRelators (X := X) (Y := Y)) := by

105 let S : Set (FreeGroup (Sum X Y)) :=

106 trivialGeneratorRelators (X := X) (Y := Y)

107 let N : Subgroup (FreeGroup (Sum X Y)) := Subgroup.normalClosure S

108 let F : FreeGroup (Sum X Y) →* FreeGroup (Sum X Y) :=

109 (includeAdjoinedGenerators X Y).comp (trivializeGeneratorsHom X Y)

110 have hhom : (QuotientGroup.mk' N).comp F = QuotientGroup.mk' N := by

111 ext z

112 cases z with

113 | inl x =>

114 simp only [includeAdjoinedGenerators, trivializeGeneratorsHom, MonoidHom.coe_comp,

115 QuotientGroup.coe_mk',

116 Function.comp_apply, eliminateAdjoinedGeneratorsHom_inl, FreeGroup.map.of,

117 QuotientGroup.mk'_apply, N, F]

118 | inr y =>

119 simp only [MonoidHom.comp_apply, F, trivializeGeneratorsHom_inr,

120 map_one]

121 change ((1 : FreeGroup (Sum X Y)) : FreeGroup (Sum X Y) ⧸ N) =

122 ((FreeGroup.of (Sum.inr y) : FreeGroup (Sum X Y)) :

123 FreeGroup (Sum X Y) ⧸ N)

124 apply (QuotientGroup.eq_iff_div_mem

125 (N := N)

126 (x := (1 : FreeGroup (Sum X Y)))

127 (y := FreeGroup.of (Sum.inr y))).2

128 have hrel :

129 FreeGroup.of (Sum.inr y) ∈ N :=

130 Subgroup.subset_normalClosure

131 (trivialGeneratorRelator_mem (X := X) (Y := Y) y)

132 simpa [N, div_eq_mul_inv] using N.inv_mem hrel

133 have hz := congrArg (fun f : FreeGroup (Sum X Y) →*

134 FreeGroup (Sum X Y) ⧸ N => f z) hhom

135 change (includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y z) :

136 FreeGroup (Sum X Y) ⧸ N) = z at hz

137 exact (QuotientGroup.eq_iff_div_mem

138 (N := N)

139 (x := includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y z))

140 (y := z)).1 hz

141

142/--

143Including the result of trivializing deleted generators is congruent to the original word modulo

144the relators with trivial generators.

145-/

146theorem include_trivializeGeneratorsHom_mod_relatorsWithTrivialGenerators

147 (R : Set (FreeGroup (Sum X Y))) (z : FreeGroup (Sum X Y)) :

148 includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y z) * z⁻¹ ∈

149 Subgroup.normalClosure (relatorsWithTrivialGenerators R) :=

150 Subgroup.normalClosure_mono

151 (fun _ hq => Or.inr hq)

152 (include_trivializeGeneratorsHom_mod_trivialGeneratorRelators

153 (X := X) (Y := Y) z)

154

155/--

156Deleting generators forced to be trivial gives mutual maps between the original presentation and

157the reduced presentation.

158-/

159def deleteTrivialGeneratorsMutualMapData

160 (R : Set (FreeGroup (Sum X Y))) :

161 RelatorQuotientMutualMapData

162 (relatorsWithTrivialGenerators R)

163 (relatorsAfterDeletingTrivialGenerators R) where

164 toHom := trivializeGeneratorsHom X Y

165 invHom := includeAdjoinedGenerators X Y

166 mapsRelators := by

167 intro r hr

168 rcases hr with hr | hr

169 · exact Subgroup.subset_normalClosure ⟨r, hr, rfl⟩

170 · rcases hr with ⟨y, rfl⟩

171 simp only [trivializeGeneratorsHom_inr, one_mem]

172 mapsTargetRelators := by

173 intro s hs

174 rcases hs with ⟨r, hr, rfl⟩

175 let N : Subgroup (FreeGroup (Sum X Y)) :=

176 Subgroup.normalClosure (relatorsWithTrivialGenerators R)

177 have hmod :

178 includeAdjoinedGenerators X Y (trivializeGeneratorsHom X Y r) *

179 r⁻¹ ∈ N :=

180 include_trivializeGeneratorsHom_mod_relatorsWithTrivialGenerators

181 (X := X) (Y := Y) R r

182 have hrN : r ∈ N :=

183 Subgroup.subset_normalClosure

184 (relator_mem_relatorsWithTrivialGenerators (R := R) hr)

185 have hprod := Subgroup.mul_mem N hmod hrN

186 convert hprod using 1

187 group

188 inv_toHom := by

189 intro z

190 exact include_trivializeGeneratorsHom_mod_relatorsWithTrivialGenerators

191 (X := X) (Y := Y) R z

192 to_invHom := by

193 intro z

194 have hcomp := congrArg (fun f : FreeGroup X →* FreeGroup X => f z)

195 (trivializeGeneratorsHom_comp_include (X := X) (Y := Y))

196 have hz :

197 trivializeGeneratorsHom X Y (includeAdjoinedGenerators X Y z) = z := by

198 simpa using hcomp

199 simp only [hz, mul_inv_cancel, one_mem]

200

201/-- Tietze equivalence deleting generators forced to be trivial by the relators \(y = 1\). -/

202def deleteTrivialGeneratorsTietzeEquiv

203 (R : Set (FreeGroup (Sum X Y))) :

204 TietzeEquiv

205 (relatorsWithTrivialGenerators R)

206 (relatorsAfterDeletingTrivialGenerators R) :=

207 TietzeEquiv.ofMutualMapData

208 (deleteTrivialGeneratorsMutualMapData R)

209

210/--

211Tietze move deleting a family of generators that have relators y = 1. Every remaining relator is

212pushed forward by substituting those deleted generators with 1.

213-/

214noncomputable def deleteTrivialGenerators

215 (R : Set (FreeGroup (Sum X Y))) :

216 PresentedGroup (relatorsWithTrivialGenerators R) ≃*

217 PresentedGroup (relatorsAfterDeletingTrivialGenerators R) :=

218 (deleteTrivialGeneratorsTietzeEquiv R).presentedEquiv

219

220end DeleteTrivialGenerators

221

222section DeleteGeneratorsAlongEquiv

223

224variable {Z X Y : Type*}

225

226namespace GeneratorPartition

227

228/-- Generators kept after deleting the generators satisfying `delete`. -/

229def Kept (delete : Z → Prop) : Type _ :=

230 {z : Z // ¬ delete z}

231

232/-- Generators deleted by a predicate `delete`. -/

233def Deleted (delete : Z → Prop) : Type _ :=

234 {z : Z // delete z}

235

236/--

237Split an arbitrary generator type into the generators kept and deleted by a decidable predicate.

238-/

239def equiv (delete : Z → Prop) [DecidablePred delete] :

240 Z ≃ Sum (Kept delete) (Deleted delete) where

241 toFun z :=

242 if hz : delete z then

243 Sum.inr ⟨z, hz⟩

244 else

245 Sum.inl ⟨z, hz⟩

246 invFun z :=

247 match z with

248 | Sum.inl x => x.1

249 | Sum.inr y => y.1

250 left_inv z := by

251 by_cases hz : delete z <;> simp only [hz, ↓reduceDIte]

252 right_inv z := by

253 cases z with

254 | inl x =>

255 simp only [Kept, Deleted, x.property, ↓reduceDIte, Subtype.coe_eta]

256 | inr y =>

257 simp only [Kept, Deleted, y.property, ↓reduceDIte, Subtype.coe_eta]

258

259/-- The partition equivalence sends a generator satisfying the deletion predicate to the

260deleted summand. -/

261@[simp]

262theorem equiv_apply_of_delete

263 (delete : Z → Prop) [DecidablePred delete]

264 {z : Z} (hz : delete z) :

265 equiv delete z = Sum.inr (⟨z, hz⟩ : Deleted delete) := by

266 simp only [equiv, Equiv.coe_fn_mk, hz, ↓reduceDIte]

267 congr

268

269/-- The partition equivalence sends a retained generator to the kept summand. -/

270@[simp]

271theorem equiv_apply_of_not_delete

272 (delete : Z → Prop) [DecidablePred delete]

273 {z : Z} (hz : ¬ delete z) :

274 equiv delete z = Sum.inl (⟨z, hz⟩ : Kept delete) := by

275 simp only [equiv, Equiv.coe_fn_mk, hz, ↓reduceDIte]

276 congr

277

278/-- The inverse partition equivalence forgets the proof attached to a retained generator. -/

279@[simp]

280theorem equiv_symm_inl

281 (delete : Z → Prop) [DecidablePred delete]

282 (z : Kept delete) :

283 (equiv delete).symm (Sum.inl z) = z.1 :=

284 rfl

285

286/-- The inverse partition equivalence forgets the proof attached to a deleted generator. -/

287@[simp]

288theorem equiv_symm_inr

289 (delete : Z → Prop) [DecidablePred delete]

290 (z : Deleted delete) :

291 (equiv delete).symm (Sum.inr z) = z.1 :=

292 rfl

293

294end GeneratorPartition

295

296/--

297Pull back the defining relators \(y = \mathrm{word}(y)\) along an equivalence that splits an

298arbitrary generator type into kept and deleted generators.

299-/

300def definedGeneratorRelatorsAlongEquiv

301 (e : Z ≃ Sum X Y) (word : Y → FreeGroup X) :

302 Set (FreeGroup Z) :=

303 (FreeGroup.freeGroupCongr e).symm ''

304 definedGeneratorRelators (X := X) (Y := Y) word

305

306/--

307Add defining relators to an arbitrary presentation whose generator type is identified with \(X

308\oplus Y\).

309-/

310def relatorsWithDefinedGeneratorsAlongEquiv

311 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)

312 (word : Y → FreeGroup X) :

313 Set (FreeGroup Z) :=

314 R ∪ definedGeneratorRelatorsAlongEquiv e word

315

316/--

317Relators after renaming by \(e\) and substituting every deleted generator \(y : Y\) by

318\(\mathrm{word}(y)\).

319-/

320def relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv

321 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)

322 (word : Y → FreeGroup X) :

323 Set (FreeGroup X) :=

324 relatorsAfterSubstitutingDefinedGenerators

325 (FreeGroup.freeGroupCongr e '' R) word

326

327/--

328Renaming generators carries the pulled-back defining-generator relators to the

329defining-generator relators after the split.

330-/

331theorem freeGroupCongr_image_definedGeneratorRelatorsAlongEquiv

332 (e : Z ≃ Sum X Y) (word : Y → FreeGroup X) :

333 FreeGroup.freeGroupCongr e ''

334 definedGeneratorRelatorsAlongEquiv e word =

335 definedGeneratorRelators (X := X) (Y := Y) word := by

336 ext q

337 constructor

338 · rintro ⟨z, hz, rfl⟩

339 rcases hz with ⟨p, hp, hpz⟩

340 have hpmap :

341 FreeGroup.map (fun z : Z => e z)

342 (FreeGroup.map (fun z : Sum X Y => e.symm z) p) = p := by

343 simpa [FreeGroup.freeGroupCongr] using

344 (FreeGroup.freeGroupCongr e).right_inv p

345 simpa [FreeGroup.freeGroupCongr, ← hpz, hpmap] using hp

346 · intro hq

347 exact ⟨(FreeGroup.freeGroupCongr e).symm q, ⟨q, hq, rfl⟩,

348 (FreeGroup.freeGroupCongr e).right_inv q⟩

349

350/--

351Renaming generators carries the pulled-back relators with defined generators to the

352corresponding split relator set.

353-/

354theorem freeGroupCongr_image_relatorsWithDefinedGeneratorsAlongEquiv

355 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)

356 (word : Y → FreeGroup X) :

357 FreeGroup.freeGroupCongr e ''

358 relatorsWithDefinedGeneratorsAlongEquiv R e word =

359 relatorsWithDefinedGenerators

360 (FreeGroup.freeGroupCongr e '' R) word := by

361 ext q

362 constructor

363 · rintro ⟨z, hz, rfl⟩

364 rcases hz with hz | hz

365 · exact Or.inl ⟨z, hz, rfl⟩

366 · rcases hz with ⟨p, hp, hpz⟩

367 exact Or.inr (by

368 have hpmap :

369 FreeGroup.map (fun z : Z => e z)

370 (FreeGroup.map (fun z : Sum X Y => e.symm z) p) = p := by

371 simpa [FreeGroup.freeGroupCongr] using

372 (FreeGroup.freeGroupCongr e).right_inv p

373 simpa [FreeGroup.freeGroupCongr, ← hpz, hpmap] using hp)

374 · intro hq

375 rcases hq with hq | hq

376 · rcases hq with ⟨z, hz, hzq⟩

377 exact ⟨z, Or.inl hz, hzq⟩

378 · exact ⟨(FreeGroup.freeGroupCongr e).symm q,

379 Or.inr ⟨q, hq, rfl⟩,

380 (FreeGroup.freeGroupCongr e).right_inv q⟩

381

382/--

383Tietze move eliminating an arbitrary family of generators after splitting the generator type by

384an equivalence \(Z \simeq X \oplus Y\).

385-/

386def substituteDefinedGeneratorsAlongEquivTietzeEquiv

387 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)

388 (word : Y → FreeGroup X) :

389 TietzeEquiv

390 (relatorsWithDefinedGeneratorsAlongEquiv R e word)

391 (relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv R e word) :=

392 (renameGeneratorsTietzeEquiv

393 (relatorsWithDefinedGeneratorsAlongEquiv R e word) e).trans

394 ((TietzeEquiv.ofNormalClosureEq

395 (R := FreeGroup.freeGroupCongr e ''

396 relatorsWithDefinedGeneratorsAlongEquiv R e word)

397 (S := relatorsWithDefinedGenerators

398 (FreeGroup.freeGroupCongr e '' R) word)

399 (by

400 rw [freeGroupCongr_image_relatorsWithDefinedGeneratorsAlongEquiv])).trans

401 (substituteDefinedGeneratorsTietzeEquiv

402 (FreeGroup.freeGroupCongr e '' R) word))

403

404/-- Defines `substituteDefinedGeneratorsAlongEquiv`. -/

405noncomputable def substituteDefinedGeneratorsAlongEquiv

406 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)

407 (word : Y → FreeGroup X) :

408 PresentedGroup (relatorsWithDefinedGeneratorsAlongEquiv R e word) ≃*

409 PresentedGroup

410 (relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv R e word) :=

411 (substituteDefinedGeneratorsAlongEquivTietzeEquiv R e word).presentedEquiv

412

413/--

414Add defining relations for all generators satisfying the deletion predicate; the kept generator

415type is the subtype of generators not satisfying that predicate.

416-/

417def definedGeneratorRelatorsOfPredicate

418 (delete : Z → Prop) [DecidablePred delete]

419 (word :

420 GeneratorPartition.Deleted delete →

421 FreeGroup (GeneratorPartition.Kept delete)) :

422 Set (FreeGroup Z) :=

423 definedGeneratorRelatorsAlongEquiv

424 (GeneratorPartition.equiv delete) word

425

426/--

427The relator set obtained by adding defining relators for all generators satisfying the

428predicate.

429-/

430def relatorsWithDefinedGeneratorsOfPredicate

431 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]

432 (word :

433 GeneratorPartition.Deleted delete →

434 FreeGroup (GeneratorPartition.Kept delete)) :

435 Set (FreeGroup Z) :=

436 relatorsWithDefinedGeneratorsAlongEquiv R

437 (GeneratorPartition.equiv delete) word

438

439/--

440Relators obtained after substituting every generator satisfying the predicate by its defining

441word.

442-/

443def relatorsAfterSubstitutingDefinedGeneratorsOfPredicate

444 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]

445 (word :

446 GeneratorPartition.Deleted delete →

447 FreeGroup (GeneratorPartition.Kept delete)) :

448 Set (FreeGroup (GeneratorPartition.Kept delete)) :=

449 relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv R

450 (GeneratorPartition.equiv delete) word

451

452/--

453Tietze equivalence substituting the generators satisfying the predicate by their defining words.

454-/

455def substituteDefinedGeneratorsOfPredicateTietzeEquiv

456 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]

457 (word :

458 GeneratorPartition.Deleted delete →

459 FreeGroup (GeneratorPartition.Kept delete)) :

460 TietzeEquiv

461 (relatorsWithDefinedGeneratorsOfPredicate R delete word)

462 (relatorsAfterSubstitutingDefinedGeneratorsOfPredicate R delete word) :=

463 substituteDefinedGeneratorsAlongEquivTietzeEquiv R

464 (GeneratorPartition.equiv delete) word

465

466/-- Defines `substituteDefinedGeneratorsOfPredicate`. -/

467noncomputable def substituteDefinedGeneratorsOfPredicate

468 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete]

469 (word :

470 GeneratorPartition.Deleted delete →

471 FreeGroup (GeneratorPartition.Kept delete)) :

472 PresentedGroup (relatorsWithDefinedGeneratorsOfPredicate R delete word) ≃*

473 PresentedGroup

474 (relatorsAfterSubstitutingDefinedGeneratorsOfPredicate R delete word) :=

475 (substituteDefinedGeneratorsOfPredicateTietzeEquiv R delete word).presentedEquiv

476

477/--

478Pull back the trivial-generator relators \(y = 1\) along an equivalence that splits an arbitrary

479generator type into kept and deleted generators.

480-/

481def trivialGeneratorRelatorsAlongEquiv

482 (e : Z ≃ Sum X Y) :

483 Set (FreeGroup Z) :=

484 (FreeGroup.freeGroupCongr e).symm ''

485 trivialGeneratorRelators (X := X) (Y := Y)

486

487/--

488Add trivial-generator relators to an arbitrary presentation whose generator type is identified

489with \(X \oplus Y\).

490-/

491def relatorsWithTrivialGeneratorsAlongEquiv

492 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :

493 Set (FreeGroup Z) :=

494 R ∪ trivialGeneratorRelatorsAlongEquiv e

495

496/-- Relators after renaming by \(e\) and deleting every generator in \(Y\). -/

497def relatorsAfterDeletingTrivialGeneratorsAlongEquiv

498 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :

499 Set (FreeGroup X) :=

500 relatorsAfterDeletingTrivialGenerators (FreeGroup.freeGroupCongr e '' R)

501

502/--

503Renaming generators carries the pulled-back trivial-generator relators to the trivial-generator

504relators after the split.

505-/

506theorem freeGroupCongr_image_trivialGeneratorRelatorsAlongEquiv

507 (e : Z ≃ Sum X Y) :

508 FreeGroup.freeGroupCongr e ''

509 trivialGeneratorRelatorsAlongEquiv (X := X) (Y := Y) e =

510 trivialGeneratorRelators (X := X) (Y := Y) := by

511 ext q

512 constructor

513 · rintro ⟨z, hz, rfl⟩

514 rcases hz with ⟨p, hp, hpz⟩

515 have hpmap :

516 FreeGroup.map (fun z : Z => e z)

517 (FreeGroup.map (fun z : Sum X Y => e.symm z) p) = p := by

518 simpa [FreeGroup.freeGroupCongr] using

519 (FreeGroup.freeGroupCongr e).right_inv p

520 simpa [FreeGroup.freeGroupCongr, ← hpz, hpmap] using hp

521 · intro hq

522 exact ⟨(FreeGroup.freeGroupCongr e).symm q, ⟨q, hq, rfl⟩,

523 (FreeGroup.freeGroupCongr e).right_inv q⟩

524

525/--

526Renaming generators carries the pulled-back relators with trivial generators to the

527corresponding split relator set.

528-/

529theorem freeGroupCongr_image_relatorsWithTrivialGeneratorsAlongEquiv

530 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :

531 FreeGroup.freeGroupCongr e ''

532 relatorsWithTrivialGeneratorsAlongEquiv R e =

533 relatorsWithTrivialGenerators (FreeGroup.freeGroupCongr e '' R) := by

534 ext q

535 constructor

536 · rintro ⟨z, hz, rfl⟩

537 rcases hz with hz | hz

538 · exact Or.inl ⟨z, hz, rfl⟩

539 · rcases hz with ⟨p, hp, hpz⟩

540 exact Or.inr (by

541 have hpmap :

542 FreeGroup.map (fun z : Z => e z)

543 (FreeGroup.map (fun z : Sum X Y => e.symm z) p) = p := by

544 simpa [FreeGroup.freeGroupCongr] using

545 (FreeGroup.freeGroupCongr e).right_inv p

546 simpa [FreeGroup.freeGroupCongr, ← hpz, hpmap] using hp)

547 · intro hq

548 rcases hq with hq | hq

549 · rcases hq with ⟨z, hz, hzq⟩

550 exact ⟨z, Or.inl hz, hzq⟩

551 · exact ⟨(FreeGroup.freeGroupCongr e).symm q,

552 Or.inr ⟨q, hq, rfl⟩,

553 (FreeGroup.freeGroupCongr e).right_inv q⟩

554

555/--

556Tietze move deleting an arbitrary family of generators after splitting the generator type by an

557equivalence \(Z \simeq X \oplus Y\).

558-/

559def deleteTrivialGeneratorsAlongEquivTietzeEquiv

560 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :

561 TietzeEquiv

562 (relatorsWithTrivialGeneratorsAlongEquiv R e)

563 (relatorsAfterDeletingTrivialGeneratorsAlongEquiv R e) :=

564 (renameGeneratorsTietzeEquiv

565 (relatorsWithTrivialGeneratorsAlongEquiv R e) e).trans

566 ((TietzeEquiv.ofNormalClosureEq

567 (R := FreeGroup.freeGroupCongr e ''

568 relatorsWithTrivialGeneratorsAlongEquiv R e)

569 (S := relatorsWithTrivialGenerators

570 (FreeGroup.freeGroupCongr e '' R))

571 (by

572 rw [freeGroupCongr_image_relatorsWithTrivialGeneratorsAlongEquiv])).trans

573 (deleteTrivialGeneratorsTietzeEquiv

574 (FreeGroup.freeGroupCongr e '' R)))

575

576/-- Defines `deleteTrivialGeneratorsAlongEquiv`. -/

577noncomputable def deleteTrivialGeneratorsAlongEquiv

578 (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :

579 PresentedGroup (relatorsWithTrivialGeneratorsAlongEquiv R e) ≃*

580 PresentedGroup

581 (relatorsAfterDeletingTrivialGeneratorsAlongEquiv R e) :=

582 (deleteTrivialGeneratorsAlongEquivTietzeEquiv R e).presentedEquiv

583

584/-- Trivial-generator relators for the generators satisfying the deletion predicate. -/

585def trivialGeneratorRelatorsOfPredicate

586 (delete : Z → Prop) [DecidablePred delete] :

587 Set (FreeGroup Z) :=

588 trivialGeneratorRelatorsAlongEquiv

589 (X := GeneratorPartition.Kept delete)

590 (Y := GeneratorPartition.Deleted delete)

591 (GeneratorPartition.equiv delete)

592

593/--

594The relator set obtained by adding trivial-generator relators for all generators satisfying the

595predicate.

596-/

597def relatorsWithTrivialGeneratorsOfPredicate

598 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :

599 Set (FreeGroup Z) :=

600 relatorsWithTrivialGeneratorsAlongEquiv R

601 (X := GeneratorPartition.Kept delete)

602 (Y := GeneratorPartition.Deleted delete)

603 (GeneratorPartition.equiv delete)

604

605/--

606Relators obtained after deleting every generator satisfying the predicate by substituting it

607with \(1\).

608-/

609def relatorsAfterDeletingTrivialGeneratorsOfPredicate

610 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :

611 Set (FreeGroup (GeneratorPartition.Kept delete)) :=

612 relatorsAfterDeletingTrivialGeneratorsAlongEquiv R

613 (X := GeneratorPartition.Kept delete)

614 (Y := GeneratorPartition.Deleted delete)

615 (GeneratorPartition.equiv delete)

616

617/-- Tietze equivalence deleting the generators satisfying the chosen predicate. -/

618def deleteTrivialGeneratorsOfPredicateTietzeEquiv

619 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :

620 TietzeEquiv

621 (relatorsWithTrivialGeneratorsOfPredicate R delete)

622 (relatorsAfterDeletingTrivialGeneratorsOfPredicate R delete) :=

623 deleteTrivialGeneratorsAlongEquivTietzeEquiv R

624 (X := GeneratorPartition.Kept delete)

625 (Y := GeneratorPartition.Deleted delete)

626 (GeneratorPartition.equiv delete)

627

628/-- Defines `deleteTrivialGeneratorsOfPredicate`. -/

629noncomputable def deleteTrivialGeneratorsOfPredicate

630 (R : Set (FreeGroup Z)) (delete : Z → Prop) [DecidablePred delete] :

631 PresentedGroup (relatorsWithTrivialGeneratorsOfPredicate R delete) ≃*

632 PresentedGroup

633 (relatorsAfterDeletingTrivialGeneratorsOfPredicate R delete) :=

634 (deleteTrivialGeneratorsOfPredicateTietzeEquiv R delete).presentedEquiv

635

636end DeleteGeneratorsAlongEquiv

637

638end AdjoinGenerators

639

640end Presented

641

642end ReidemeisterSchreier.Discrete.Presentations