Yamaguchi Lean 4 Library
ProCGroups/Presentations/SchreierTietze/Data.lean
ProCGroups/Presentations/SchreierTietze/Data/Source

ProCGroups/Presentations/SchreierTietze/Data.lean

1import ProCGroups.Presentations.SchreierTietze.Restricted
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/Presentations/SchreierTietze/Data.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Profinite presentations
14Presentation-level API for profinite groups, finite quotients, relators, and Schreier-Tietze restrictions.
15-/
17noncomputable section
19open scoped Topology
21namespace ProCGroups.Presentations
23universe u v w
27variable (C : ProCGroups.FiniteGroupClass.{u})
28variable {E F G : Type u} [Group E] [Group F] [Group G]
29variable [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G]
30variable [IsTopologicalGroup E] [IsTopologicalGroup F] [IsTopologicalGroup G]
32/-- The presentation map to an open-subgroup target after a proposed Schreier source
33maps into the source preimage. -/
35 (π : F →ₜ* G) (U : Subgroup G)
36 (α : E →ₜ* presentationSubgroupPreimage π U) : E →ₜ* U :=
39/-- The same map, specialized to an open subgroup target. -/
41 (π : F →ₜ* G) (U : OpenSubgroup G)
42 (α : E →ₜ* presentationSubgroupPreimage π (U : Subgroup G)) :
43 E →ₜ* ↥(U : Subgroup G) :=
44 schreierPresentationHom π (U : Subgroup G) α
46/-- Abstract profinite Reidemeister-Schreier presentation data.
48Here `E` is the proposed source on Schreier generators, `R` is the raw or cleaned
49set of rewritten relators in `E`, and `α` is the continuous map from `E` to
50`π⁻¹(U)`. A concrete rewriting construction proves the two recorded facts:
51surjectivity onto `U` and equality of the kernel with the closed normal closure
52of the rewritten relators. -/
54 (π : F →ₜ* G) (U : Subgroup G) (R : Set E) where
55 targetProC : ProCGroups.ProC.IsProCGroup C U
56 sourceToPreimage : E →ₜ* presentationSubgroupPreimage π U
57 sourceToOpen_surjective :
58 Function.Surjective (schreierPresentationHom π U sourceToPreimage)
60 (schreierPresentationHom π U sourceToPreimage).toMonoidHom.ker =
61 closedNormalClosure R
63/-- Open-subgroup Schreier presentation data with the rewriting map, surjectivity, and kernel
64identity recorded explicitly. -/
66 (π : F →ₜ* G) (U : OpenSubgroup G) (R : Set E) where
67 sourceToPreimage : E →ₜ* presentationSubgroupPreimage π (U : Subgroup G)
68 sourceToOpen_surjective :
69 Function.Surjective (openSchreierPresentationHom π U sourceToPreimage)
71 (openSchreierPresentationHom π U sourceToPreimage).toMonoidHom.ker =
72 closedNormalClosure R
76variable {C}
77variable {π : F →ₜ* G} {U : Subgroup G} {R S D : Set E}
79omit [IsTopologicalGroup F] in
80theorem isRelatorPresentationOf
82 IsRelatorPresentationOf C (F := E) (G := U) R := by
83 exact ⟨D.targetProC, schreierPresentationHom π U D.sourceToPreimage,
84 D.sourceToOpen_surjective, D.kernel_eq_closedNormalClosure⟩
86def clean
88 (T : RelatorTietzeData R S) :
90 targetProC := D.targetProC
91 sourceToPreimage := D.sourceToPreimage
92 sourceToOpen_surjective := D.sourceToOpen_surjective
94 simpa [T.closedNormalClosure_eq] using D.kernel_eq_closedNormalClosure
96def delete_redundant_relators
97 (Ddata : SchreierRelatorPresentationData C π U (R ∪ D))
98 (hD : D ⊆ closedNormalClosure R) :
100 targetProC := Ddata.targetProC
101 sourceToPreimage := Ddata.sourceToPreimage
102 sourceToOpen_surjective := Ddata.sourceToOpen_surjective
104 simpa [closedNormalClosure_union_eq_left (F := E) hD] using
105 Ddata.kernel_eq_closedNormalClosure
107def add_redundant_relators
109 (hD : D ⊆ closedNormalClosure R) :
111 targetProC := Ddata.targetProC
112 sourceToPreimage := Ddata.sourceToPreimage
113 sourceToOpen_surjective := Ddata.sourceToOpen_surjective
115 simpa [closedNormalClosure_union_eq_left (F := E) hD] using
116 Ddata.kernel_eq_closedNormalClosure
118def delete_trivial_relators
119 (Ddata : SchreierRelatorPresentationData C π U (R ∪ D))
120 (hD : D ⊆ ({1} : Set E)) :
122 Ddata.delete_redundant_relators
125def add_trivial_relators
127 (hD : D ⊆ ({1} : Set E)) :
129 Ddata.add_redundant_relators
132def delete_degenerate_schreier_relators
135 (H : ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData T) :
137 Ddata.clean H.relatorTietze_raw_rewritten
139def clean_schreier_relators
142 (H : ProfiniteSchreierRelatorSets.CleaningData T) :
144 Ddata.clean H.relatorTietze_raw_cleaned
150variable {C}
151variable {π : F →ₜ* G} {U : OpenSubgroup G} {R S D : Set E}
153def targetProC
155 (hG : ProCGroups.ProC.IsProCGroup C G) :
156 ProCGroups.ProC.IsProCGroup C ↥(U : Subgroup G) := by
157 have hUclosed : IsClosed (((U : Subgroup G) : Set G)) :=
160 hC hG (U : Subgroup G) hUclosed
165 (hG : ProCGroups.ProC.IsProCGroup C G) :
166 SchreierRelatorPresentationData C π (U : Subgroup G) R where
167 targetProC := targetProC (C := C) (U := U) hC hG
168 sourceToPreimage := Ddata.sourceToPreimage
169 sourceToOpen_surjective := Ddata.sourceToOpen_surjective
170 kernel_eq_closedNormalClosure := Ddata.kernel_eq_closedNormalClosure
172omit [IsTopologicalGroup F] in
173theorem isRelatorPresentationOf
176 (hG : ProCGroups.ProC.IsProCGroup C G) :
177 IsRelatorPresentationOf C (F := E) (G := ↥(U : Subgroup G)) R :=
178 (Ddata.toSchreierRelatorPresentationData hC hG).isRelatorPresentationOf
180theorem isRelatorPresentationOf_of_ambientPresentation
181 {R₀ : Set F}
184 (hambient : IsRelatorPresentationOf C (F := F) (G := G) R₀) :
185 IsRelatorPresentationOf C (F := E) (G := ↥(U : Subgroup G)) R :=
186 Ddata.isRelatorPresentationOf hC hambient.1
188def clean
192 sourceToPreimage := Ddata.sourceToPreimage
193 sourceToOpen_surjective := Ddata.sourceToOpen_surjective
195 simpa [T.closedNormalClosure_eq] using Ddata.kernel_eq_closedNormalClosure
197def delete_redundant_relators
199 (hD : D ⊆ closedNormalClosure R) :
201 sourceToPreimage := Ddata.sourceToPreimage
202 sourceToOpen_surjective := Ddata.sourceToOpen_surjective
204 simpa [closedNormalClosure_union_eq_left (F := E) hD] using
205 Ddata.kernel_eq_closedNormalClosure
207def add_redundant_relators
209 (hD : D ⊆ closedNormalClosure R) :
211 sourceToPreimage := Ddata.sourceToPreimage
212 sourceToOpen_surjective := Ddata.sourceToOpen_surjective
214 simpa [closedNormalClosure_union_eq_left (F := E) hD] using
215 Ddata.kernel_eq_closedNormalClosure
217def delete_trivial_relators
219 (hD : D ⊆ ({1} : Set E)) :
221 Ddata.delete_redundant_relators
224def add_trivial_relators
226 (hD : D ⊆ ({1} : Set E)) :
228 Ddata.add_redundant_relators
231def delete_degenerate_schreier_relators
234 (H : ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData T) :
236 Ddata.clean H.relatorTietze_raw_rewritten
238def clean_schreier_relators
241 (H : ProfiniteSchreierRelatorSets.CleaningData T) :
243 Ddata.clean H.relatorTietze_raw_cleaned
246 {R₀ : Set F} {T : ProfiniteSchreierRelatorSets E}
248 (H : ProfiniteSchreierRelatorSets.CleaningData T)
250 (hambient : IsRelatorPresentationOf C (F := F) (G := G) R₀) :
251 IsRelatorPresentationOf C (F := E) (G := ↥(U : Subgroup G)) T.cleaned :=
252 (Ddata.clean_schreier_relators H).isRelatorPresentationOf hC hambient.1
256section StandardPresentationData
258variable {Eₛ : Type u} [Group Eₛ] [TopologicalSpace Eₛ] [IsTopologicalGroup Eₛ]
260/-- A standard-form Schreier presentation package when the final Tietze step may change the
261presentation source, as in deletion of redundant Schreier generators. -/
263 (π : F →ₜ* G) (U : Subgroup G)
264 (rawRelators : Set E) (standardRelators : Set Eₛ) where
265 rawData : SchreierRelatorPresentationData C π U rawRelators
266 standardTietze : RelatorMapTietzeData rawRelators standardRelators
270variable {C}
271variable {π : F →ₜ* G} {U : Subgroup G}
272variable {rawRelators : Set E} {standardRelators : Set Eₛ}
274omit [IsTopologicalGroup F] in
275theorem isRelatorPresentationOf
276 (D : SchreierStandardPresentationData C π U rawRelators standardRelators) :
277 IsRelatorPresentationOf C (F := Eₛ) (G := U) standardRelators :=
278 D.standardTietze.presentation (C := C) (G := U) D.rawData.isRelatorPresentationOf
280def ofCleaningData
283 (H : ProfiniteSchreierRelatorSets.CleaningData T) :
284 SchreierStandardPresentationData C π U T.raw T.cleaned where
285 rawData := Ddata
286 standardTietze :=
287 RelatorMapTietzeData.ofRelatorTietzeData H.relatorTietze_raw_cleaned
291/-- Standard-form data for an open subgroup, consisting of a raw Schreier presentation datum and
292a Tietze datum from the raw source to the final standard source. -/
294 (π : F →ₜ* G) (U : OpenSubgroup G)
295 (rawRelators : Set E) (standardRelators : Set Eₛ) where
297 standardTietze : RelatorMapTietzeData rawRelators standardRelators
301variable {C}
302variable {π : F →ₜ* G} {U : OpenSubgroup G}
303variable {rawRelators : Set E} {standardRelators : Set Eₛ}
305omit [IsTopologicalGroup F] in
306theorem isRelatorPresentationOf
307 (D : OpenSubgroupSchreierStandardPresentationData π U rawRelators standardRelators)
309 (hG : ProCGroups.ProC.IsProCGroup C G) :
310 IsRelatorPresentationOf C (F := Eₛ) (G := ↥(U : Subgroup G)) standardRelators :=
311 D.standardTietze.presentation (C := C) (G := ↥(U : Subgroup G))
312 (D.rawData.isRelatorPresentationOf hC hG)
314theorem isRelatorPresentationOf_of_ambientPresentation
315 {R₀ : Set F}
316 (D : OpenSubgroupSchreierStandardPresentationData π U rawRelators standardRelators)
318 (hambient : IsRelatorPresentationOf C (F := F) (G := G) R₀) :
319 IsRelatorPresentationOf C (F := Eₛ) (G := ↥(U : Subgroup G)) standardRelators :=
320 D.isRelatorPresentationOf hC hambient.1
323 {X : Type u} [TopologicalSpace X] {ι : X → F} {R₀ : Set F}
324 (D : OpenSubgroupSchreierStandardPresentationData π U rawRelators standardRelators)
326 (hambient : IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι R₀) :
327 IsRelatorPresentationOf C (F := Eₛ) (G := ↥(U : Subgroup G)) standardRelators :=
328 D.isRelatorPresentationOf hC
329 (IsFreeRelatorPresentationOfClass.isRelatorPresentationOf (C := C) (G := G) hambient).1
331def ofCleaningData
334 (H : ProfiniteSchreierRelatorSets.CleaningData T) :
336 rawData := Ddata
337 standardTietze :=
338 RelatorMapTietzeData.ofRelatorTietzeData H.relatorTietze_raw_cleaned
340omit [IsTopologicalGroup F] in
344 (H : ProfiniteSchreierRelatorSets.CleaningData T)
346 (hG : ProCGroups.ProC.IsProCGroup C G) :
347 IsRelatorPresentationOf C (F := E) (G := ↥(U : Subgroup G)) T.cleaned :=
348 (ofCleaningData Ddata H).isRelatorPresentationOf hC hG
351 {X : Type u} [TopologicalSpace X] {ι : X → F} {R₀ : Set F}
354 (H : ProfiniteSchreierRelatorSets.CleaningData T)
356 (hambient : IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι R₀) :
357 IsRelatorPresentationOf C (F := E) (G := ↥(U : Subgroup G)) T.cleaned :=
359 hC hambient
363section FreeSourcePresentationData
365variable {Y Yₛ : Type u} [TopologicalSpace Y] [TopologicalSpace Yₛ]
366variable {η : Y → E} {ηₛ : Yₛ → Eₛ}
368/-- A Schreier relator-presentation datum whose source is explicitly the free pro-`C` group on
369the chosen Schreier generators. This is the direct formal shape of
370`U = ⟨Schreier generators | rewritten relators⟩_{pro-C}`. -/
372 (η : Y → E) (π : F →ₜ* G) (U : Subgroup G) (R : Set E) where
380variable {C}
381variable {π : F →ₜ* G} {U : Subgroup G} {R S D : Set E}
383omit [IsTopologicalGroup F] in
384theorem isFreeRelatorPresentationOfClass
386 IsFreeRelatorPresentationOfClass C (F := E) (G := U) η R := by
387 exact ⟨Ddata.freeSource, by simpa using Ddata.relatorData.targetProC,
388 schreierPresentationHom π U Ddata.relatorData.sourceToPreimage,
389 Ddata.relatorData.sourceToOpen_surjective,
390 Ddata.relatorData.kernel_eq_closedNormalClosure⟩
392omit [IsTopologicalGroup F] in
393theorem isRelatorPresentationOf
395 IsRelatorPresentationOf C (F := E) (G := U) R :=
396 Ddata.isFreeRelatorPresentationOfClass.isRelatorPresentationOf
398def clean
402 freeSource := Ddata.freeSource
403 relatorData := Ddata.relatorData.clean T
405def delete_redundant_relators
406 (Ddata : SchreierFreeRelatorPresentationData C η π U (R ∪ D))
407 (hD : D ⊆ closedNormalClosure R) :
409 freeSource := Ddata.freeSource
410 relatorData := Ddata.relatorData.delete_redundant_relators hD
412def delete_trivial_relators
413 (Ddata : SchreierFreeRelatorPresentationData C η π U (R ∪ D))
414 (hD : D ⊆ ({1} : Set E)) :
416 freeSource := Ddata.freeSource
417 relatorData := Ddata.relatorData.delete_trivial_relators hD
419def delete_degenerate_schreier_relators
422 (H : ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData T) :
424 Ddata.clean H.relatorTietze_raw_rewritten
426def clean_schreier_relators
429 (H : ProfiniteSchreierRelatorSets.CleaningData T) :
431 Ddata.clean H.relatorTietze_raw_cleaned
435/-- The open-subgroup version of `SchreierFreeRelatorPresentationData`. The open subgroup is
436shown to be pro-`C` from the ambient presentation and full-formation hypothesis. -/
438 (η : Y → E) (π : F →ₜ* G) (U : OpenSubgroup G) (R : Set E) where
446variable {C}
447variable {π : F →ₜ* G} {U : OpenSubgroup G} {R S D : Set E}
449omit [IsTopologicalGroup F] in
450theorem isFreeRelatorPresentationOfClass
453 (hG : ProCGroups.ProC.IsProCGroup C G) :
454 IsFreeRelatorPresentationOfClass C (F := E) (G := ↥(U : Subgroup G)) η R := by
455 have hU : ProCGroups.ProC.IsProCGroup C ↥(U : Subgroup G) :=
456 OpenSubgroupSchreierRelatorPresentationData.targetProC (C := C) (U := U) hC hG
457 exact ⟨Ddata.freeSource, by simpa using hU,
458 openSchreierPresentationHom π U Ddata.relatorData.sourceToPreimage,
459 Ddata.relatorData.sourceToOpen_surjective,
460 Ddata.relatorData.kernel_eq_closedNormalClosure⟩
463 {R₀ : Set F}
466 (hambient : IsRelatorPresentationOf C (F := F) (G := G) R₀) :
467 IsFreeRelatorPresentationOfClass C (F := E) (G := ↥(U : Subgroup G)) η R :=
468 Ddata.isFreeRelatorPresentationOfClass hC hambient.1
470theorem isFreeRelatorPresentationOfClass_of_ambientFreeRelatorPresentation
471 {X : Type u} [TopologicalSpace X] {ι : X → F} {R₀ : Set F}
474 (hambient : IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι R₀) :
475 IsFreeRelatorPresentationOfClass C (F := E) (G := ↥(U : Subgroup G)) η R :=
476 Ddata.isFreeRelatorPresentationOfClass hC
477 (IsFreeRelatorPresentationOfClass.isRelatorPresentationOf
478 (C := C) (G := G) hambient).1
480def clean
484 freeSource := Ddata.freeSource
485 relatorData := Ddata.relatorData.clean T
487def delete_redundant_relators
489 (hD : D ⊆ closedNormalClosure R) :
491 freeSource := Ddata.freeSource
492 relatorData := Ddata.relatorData.delete_redundant_relators hD
494def delete_trivial_relators
496 (hD : D ⊆ ({1} : Set E)) :
498 freeSource := Ddata.freeSource
499 relatorData := Ddata.relatorData.delete_trivial_relators hD
501def delete_degenerate_schreier_relators
504 (H : ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData T) :
506 Ddata.clean H.relatorTietze_raw_rewritten
508def clean_schreier_relators
511 (H : ProfiniteSchreierRelatorSets.CleaningData T) :
513 Ddata.clean H.relatorTietze_raw_cleaned
515theorem cleanedFreeRelatorPresentationOf_of_ambientFreeRelatorPresentation
516 {X : Type u} [TopologicalSpace X] {ι : X → F} {R₀ : Set F}
519 (H : ProfiniteSchreierRelatorSets.CleaningData T)
521 (hambient : IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι R₀) :
522 IsFreeRelatorPresentationOfClass C (F := E) (G := ↥(U : Subgroup G)) η T.cleaned :=
523 (Ddata.clean_schreier_relators H)
524 |>.isFreeRelatorPresentationOfClass_of_ambientFreeRelatorPresentation hC hambient
528/-- Standard-form free Schreier presentation data. The final source is explicitly free on the
529surviving Schreier generators after generator deletion. -/
531 (ηₛ : Yₛ → Eₛ) (π : F →ₜ* G) (U : OpenSubgroup G)
532 (rawRelators : Set E) (standardRelators : Set Eₛ) where
533 freeStandardSource :
536 standardData :
537 OpenSubgroupSchreierStandardPresentationData π U rawRelators standardRelators
541variable {C}
542variable {π : F →ₜ* G} {U : OpenSubgroup G}
543variable {rawRelators : Set E} {standardRelators : Set Eₛ}
545omit [IsTopologicalGroup F] in
546theorem isFreeRelatorPresentationOfClass
548 C ηₛ π U rawRelators standardRelators)
550 (hG : ProCGroups.ProC.IsProCGroup C G) :
552 (F := Eₛ) (G := ↥(U : Subgroup G)) ηₛ standardRelators := by
553 rcases D.standardData.isRelatorPresentationOf hC hG with
554 ⟨hU, ρ, hρsurj, hρker⟩
555 exact ⟨D.freeStandardSource, by simpa using hU, ρ, hρsurj, hρker⟩
557theorem isFreeRelatorPresentationOfClass_of_ambientFreeRelatorPresentation
558 {X : Type u} [TopologicalSpace X] {ι : X → F} {R₀ : Set F}
560 C ηₛ π U rawRelators standardRelators)
562 (hambient : IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι R₀) :
564 (F := Eₛ) (G := ↥(U : Subgroup G)) ηₛ standardRelators :=
565 D.isFreeRelatorPresentationOfClass hC
566 (IsFreeRelatorPresentationOfClass.isRelatorPresentationOf
567 (C := C) (G := G) hambient).1
571section RewritingFreeSourcePresentationData
573variable {Q : Type v}
576/-- Open-subgroup free Schreier presentation data whose rewritten relators are definitionally
577constructed from a map `tau`. -/
579 (η : Y → E) (π : F →ₜ* G) (U : OpenSubgroup G)
584 relatorData :
589variable {C}
590variable {π : F →ₜ* G} {U : OpenSubgroup G}
594 OpenSubgroupSchreierFreeRelatorPresentationData C η π U Srw.toRelatorSets.raw where
595 freeSource := Ddata.freeSource
596 relatorData := Ddata.relatorData
599 {X : Type u} [TopologicalSpace X] {ι : X → F}
602 (hambient :
603 IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι Srw.originalRelators) :
605 (F := E) (G := ↥(U : Subgroup G)) η Srw.toRelatorSets.raw :=
606 Ddata.toRawFreeRelatorPresentationData
607 |>.isFreeRelatorPresentationOfClass_of_ambientFreeRelatorPresentation hC hambient
610 {X : Type u} [TopologicalSpace X] {ι : X → F}
612 (H : ProfiniteSchreierRewritingRelatorSets.DegenerateRelatorDeletionData Srw)
614 (hambient :
615 IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι Srw.originalRelators) :
617 (F := E) (G := ↥(U : Subgroup G)) η Srw.toRelatorSets.rewritten :=
618 (Ddata.toRawFreeRelatorPresentationData.delete_degenerate_schreier_relators H)
619 |>.isFreeRelatorPresentationOfClass_of_ambientFreeRelatorPresentation hC hambient
621theorem cleanedFreeRelatorPresentationOf_of_ambientFreeRelatorPresentation
622 {X : Type u} [TopologicalSpace X] {ι : X → F}
624 (H : ProfiniteSchreierRewritingRelatorSets.CleaningData Srw)
626 (hambient :
627 IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι Srw.originalRelators) :
629 (F := E) (G := ↥(U : Subgroup G)) η Srw.toRelatorSets.cleaned :=
630 (Ddata.toRawFreeRelatorPresentationData.clean_schreier_relators H)
631 |>.isFreeRelatorPresentationOfClass_of_ambientFreeRelatorPresentation hC hambient
635/-- Standard-form free Schreier presentation data whose raw relators are built from `tau`. The
636standard source may differ from the raw source after deleting redundant Schreier generators. -/
638 (ηₛ : Yₛ → Eₛ) (π : F →ₜ* G) (U : OpenSubgroup G)
640 (standardRelators : Set Eₛ) where
641 freeStandardSource :
644 standardData :
645 OpenSubgroupSchreierStandardPresentationData π U Srw.toRelatorSets.raw standardRelators
649variable {C}
650variable {π : F →ₜ* G} {U : OpenSubgroup G}
651variable {standardRelators : Set Eₛ}
655 C ηₛ π U Srw standardRelators) :
657 C ηₛ π U Srw.toRelatorSets.raw standardRelators where
658 freeStandardSource := D.freeStandardSource
659 standardData := D.standardData
661theorem isFreeRelatorPresentationOfClass_of_ambientFreeRelatorPresentation
662 {X : Type u} [TopologicalSpace X] {ι : X → F}
664 C ηₛ π U Srw standardRelators)
666 (hambient :
667 IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι Srw.originalRelators) :
669 (F := Eₛ) (G := ↥(U : Subgroup G)) ηₛ standardRelators :=
670 D.toStandardFreeRelatorPresentationData
671 |>.isFreeRelatorPresentationOfClass_of_ambientFreeRelatorPresentation hC hambient
675end RewritingFreeSourcePresentationData
677end FreeSourcePresentationData
679end StandardPresentationData
683end ProCGroups.Presentations