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

ProCGroups/Presentations/SchreierTietze/Relators.lean

1import ProCGroups.Presentations.Profinite
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/Presentations/SchreierTietze/Relators.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
25section RelatorIndexing
27variable {F : Type u}
29/-- The relator set represented by an indexed family. This is the profinite analogue of the
30``relator family'' notation used in Reidemeister-Schreier/Tietze arguments. -/
31def relatorFamilySet {ι : Sort v} (r : ι → F) : Set F :=
32 Set.range r
34@[simp] theorem mem_relatorFamilySet {ι : Sort v} (r : ι → F) (x : F) :
35 x ∈ relatorFamilySet r ↔ ∃ i, r i = x :=
36 Iff.rfl
38/-- The relator set represented by a finite list. This avoids quotienting the list by
39permutation; order and repetitions are syntactic data, while the closed normal closure only sees
40the induced set. -/
41def relatorListSet (l : List F) : Set F :=
42 {x | x ∈ l}
44@[simp] theorem mem_relatorListSet (l : List F) (x : F) :
45 x ∈ relatorListSet l ↔ x ∈ l :=
46 Iff.rfl
48@[simp] theorem relatorListSet_nil :
49 relatorListSet ([] : List F) = (∅ : Set F) := by
50 ext x
51 simp only [relatorListSet, List.not_mem_nil, Set.setOf_false, Set.mem_empty_iff_false]
53@[simp] theorem relatorListSet_cons (x : F) (l : List F) :
54 relatorListSet (x :: l) = ({x} : Set F) ∪ relatorListSet l := by
55 ext y
56 simp only [relatorListSet, List.mem_cons, Set.mem_setOf_eq, Set.singleton_union, Set.mem_insert_iff]
58@[simp] theorem relatorListSet_append (l m : List F) :
60 ext x
61 simp only [relatorListSet, List.mem_append, Set.mem_setOf_eq, Set.mem_union]
63/-- The relator set represented by a finset. -/
64def relatorFinsetSet (s : Finset F) : Set F :=
65 {x | x ∈ s}
67@[simp] theorem mem_relatorFinsetSet (s : Finset F) (x : F) :
68 x ∈ relatorFinsetSet s ↔ x ∈ s :=
69 Iff.rfl
71@[simp] theorem relatorFinsetSet_empty :
72 relatorFinsetSet (∅ : Finset F) = (∅ : Set F) := by
73 ext x
74 simp only [relatorFinsetSet, Finset.notMem_empty, Set.setOf_false, Set.mem_empty_iff_false]
76@[simp] theorem relatorFinsetSet_insert [DecidableEq F] (x : F) (s : Finset F) :
77 relatorFinsetSet (insert x s) = ({x} : Set F) ∪ relatorFinsetSet s := by
78 ext y
79 simp only [relatorFinsetSet, Finset.mem_insert, Set.mem_setOf_eq, SetLike.setOf_mem_eq, Set.singleton_union,
80 Set.mem_insert_iff, SetLike.mem_coe]
82@[simp] theorem relatorFinsetSet_union [DecidableEq F] (s t : Finset F) :
84 ext x
85 simp only [relatorFinsetSet, Finset.mem_union, Set.mem_setOf_eq, SetLike.setOf_mem_eq, Set.mem_union,
86 SetLike.mem_coe]
88/-- The relator set obtained from a Schreier rewriting map `τ`, a family of transversal labels,
89and a family of original relators. This is the profinite/presentation-level spelling of
90`{ τ(t,r) | t ∈ T, r ∈ R }`. -/
91def schreierRelatorSet {Q : Type v} {A : Type w}
92 (τ : Q → A → F) (T : Set Q) (R : Set A) : Set F :=
93 {x | ∃ t ∈ T, ∃ r ∈ R, τ t r = x}
95@[simp] theorem mem_schreierRelatorSet
96 {Q : Type v} {A : Type w}
97 (τ : Q → A → F) (T : Set Q) (R : Set A) (x : F) :
98 x ∈ schreierRelatorSet τ T R ↔ ∃ t ∈ T, ∃ r ∈ R, τ t r = x :=
99 Iff.rfl
101/-- List version of a Schreier rewritten relator family. -/
102def schreierRelatorList {Q : Type v} {A : Type w}
103 (τ : Q → A → F) : List Q → List A → List F
104 | [], _ => []
105 | t :: ts, rs => rs.map (τ t) ++ schreierRelatorList τ ts rs
108 {Q : Type v} {A : Type w}
109 (τ : Q → A → F) (ts : List Q) (rs : List A) (x : F) :
110 x ∈ schreierRelatorList τ ts rs ↔ ∃ t ∈ ts, ∃ r ∈ rs, τ t r = x := by
111 induction ts with
112 | nil =>
113 simp only [schreierRelatorList, List.not_mem_nil, false_and, exists_false]
114 | cons t ts ih =>
115 simp only [schreierRelatorList, List.mem_append, List.mem_map, ih, List.mem_cons, exists_eq_or_imp]
118 {Q : Type v} {A : Type w}
119 (τ : Q → A → F) (ts : List Q) (rs : List A) :
122 ext x
125/-- Finset version of a Schreier rewritten relator family. -/
126def schreierRelatorFinset {Q : Type v} {A : Type w} [DecidableEq F]
127 (τ : Q → A → F) (ts : Finset Q) (rs : Finset A) : Finset F :=
128 ts.biUnion fun t => rs.image (τ t)
130@[simp] theorem mem_schreierRelatorFinset
131 {Q : Type v} {A : Type w} [DecidableEq F]
132 (τ : Q → A → F) (ts : Finset Q) (rs : Finset A) (x : F) :
133 x ∈ schreierRelatorFinset τ ts rs ↔ ∃ t ∈ ts, ∃ r ∈ rs, τ t r = x := by
134 simp only [schreierRelatorFinset, Finset.mem_biUnion, Finset.mem_image]
137 {Q : Type v} {A : Type w} [DecidableEq F]
138 (τ : Q → A → F) (ts : Finset Q) (rs : Finset A) :
139 relatorFinsetSet (schreierRelatorFinset τ ts rs) =
141 ext x
142 simp only [mem_relatorFinsetSet, mem_schreierRelatorFinset, schreierRelatorSet, Set.mem_setOf_eq]
144end RelatorIndexing
146section RelatorPresentations
148variable (C : ProCGroups.FiniteGroupClass.{u})
149variable {F G : Type u} [Group F] [Group G]
150variable [TopologicalSpace F] [TopologicalSpace G]
151variable [IsTopologicalGroup F] [IsTopologicalGroup G]
153/-- A pro-`C` presentation whose relator kernel is the closed normal closure of `R`. -/
154def IsRelatorPresentationOf (R : Set F) : Prop :=
155 IsQuotientByKernel C (F := F) (G := G) (closedNormalClosure R)
157/-- A pro-`C` presentation `G = ⟨X | R⟩` whose source is the chosen free pro-`C`
158group on `X`. -/
160 {X : Type u} [TopologicalSpace X] (ι : X → F) (R : Set F) : Prop :=
163theorem IsFreeRelatorPresentationOfClass.isRelatorPresentationOf
164 {X : Type u} [TopologicalSpace X] {ι : X → F} {R : Set F} :
166 IsRelatorPresentationOf C (G := G) R := by
167 intro h
168 exact IsFreePresentationOfClass.isQuotientByKernel C h
170/-- Tietze equivalence of two relator sets in the same profinite source. -/
171structure RelatorTietzeData (R S : Set F) : Prop where
172 left_relators : R ⊆ closedNormalClosure S
173 right_relators : S ⊆ closedNormalClosure R
177variable {C}
178variable {R S T : Set F}
181 closedNormalClosure R = closedNormalClosure S :=
182 closedNormalClosure_eq_of_mutual_le D.left_relators D.right_relators
184def refl (R : Set F) : RelatorTietzeData R R where
185 left_relators := subset_closedNormalClosure R
186 right_relators := subset_closedNormalClosure R
188def symm (D : RelatorTietzeData R S) : RelatorTietzeData S R where
189 left_relators := D.right_relators
190 right_relators := D.left_relators
192def trans (D₁ : RelatorTietzeData R S) (D₂ : RelatorTietzeData S T) :
194 left_relators := by
195 have hST : closedNormalClosure S ≤ closedNormalClosure T :=
197 (F := F) (N := closedNormalClosure T)
198 (closedNormalClosure_isClosed (F := F) T) D₂.left_relators
199 exact fun x hx => hST (D₁.left_relators hx)
200 right_relators := by
201 have hSR : closedNormalClosure S ≤ closedNormalClosure R :=
203 (F := F) (N := closedNormalClosure R)
204 (closedNormalClosure_isClosed (F := F) R) D₁.right_relators
205 exact fun x hx => hSR (D₂.right_relators hx)
207theorem presentation (D : RelatorTietzeData R S) :
208 IsRelatorPresentationOf C (G := G) R →
209 IsRelatorPresentationOf C (G := G) S := by
210 intro h
211 simpa [IsRelatorPresentationOf, D.closedNormalClosure_eq] using h
214 IsRelatorPresentationOf C (G := G) R ↔
215 IsRelatorPresentationOf C (G := G) S := by
216 constructor
217 · exact D.presentation
218 · exact D.symm.presentation
220def of_closedNormalClosure_eq (h : closedNormalClosure R = closedNormalClosure S) :
222 left_relators := by
223 intro x hx
224 simpa [h] using subset_closedNormalClosure (F := F) R hx
225 right_relators := by
226 intro x hx
227 simpa [h] using subset_closedNormalClosure (F := F) S hx
229def add_redundant_relators (hS : S ⊆ closedNormalClosure R) :
230 RelatorTietzeData (R ∪ S) R where
231 left_relators := by
232 intro x hx
233 exact hx.elim
234 (fun hxR => subset_closedNormalClosure (F := F) R hxR)
235 (fun hxS => hS hxS)
236 right_relators := by
237 intro x hx
238 exact subset_closedNormalClosure (F := F) (R ∪ S) (Or.inl hx)
240def delete_redundant_relators (hS : S ⊆ closedNormalClosure R) :
241 RelatorTietzeData R (R ∪ S) :=
242 (add_redundant_relators (F := F) hS).symm
244def removeRelatorSubset (hS : S ⊆ closedNormalClosure (R \ S)) :
245 RelatorTietzeData R (R \ S) where
246 left_relators := by
247 intro x hxR
248 by_cases hxS : x ∈ S
249 · exact hS hxS
250 · exact subset_closedNormalClosure (F := F) (R \ S) ⟨hxR, hxS⟩
251 right_relators := by
252 intro x hx
253 exact subset_closedNormalClosure (F := F) R hx.1
255def replaceRelatorSubset
256 {D E : Set F}
257 (hD : D ⊆ closedNormalClosure ((R \ D) ∪ E))
258 (hE : E ⊆ closedNormalClosure R) :
259 RelatorTietzeData R ((R \ D) ∪ E) where
260 left_relators := by
261 intro x hxR
262 by_cases hxD : x ∈ D
263 · exact hD hxD
264 · exact subset_closedNormalClosure (F := F) ((R \ D) ∪ E) (Or.inl ⟨hxR, hxD⟩)
265 right_relators := by
266 intro x hx
267 exact hx.elim
268 (fun hxRD => subset_closedNormalClosure (F := F) R hxRD.1)
269 (fun hxE => hE hxE)
271def replaceRelator
272 {r s : F}
273 (hr : r ∈ closedNormalClosure ((R \ {r}) ∪ ({s} : Set F)))
274 (hs : s ∈ closedNormalClosure R) :
275 RelatorTietzeData R ((R \ {r}) ∪ ({s} : Set F)) :=
276 replaceRelatorSubset (F := F) (R := R) (D := ({r} : Set F)) (E := ({s} : Set F))
277 (by
278 intro x hx
279 rw [Set.mem_singleton_iff] at hx
280 subst x
281 exact hr)
282 (by
283 intro x hx
284 rw [Set.mem_singleton_iff] at hx
285 subst x
286 exact hs)
288def add_trivial_relators
289 {D : Set F} (hD : D ⊆ ({1} : Set F)) :
290 RelatorTietzeData (R ∪ D) R :=
291 add_redundant_relators (F := F) (R := R) (S := D)
294def delete_trivial_relators
295 {D : Set F} (hD : D ⊆ ({1} : Set F)) :
296 RelatorTietzeData R (R ∪ D) :=
297 (add_trivial_relators (F := F) (R := R) hD).symm
302 {E : Type u} [Group E] [TopologicalSpace E] [IsTopologicalGroup E]
303 {R : Set F} {S : Set E}
304 (D : KernelTietzeData (closedNormalClosure R) (closedNormalClosure S)) :
305 IsRelatorPresentationOf C (G := G) R →
306 IsRelatorPresentationOf C (F := E) (G := G) S := by
309/-- Same-source relator Tietze data is enough for cosmetic cleaning. This structure is the
310cross-source version used when a Tietze step also changes the Schreier generator source. The
311recorded homomorphisms only have to carry the named relators into the opposite closed normal
312closure and be inverse modulo the corresponding closed normal closures. -/
314 {E : Type u} [Group E] [TopologicalSpace E] [IsTopologicalGroup E]
315 (R : Set F) (S : Set E) where
316 toHom : F →ₜ* E
317 invHom : E →ₜ* F
318 maps_relators : R ⊆ Subgroup.comap toHom.toMonoidHom (closedNormalClosure S)
319 maps_target_relators : S ⊆ Subgroup.comap invHom.toMonoidHom (closedNormalClosure R)
320 inv_toHom : ∀ x : F, invHom (toHom x) * x⁻¹ ∈ closedNormalClosure R
321 to_invHom : ∀ y : E, toHom (invHom y) * y⁻¹ ∈ closedNormalClosure S
325variable {C}
326variable {R S : Set F}
330 toHom := ContinuousMonoidHom.id F
331 invHom := ContinuousMonoidHom.id F
332 maps_relators := by
333 intro x hx
334 simpa using D.left_relators hx
335 maps_target_relators := by
336 intro x hx
337 simpa using D.right_relators hx
338 inv_toHom := by
339 intro x
340 simp only [ContinuousMonoidHom.id_toFun, mul_inv_cancel, one_mem]
341 to_invHom := by
342 intro x
343 simp only [ContinuousMonoidHom.id_toFun, mul_inv_cancel, one_mem]
345variable {E : Type u} [Group E] [TopologicalSpace E] [IsTopologicalGroup E]
346variable {R : Set F} {S : Set E}
349 closedNormalClosure R ≤ Subgroup.comap D.toHom.toMonoidHom (closedNormalClosure S) := by
350 let N : Subgroup F := Subgroup.comap D.toHom.toMonoidHom (closedNormalClosure S)
351 haveI : N.Normal := by
352 dsimp [N]
353 infer_instance
354 have hNclosed : IsClosed (N : Set F) := by
355 change IsClosed (D.toHom ⁻¹' ((closedNormalClosure S : Subgroup E) : Set E))
356 exact (closedNormalClosure_isClosed (F := E) S).preimage D.toHom.continuous_toFun
357 exact closedNormalClosure_le_closed_normal (F := F) (N := N) hNclosed D.maps_relators
360 closedNormalClosure S ≤ Subgroup.comap D.invHom.toMonoidHom (closedNormalClosure R) := by
361 let N : Subgroup E := Subgroup.comap D.invHom.toMonoidHom (closedNormalClosure R)
362 haveI : N.Normal := by
363 dsimp [N]
364 infer_instance
365 have hNclosed : IsClosed (N : Set E) := by
366 change IsClosed (D.invHom ⁻¹' ((closedNormalClosure R : Subgroup F) : Set F))
367 exact (closedNormalClosure_isClosed (F := F) R).preimage D.invHom.continuous_toFun
368 exact closedNormalClosure_le_closed_normal (F := E) (N := N) hNclosed
369 D.maps_target_relators
372 KernelTietzeData (closedNormalClosure R) (closedNormalClosure S) where
373 toHom := D.toHom
374 invHom := D.invHom
375 mapsKernel := D.maps_closedNormalClosure
376 mapsTargetKernel := D.maps_target_closedNormalClosure
377 inv_toHom := D.inv_toHom
378 to_invHom := D.to_invHom
380theorem presentation (D : RelatorMapTietzeData R S) :
381 IsRelatorPresentationOf C (G := G) R →
382 IsRelatorPresentationOf C (F := E) (G := G) S :=
387theorem isRelatorPresentationOf_delete_redundant_relators
388 {R D : Set F} (hD : D ⊆ closedNormalClosure R) :
389 IsRelatorPresentationOf C (G := G) (R ∪ D) →
390 IsRelatorPresentationOf C (G := G) R := by
391 intro h
392 simpa [IsRelatorPresentationOf, closedNormalClosure_union_eq_left (F := F) hD] using h
395 {R D : Set F} (hD : D ⊆ closedNormalClosure R) :
396 IsRelatorPresentationOf C (G := G) R →
397 IsRelatorPresentationOf C (G := G) (R ∪ D) := by
398 intro h
399 simpa [IsRelatorPresentationOf, closedNormalClosure_union_eq_left (F := F) hD] using h
402 {R D : Set F} (hD : D ⊆ ({1} : Set F)) :
403 IsRelatorPresentationOf C (G := G) (R ∪ D) →
405 isRelatorPresentationOf_delete_redundant_relators C
409 {R D : Set F} (hD : D ⊆ ({1} : Set F)) :
410 IsRelatorPresentationOf C (G := G) R →
411 IsRelatorPresentationOf C (G := G) (R ∪ D) :=
415/-- The named relator families appearing in a profinite Reidemeister-Schreier presentation:
416rewrites of the original relators, degenerate Schreier-generator relators, and a cleaned family
417after Tietze deletions/substitutions. -/
418structure ProfiniteSchreierRelatorSets (F : Type u) where
419 rewritten : Set F
420 degenerate : Set F
421 cleaned : Set F
425/-- The raw Schreier relators: rewritten original relators plus degenerate generator relators. -/
426def raw (S : ProfiniteSchreierRelatorSets F) : Set F :=
427 S.rewritten ∪ S.degenerate
429/-- Data saying that the relators in `D` are redundant relative to `R` in the same ambient free
430group. This is relator deletion, not generator deletion: the presentation source is unchanged. -/
431structure RedundantRelatorDeletionData (R D : Set F) : Prop where
432 redundant : D ⊆ closedNormalClosure R
436variable {R D : Set F}
438theorem closedNormalClosure_union_eq_left (H : RedundantRelatorDeletionData (F := F) R D) :
439 closedNormalClosure (R ∪ D) = closedNormalClosure R := by
440 exact _root_.ProCGroups.Presentations.closedNormalClosure_union_eq_left (F := F) H.redundant
443 RelatorTietzeData (R ∪ D) R where
444 left_relators := by
445 intro x hx
446 have hx' : x ∈ closedNormalClosure (R ∪ D) :=
447 subset_closedNormalClosure (F := F) (R ∪ D) hx
448 simpa [H.closedNormalClosure_union_eq_left] using hx'
449 right_relators := by
450 intro x hx
451 exact subset_closedNormalClosure (F := F) (R ∪ D) (Or.inl hx)
453theorem isRelatorPresentationOf_delete_redundant_relators
454 (H : RedundantRelatorDeletionData (F := F) R D) :
455 IsRelatorPresentationOf C (G := G) (R ∪ D) →
457 H.relatorTietze_union_left.presentation
461/-- Tietze data for genuine generator deletion, where the ambient free group may change.
463Unlike `RedundantRelatorDeletionData`, this records maps between two presentation sources and
464inverse data modulo the respective closed normal closures. -/
466 (Fraw Fclean : Type u)
467 [Group Fraw] [TopologicalSpace Fraw] [IsTopologicalGroup Fraw]
468 [Group Fclean] [TopologicalSpace Fclean] [IsTopologicalGroup Fclean]
469 (Rraw : Set Fraw) (Rclean : Set Fclean) where
470 mapRawToClean : Fraw →* Fclean
471 mapCleanToRaw : Fclean →* Fraw
472 relators_forward : mapRawToClean '' Rraw ⊆ closedNormalClosure Rclean
473 relators_backward : mapCleanToRaw '' Rclean ⊆ closedNormalClosure Rraw
474 inverse_mod_relators_raw :
475 ∀ x : Fraw, mapCleanToRaw (mapRawToClean x) * x⁻¹ ∈ closedNormalClosure Rraw
476 inverse_mod_relators_clean :
477 ∀ x : Fclean, mapRawToClean (mapCleanToRaw x) * x⁻¹ ∈ closedNormalClosure Rclean
479/-- Schreier-specific redundant-relator deletion for degenerate relators. -/
480abbrev DegenerateRelatorDeletionData (S : ProfiniteSchreierRelatorSets F) : Prop :=
481 RedundantRelatorDeletionData S.rewritten S.degenerate
483namespace DegenerateRelatorDeletionData
487theorem closedNormalClosure_raw_eq_rewritten (D : DegenerateRelatorDeletionData S) :
488 closedNormalClosure S.raw = closedNormalClosure S.rewritten := by
489 exact D.closedNormalClosure_union_eq_left
491theorem relatorTietze_raw_rewritten (D : DegenerateRelatorDeletionData S) :
492 RelatorTietzeData S.raw S.rewritten :=
493 D.relatorTietze_union_left
495theorem isRelatorPresentationOf_delete_degenerate_relators
496 (D : DegenerateRelatorDeletionData S) :
497 IsRelatorPresentationOf C (G := G) S.raw →
498 IsRelatorPresentationOf C (G := G) S.rewritten :=
499 D.relatorTietze_raw_rewritten.presentation
501end DegenerateRelatorDeletionData
503/-- Cleaning data saying that degenerate relators are Tietze-redundant and that the cleaned
504family generates the same closed normal subgroup as the rewritten relators. -/
505structure CleaningData (S : ProfiniteSchreierRelatorSets F) : Prop where
506 degenerate_le : S.degenerate ⊆ closedNormalClosure S.rewritten
507 rewritten_le_cleaned : S.rewritten ⊆ closedNormalClosure S.cleaned
508 cleaned_le_rewritten : S.cleaned ⊆ closedNormalClosure S.rewritten
510namespace CleaningData
514def toDegenerateRelatorDeletionData (D : CleaningData S) :
515 DegenerateRelatorDeletionData S where
516 redundant := D.degenerate_le
518theorem closedNormalClosure_raw_eq_rewritten (D : CleaningData S) :
519 closedNormalClosure S.raw = closedNormalClosure S.rewritten := by
520 exact D.toDegenerateRelatorDeletionData.closedNormalClosure_raw_eq_rewritten
522theorem relatorTietze_raw_rewritten (D : CleaningData S) :
523 RelatorTietzeData S.raw S.rewritten :=
524 D.toDegenerateRelatorDeletionData.relatorTietze_raw_rewritten
526theorem relatorTietze_rewritten_cleaned (D : CleaningData S) :
527 RelatorTietzeData S.rewritten S.cleaned where
528 left_relators := D.rewritten_le_cleaned
529 right_relators := D.cleaned_le_rewritten
531theorem relatorTietze_raw_cleaned (D : CleaningData S) :
532 RelatorTietzeData S.raw S.cleaned :=
533 (D.relatorTietze_raw_rewritten).trans D.relatorTietze_rewritten_cleaned
535theorem closedNormalClosure_raw_eq_cleaned (D : CleaningData S) :
536 closedNormalClosure S.raw = closedNormalClosure S.cleaned :=
537 D.relatorTietze_raw_cleaned.closedNormalClosure_eq
539theorem isRelatorPresentationOf_cleaned
540 (D : CleaningData S) :
541 IsRelatorPresentationOf C (G := G) S.raw →
542 IsRelatorPresentationOf C (G := G) S.cleaned :=
543 D.relatorTietze_raw_cleaned.presentation
545theorem isRelatorPresentationOf_cleaned_iff
546 (D : CleaningData S) :
547 IsRelatorPresentationOf C (G := G) S.raw ↔
548 IsRelatorPresentationOf C (G := G) S.cleaned :=
549 D.relatorTietze_raw_cleaned.presentation_iff
551end CleaningData
555/-- A list-level spelling of the three Schreier relator families. It is useful for statements
556whose input is literally a relator list in a paper or construction. -/
557structure ProfiniteSchreierRelatorLists (F : Type u) where
558 rewritten : List F
559 degenerate : List F
560 cleaned : List F
564def raw (S : ProfiniteSchreierRelatorLists F) : List F :=
565 S.rewritten ++ S.degenerate
567def toRelatorSets (S : ProfiniteSchreierRelatorLists F) :
569 rewritten := relatorListSet S.rewritten
570 degenerate := relatorListSet S.degenerate
571 cleaned := relatorListSet S.cleaned
573omit [Group F] [TopologicalSpace F] [IsTopologicalGroup F] in
575 relatorListSet S.raw = S.toRelatorSets.raw := by
576 ext x
577 simp only [raw, relatorListSet_append, Set.mem_union, mem_relatorListSet, ProfiniteSchreierRelatorSets.raw,
578 toRelatorSets]
580abbrev DegenerateRelatorDeletionData (S : ProfiniteSchreierRelatorLists F) : Prop :=
581 ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData S.toRelatorSets
583abbrev CleaningData (S : ProfiniteSchreierRelatorLists F) : Prop :=
584 ProfiniteSchreierRelatorSets.CleaningData S.toRelatorSets
586theorem isRelatorPresentationOf_delete_degenerate_relators
588 (D : DegenerateRelatorDeletionData S) :
590 IsRelatorPresentationOf C (G := G) (relatorListSet S.rewritten) := by
591 intro h
592 have hraw : IsRelatorPresentationOf C (G := G) S.toRelatorSets.raw := by
593 simpa [relatorListSet_raw] using h
594 have hrewritten :
595 IsRelatorPresentationOf C (G := G) S.toRelatorSets.rewritten :=
596 ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData.isRelatorPresentationOf_delete_degenerate_relators
597 (C := C) (G := G) D hraw
598 simpa [toRelatorSets] using hrewritten
600theorem isRelatorPresentationOf_cleaned
602 (D : CleaningData S) :
604 IsRelatorPresentationOf C (G := G) (relatorListSet S.cleaned) := by
605 intro h
606 have hraw : IsRelatorPresentationOf C (G := G) S.toRelatorSets.raw := by
607 simpa [relatorListSet_raw] using h
608 have hcleaned :
609 IsRelatorPresentationOf C (G := G) S.toRelatorSets.cleaned :=
610 ProfiniteSchreierRelatorSets.CleaningData.isRelatorPresentationOf_cleaned
611 (C := C) (G := G) D hraw
612 simpa [toRelatorSets] using hcleaned
614theorem isRelatorPresentationOf_cleaned_iff
616 (D : CleaningData S) :
618 IsRelatorPresentationOf C (G := G) (relatorListSet S.cleaned) := by
619 have hsets :
620 IsRelatorPresentationOf C (G := G) S.toRelatorSets.raw ↔
621 IsRelatorPresentationOf C (G := G) S.toRelatorSets.cleaned :=
622 ProfiniteSchreierRelatorSets.CleaningData.isRelatorPresentationOf_cleaned_iff
623 (C := C) (G := G) D
624 simpa [relatorListSet_raw, toRelatorSets] using hsets
628/-- A finset-level spelling of the three Schreier relator families. -/
629structure ProfiniteSchreierRelatorFinsets (F : Type u) where
630 rewritten : Finset F
631 degenerate : Finset F
632 cleaned : Finset F
636def raw [DecidableEq F] (S : ProfiniteSchreierRelatorFinsets F) : Finset F :=
637 S.rewritten ∪ S.degenerate
639def toRelatorSets (S : ProfiniteSchreierRelatorFinsets F) :
641 rewritten := relatorFinsetSet S.rewritten
642 degenerate := relatorFinsetSet S.degenerate
643 cleaned := relatorFinsetSet S.cleaned
645omit [Group F] [TopologicalSpace F] [IsTopologicalGroup F] in
646@[simp] theorem relatorFinsetSet_raw [DecidableEq F] (S : ProfiniteSchreierRelatorFinsets F) :
647 relatorFinsetSet S.raw = S.toRelatorSets.raw := by
648 ext x
649 simp only [raw, relatorFinsetSet_union, Set.mem_union, mem_relatorFinsetSet, ProfiniteSchreierRelatorSets.raw,
650 toRelatorSets]
652abbrev DegenerateRelatorDeletionData (S : ProfiniteSchreierRelatorFinsets F) : Prop :=
653 ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData S.toRelatorSets
655abbrev CleaningData (S : ProfiniteSchreierRelatorFinsets F) : Prop :=
656 ProfiniteSchreierRelatorSets.CleaningData S.toRelatorSets
658theorem isRelatorPresentationOf_delete_degenerate_relators
659 [DecidableEq F] {S : ProfiniteSchreierRelatorFinsets F}
660 (D : DegenerateRelatorDeletionData S) :
662 IsRelatorPresentationOf C (G := G) (relatorFinsetSet S.rewritten) := by
663 intro h
664 have hraw : IsRelatorPresentationOf C (G := G) S.toRelatorSets.raw := by
665 simpa [relatorFinsetSet_raw] using h
666 have hrewritten :
667 IsRelatorPresentationOf C (G := G) S.toRelatorSets.rewritten :=
668 ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData.isRelatorPresentationOf_delete_degenerate_relators
669 (C := C) (G := G) D hraw
670 simpa [toRelatorSets] using hrewritten
672theorem isRelatorPresentationOf_cleaned
673 [DecidableEq F] {S : ProfiniteSchreierRelatorFinsets F}
674 (D : CleaningData S) :
676 IsRelatorPresentationOf C (G := G) (relatorFinsetSet S.cleaned) := by
677 intro h
678 have hraw : IsRelatorPresentationOf C (G := G) S.toRelatorSets.raw := by
679 simpa [relatorFinsetSet_raw] using h
680 have hcleaned :
681 IsRelatorPresentationOf C (G := G) S.toRelatorSets.cleaned :=
682 ProfiniteSchreierRelatorSets.CleaningData.isRelatorPresentationOf_cleaned
683 (C := C) (G := G) D hraw
684 simpa [toRelatorSets] using hcleaned
688/-- Schreier relator data built directly from a rewriting map `tau`. The rewritten relators are
689definitionally `{ tau(t,r) | t ∈ transversal, r ∈ originalRelators }`. -/
691 (Q : Type v) (A : Type w) (F : Type u) where
692 tau : Q → A → F
693 transversal : Set Q
694 originalRelators : Set A
695 degenerate : Set F
696 cleaned : Set F
700variable {Q : Type v} {A : Type w}
702def rewritten (S : ProfiniteSchreierRewritingRelatorSets Q A F) : Set F :=
703 schreierRelatorSet S.tau S.transversal S.originalRelators
705def toRelatorSets (S : ProfiniteSchreierRewritingRelatorSets Q A F) :
707 rewritten := S.rewritten
708 degenerate := S.degenerate
709 cleaned := S.cleaned
711def raw (S : ProfiniteSchreierRewritingRelatorSets Q A F) : Set F :=
712 S.toRelatorSets.raw
714abbrev DegenerateRelatorDeletionData
716 ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData S.toRelatorSets
718abbrev CleaningData
720 ProfiniteSchreierRelatorSets.CleaningData S.toRelatorSets
722theorem isRelatorPresentationOf_delete_degenerate_relators
724 (D : DegenerateRelatorDeletionData S) :
725 IsRelatorPresentationOf C (G := G) S.toRelatorSets.raw →
726 IsRelatorPresentationOf C (G := G) S.toRelatorSets.rewritten := by
727 intro h
728 exact
729 ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData.isRelatorPresentationOf_delete_degenerate_relators
730 (C := C) (G := G) D h
732theorem isRelatorPresentationOf_cleaned
734 (D : CleaningData S) :
735 IsRelatorPresentationOf C (G := G) S.toRelatorSets.raw →
736 IsRelatorPresentationOf C (G := G) S.toRelatorSets.cleaned := by
737 intro h
738 exact ProfiniteSchreierRelatorSets.CleaningData.isRelatorPresentationOf_cleaned
739 (C := C) (G := G) D h
743/-- List-level Schreier relator data built from a rewriting map `tau`. -/
745 (Q : Type v) (A : Type w) (F : Type u) where
746 tau : Q → A → F
747 transversal : List Q
748 originalRelators : List A
749 degenerate : List F
750 cleaned : List F
754variable {Q : Type v} {A : Type w}
756def rewritten (S : ProfiniteSchreierRewritingRelatorLists Q A F) : List F :=
757 schreierRelatorList S.tau S.transversal S.originalRelators
761 rewritten := S.rewritten
762 degenerate := S.degenerate
763 cleaned := S.cleaned
765def raw (S : ProfiniteSchreierRewritingRelatorLists Q A F) : List F :=
766 S.toRelatorLists.raw
768abbrev DegenerateRelatorDeletionData
770 ProfiniteSchreierRelatorLists.DegenerateRelatorDeletionData S.toRelatorLists
772abbrev CleaningData
774 ProfiniteSchreierRelatorLists.CleaningData S.toRelatorLists
776theorem isRelatorPresentationOf_delete_degenerate_relators
778 (D : DegenerateRelatorDeletionData S) :
780 IsRelatorPresentationOf C (G := G) (relatorListSet S.rewritten) :=
781 ProfiniteSchreierRelatorLists.isRelatorPresentationOf_delete_degenerate_relators
782 (C := C) (G := G) D
784theorem isRelatorPresentationOf_cleaned
786 (D : CleaningData S) :
788 IsRelatorPresentationOf C (G := G) (relatorListSet S.cleaned) :=
789 ProfiniteSchreierRelatorLists.isRelatorPresentationOf_cleaned
790 (C := C) (G := G) D
794/-- Finset-level Schreier relator data built from a rewriting map `tau`. -/
796 (Q : Type v) (A : Type w) (F : Type u) where
797 tau : Q → A → F
798 transversal : Finset Q
799 originalRelators : Finset A
800 degenerate : Finset F
801 cleaned : Finset F
805variable {Q : Type v} {A : Type w}
807def rewritten [DecidableEq F] (S : ProfiniteSchreierRewritingRelatorFinsets Q A F) :
808 Finset F :=
809 schreierRelatorFinset S.tau S.transversal S.originalRelators
813 rewritten := S.rewritten
814 degenerate := S.degenerate
815 cleaned := S.cleaned
817def raw [DecidableEq F] (S : ProfiniteSchreierRewritingRelatorFinsets Q A F) :
818 Finset F :=
819 S.toRelatorFinsets.raw
821abbrev DegenerateRelatorDeletionData
822 [DecidableEq F] (S : ProfiniteSchreierRewritingRelatorFinsets Q A F) : Prop :=
823 ProfiniteSchreierRelatorFinsets.DegenerateRelatorDeletionData S.toRelatorFinsets
825abbrev CleaningData
826 [DecidableEq F] (S : ProfiniteSchreierRewritingRelatorFinsets Q A F) : Prop :=
827 ProfiniteSchreierRelatorFinsets.CleaningData S.toRelatorFinsets
829theorem isRelatorPresentationOf_delete_degenerate_relators
830 [DecidableEq F] {S : ProfiniteSchreierRewritingRelatorFinsets Q A F}
831 (D : DegenerateRelatorDeletionData S) :
833 IsRelatorPresentationOf C (G := G) (relatorFinsetSet S.rewritten) :=
834 ProfiniteSchreierRelatorFinsets.isRelatorPresentationOf_delete_degenerate_relators
835 (C := C) (G := G) D
837theorem isRelatorPresentationOf_cleaned
838 [DecidableEq F] {S : ProfiniteSchreierRewritingRelatorFinsets Q A F}
839 (D : CleaningData S) :
841 IsRelatorPresentationOf C (G := G) (relatorFinsetSet S.cleaned) :=
842 ProfiniteSchreierRelatorFinsets.isRelatorPresentationOf_cleaned
843 (C := C) (G := G) D
847end RelatorPresentations
849end ProCGroups.Presentations