ProCGroups.Presentations.SchreierTietze.Relators
This module develops the rewriting and basis constructions behind the subgroup calculations. It tracks words and relations through the chosen transversal to obtain the required presentation or basis statements.
def relatorFamilySet {ι : Sort v} (r : ι → F) : Set F :=
Set.range rThe relator set represented by an indexed family. This is the profinite analogue of the double-prime relator-family notation used in Reidemeister--Schreier/Tietze arguments.
@[simp] theorem mem_relatorFamilySet {ι : Sort v} (r : ι → F) (x : F) :
x ∈ relatorFamilySet r ↔ ∃ i, r i = xMembership in a relator-family set is membership in one of the family fibers.
Show proof
Iff.rflProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□def relatorListSet (l : List F) : Set F :=
{x | x ∈ l}The relator set represented by a finite list. This avoids quotienting the list by permutation; order and repetitions are syntactic data, while the closed normal closure only sees the induced set.
@[simp] theorem mem_relatorListSet (l : List F) (x : F) :
x ∈ relatorListSet l ↔ x ∈ lMembership in a list relator set is membership in the underlying list.
Show proof
Iff.rflProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□@[simp] theorem relatorListSet_nil :
relatorListSet ([] : List F) = (∅ : Set F)The relator set associated to the empty list is empty.
Show proof
by
ext x
simp only [relatorListSet, List.not_mem_nil, Set.setOf_false, Set.mem_empty_iff_false]Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□@[simp] theorem relatorListSet_cons (x : F) (l : List F) :
relatorListSet (x :: l) = ({x} : Set F) ∪ relatorListSet lAdding a relator to the front of a list adds it to the associated relator set.
Show proof
by
ext y
simp only [relatorListSet, List.mem_cons, Set.mem_setOf_eq, Set.singleton_union, Set.mem_insert_iff]Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□@[simp] theorem relatorListSet_append (l m : List F) :
relatorListSet (l ++ m) = relatorListSet l ∪ relatorListSet mThe relator set associated to an appended list is the union of the relator sets associated to the two lists.
Show proof
by
ext x
simp only [relatorListSet, List.mem_append, Set.mem_setOf_eq, Set.mem_union]Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□def relatorFinsetSet (s : Finset F) : Set F :=
{x | x ∈ s}The relator set represented by a finset.
@[simp] theorem mem_relatorFinsetSet (s : Finset F) (x : F) :
x ∈ relatorFinsetSet s ↔ x ∈ sMembership in a finset relator set is membership in the underlying finset.
Show proof
Iff.rflProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□@[simp] theorem relatorFinsetSet_empty :
relatorFinsetSet (∅ : Finset F) = (∅ : Set F)The relator set associated to the empty finset is empty.
Show proof
by
ext x
simp only [relatorFinsetSet, Finset.notMem_empty, Set.setOf_false, Set.mem_empty_iff_false]Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□@[simp] theorem relatorFinsetSet_insert [DecidableEq F] (x : F) (s : Finset F) :
relatorFinsetSet (insert x s) = ({x} : Set F) ∪ relatorFinsetSet sInserting a relator into a finset adds it to the associated relator set.
Show proof
by
ext y
simp only [relatorFinsetSet, Finset.mem_insert, Set.mem_setOf_eq, SetLike.setOf_mem_eq, Set.singleton_union,
Set.mem_insert_iff, SetLike.mem_coe]Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□@[simp] theorem relatorFinsetSet_union [DecidableEq F] (s t : Finset F) :
relatorFinsetSet (s ∪ t) = relatorFinsetSet s ∪ relatorFinsetSet tThe relator set associated to a union of finsets is the union of the associated relator sets.
Show proof
by
ext x
simp only [relatorFinsetSet, Finset.mem_union, Set.mem_setOf_eq, SetLike.setOf_mem_eq, Set.mem_union,
SetLike.mem_coe]Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□def schreierRelatorSet {Q : Type v} {A : Type w}
(τ : Q → A → F) (T : Set Q) (R : Set A) : Set F :=
{x | ∃ t ∈ T, ∃ r ∈ R, τ t r = x}The relator set obtained from a Schreier rewriting map \(\tau\), a family of transversal labels, and a family of original relators. This is the profinite/presentation-level spelling of \({ \tau(t,r) | t \in T, r \in R }\).
@[simp] theorem mem_schreierRelatorSet
{Q : Type v} {A : Type w}
(τ : Q → A → F) (T : Set Q) (R : Set A) (x : F) :
x ∈ schreierRelatorSet τ T R ↔ ∃ t ∈ T, ∃ r ∈ R, τ t r = xMembership in the Schreier relator set is membership of one of the rewritten Schreier relators.
Show proof
Iff.rflProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□def schreierRelatorList {Q : Type v} {A : Type w}
(τ : Q → A → F) : List Q → List A → List F
| [], _ => []
| t :: ts, rs => rs.map (τ t) ++ schreierRelatorList τ ts rsList version of a Schreier rewritten relator family.
@[simp] theorem mem_schreierRelatorList
{Q : Type v} {A : Type w}
(τ : Q → A → F) (ts : List Q) (rs : List A) (x : F) :
x ∈ schreierRelatorList τ ts rs ↔ ∃ t ∈ ts, ∃ r ∈ rs, τ t r = xMembership in the Schreier relator list is membership of one of the rewritten Schreier relators.
Show proof
by
induction ts with
| nil =>
simp only [schreierRelatorList, List.not_mem_nil, false_and, exists_false]
| cons t ts ih =>
simp only [schreierRelatorList, List.mem_append, List.mem_map, ih, List.mem_cons, exists_eq_or_imp]Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□@[simp] theorem relatorListSet_schreierRelatorList
{Q : Type v} {A : Type w}
(τ : Q → A → F) (ts : List Q) (rs : List A) :
relatorListSet (schreierRelatorList τ ts rs) =
schreierRelatorSet τ (relatorListSet ts) (relatorListSet rs)The relator set associated to the Schreier relator list is the set of rewritten Schreier relators.
Show proof
by
ext x
simp only [mem_relatorListSet, mem_schreierRelatorList, schreierRelatorSet, Set.mem_setOf_eq]Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□def schreierRelatorFinset {Q : Type v} {A : Type w} [DecidableEq F]
(τ : Q → A → F) (ts : Finset Q) (rs : Finset A) : Finset F :=
ts.biUnion fun t => rs.image (τ t)Finite-set version of a Schreier rewritten relator family.
@[simp] theorem mem_schreierRelatorFinset
{Q : Type v} {A : Type w} [DecidableEq F]
(τ : Q → A → F) (ts : Finset Q) (rs : Finset A) (x : F) :
x ∈ schreierRelatorFinset τ ts rs ↔ ∃ t ∈ ts, ∃ r ∈ rs, τ t r = xMembership in the Schreier relator finset is membership of one of the rewritten Schreier relators.
Show proof
by
simp only [schreierRelatorFinset, Finset.mem_biUnion, Finset.mem_image]Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□@[simp] theorem relatorFinsetSet_schreierRelatorFinset
{Q : Type v} {A : Type w} [DecidableEq F]
(τ : Q → A → F) (ts : Finset Q) (rs : Finset A) :
relatorFinsetSet (schreierRelatorFinset τ ts rs) =
schreierRelatorSet τ (relatorFinsetSet ts) (relatorFinsetSet rs)The relator set associated to the Schreier relator finset is the set of rewritten Schreier relators.
Show proof
by
ext x
simp only [mem_relatorFinsetSet, mem_schreierRelatorFinset, schreierRelatorSet, Set.mem_setOf_eq]Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□def IsRelatorPresentationOf (R : Set F) : Prop :=
IsQuotientByKernel C (F := F) (G := G) (closedNormalClosure R)A pro-\(C\) presentation whose relator kernel is the closed normal closure of R.
def IsFreeRelatorPresentationOfClass
{X : Type u} [TopologicalSpace X] (ι : X → F) (R : Set F) : Prop :=
IsFreePresentationOfClass C (G := G) ι RA pro-\(C\) presentation \(G = (X \mid R)\) whose source is the chosen free pro-\(C\) group on \(X\).
theorem IsFreeRelatorPresentationOfClass.isRelatorPresentationOf
{X : Type u} [TopologicalSpace X] {ι : X → F} {R : Set F} :
IsFreeRelatorPresentationOfClass C (G := G) ι R →
IsRelatorPresentationOf C (G := G) RA free-relator presentation in the given class is, in particular, a relator presentation.
Show proof
by
intro h
exact IsFreePresentationOfClass.isQuotientByKernel C hProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□structure RelatorTietzeData (R S : Set F) : Prop where
left_relators : R ⊆ closedNormalClosure S
right_relators : S ⊆ closedNormalClosure RTietze equivalence of two relator sets in the same profinite source.
theorem closedNormalClosure_eq (D : RelatorTietzeData R S) :
closedNormalClosure R = closedNormalClosure SThe closed normal closures agree under the stated relator comparison.
Show proof
closedNormalClosure_eq_of_mutual_le D.left_relators D.right_relatorsProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□def refl (R : Set F) : RelatorTietzeData R R where
left_relators := subset_closedNormalClosure R
right_relators := subset_closedNormalClosure RThe identity Tietze datum.
def symm (D : RelatorTietzeData R S) : RelatorTietzeData S R where
left_relators := D.right_relators
right_relators := D.left_relatorsReverse a Tietze datum.
def trans (D₁ : RelatorTietzeData R S) (D₂ : RelatorTietzeData S T) :
RelatorTietzeData R T where
left_relators := by
have hST : closedNormalClosure S ≤ closedNormalClosure T :=
closedNormalClosure_le_closed_normal
(F := F) (N := closedNormalClosure T)
(closedNormalClosure_isClosed (F := F) T) D₂.left_relators
exact fun x hx => hST (D₁.left_relators hx)
right_relators := by
have hSR : closedNormalClosure S ≤ closedNormalClosure R :=
closedNormalClosure_le_closed_normal
(F := F) (N := closedNormalClosure R)
(closedNormalClosure_isClosed (F := F) R) D₁.right_relators
exact fun x hx => hSR (D₂.right_relators hx)Tietze data compose.
theorem presentation (D : RelatorTietzeData R S) :
IsRelatorPresentationOf C (G := G) R →
IsRelatorPresentationOf C (G := G) SRelator Tietze data determine the corresponding presentation.
Show proof
by
intro h
simpa [IsRelatorPresentationOf, D.closedNormalClosure_eq] using hProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem presentation_iff (D : RelatorTietzeData R S) :
IsRelatorPresentationOf C (G := G) R ↔
IsRelatorPresentationOf C (G := G) SThe two defining conditions are equivalent after unfolding.
Show proof
by
constructor
· exact D.presentation
· exact D.symm.presentationProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□def of_closedNormalClosure_eq (h : closedNormalClosure R = closedNormalClosure S) :
RelatorTietzeData R S where
left_relators := by
intro x hx
simpa [h] using subset_closedNormalClosure (F := F) R hx
right_relators := by
intro x hx
simpa [h] using subset_closedNormalClosure (F := F) S hxThe closed normal closures agree under the stated relator comparison.
def add_redundant_relators (hS : S ⊆ closedNormalClosure R) :
RelatorTietzeData (R ∪ S) R where
left_relators := by
intro x hx
exact hx.elim
(fun hxR => subset_closedNormalClosure (F := F) R hxR)
(fun hxS => hS hxS)
right_relators := by
intro x hx
exact subset_closedNormalClosure (F := F) (R ∪ S) (Or.inl hx)Adding redundant relators preserves the corresponding relator presentation data.
def delete_redundant_relators (hS : S ⊆ closedNormalClosure R) :
RelatorTietzeData R (R ∪ S) :=
(add_redundant_relators (F := F) hS).symmDeleting redundant Reidemeister--Schreier relators preserves the relator presentation of the corresponding open subgroup.
def removeRelatorSubset (hS : S ⊆ closedNormalClosure (R \ S)) :
RelatorTietzeData R (R \ S) where
left_relators := by
intro x hxR
by_cases hxS : x ∈ S
· exact hS hxS
· exact subset_closedNormalClosure (F := F) (R \ S) ⟨hxR, hxS⟩
right_relators := by
intro x hx
exact subset_closedNormalClosure (F := F) R hx.1Removing a redundant relator subset preserves the relator Tietze data.
def replaceRelatorSubset
{D E : Set F}
(hD : D ⊆ closedNormalClosure ((R \ D) ∪ E))
(hE : E ⊆ closedNormalClosure R) :
RelatorTietzeData R ((R \ D) ∪ E) where
left_relators := by
intro x hxR
by_cases hxD : x ∈ D
· exact hD hxD
· exact subset_closedNormalClosure (F := F) ((R \ D) ∪ E) (Or.inl ⟨hxR, hxD⟩)
right_relators := by
intro x hx
exact hx.elim
(fun hxRD => subset_closedNormalClosure (F := F) R hxRD.1)
(fun hxE => hE hxE)Replace a whole subfamily \(D\) of relators by a new family \(E\). Relators outside \(D\) are kept unchanged.
def replaceRelator
{r s : F}
(hr : r ∈ closedNormalClosure ((R \ {r}) ∪ ({s} : Set F)))
(hs : s ∈ closedNormalClosure R) :
RelatorTietzeData R ((R \ {r}) ∪ ({s} : Set F)) :=
replaceRelatorSubset (F := F) (R := R) (D := ({r} : Set F)) (E := ({s} : Set F))
(by
intro x hx
rw [Set.mem_singleton_iff] at hx
subst x
exact hr)
(by
intro x hx
rw [Set.mem_singleton_iff] at hx
subst x
exact hs)Replacing a relator by an equivalent relator preserves the relator Tietze data.
def add_trivial_relators
{D : Set F} (hD : D ⊆ ({1} : Set F)) :
RelatorTietzeData (R ∪ D) R :=
add_redundant_relators (F := F) (R := R) (S := D)
(subset_closedNormalClosure_of_subset_singleton_one (F := F) hD)Adding trivial relators preserves the corresponding relator presentation data.
def delete_trivial_relators
{D : Set F} (hD : D ⊆ ({1} : Set F)) :
RelatorTietzeData R (R ∪ D) :=
(add_trivial_relators (F := F) (R := R) hD).symmDeleting trivial relators preserves the corresponding presentation data.
theorem isRelatorPresentationOf_of_kernelTietzeData
{E : Type u} [Group E] [TopologicalSpace E] [IsTopologicalGroup E]
{R : Set F} {S : Set E}
(D : KernelTietzeData (closedNormalClosure R) (closedNormalClosure S)) :
IsRelatorPresentationOf C (G := G) R →
IsRelatorPresentationOf C (F := E) (G := G) SThe resulting Reidemeister--Schreier relators present the corresponding open subgroup.
Show proof
by
exact isPresentationOf_of_kernelTietzeData C DProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□structure RelatorMapTietzeData
{E : Type u} [Group E] [TopologicalSpace E] [IsTopologicalGroup E]
(R : Set F) (S : Set E) where
toHom : F →ₜ* E
invHom : E →ₜ* F
maps_relators : R ⊆ Subgroup.comap toHom.toMonoidHom (closedNormalClosure S)
maps_target_relators : S ⊆ Subgroup.comap invHom.toMonoidHom (closedNormalClosure R)
inv_toHom : ∀ x : F, invHom (toHom x) * x⁻¹ ∈ closedNormalClosure R
to_invHom : ∀ y : E, toHom (invHom y) * y⁻¹ ∈ closedNormalClosure SSame-source relator Tietze data is enough for cosmetic cleaning. This structure is the cross-source version used when a Tietze step also changes the Schreier generator source. The recorded homomorphisms only have to carry the named relators into the opposite closed normal closure and be inverse modulo the corresponding closed normal closures.
def ofRelatorTietzeData (D : RelatorTietzeData R S) :
RelatorMapTietzeData R S where
toHom := ContinuousMonoidHom.id F
invHom := ContinuousMonoidHom.id F
maps_relators := by
intro x hx
simpa using D.left_relators hx
maps_target_relators := by
intro x hx
simpa using D.right_relators hx
inv_toHom := by
intro x
simp only [ContinuousMonoidHom.id_toFun, mul_inv_cancel, one_mem]
to_invHom := by
intro x
simp only [ContinuousMonoidHom.id_toFun, mul_inv_cancel, one_mem]Relator Tietze data yields the corresponding Schreier rewriting relator data.
theorem maps_closedNormalClosure (D : RelatorMapTietzeData R S) :
closedNormalClosure R ≤ Subgroup.comap D.toHom.toMonoidHom (closedNormalClosure S)The induced pro-\(C\) map agrees with the corresponding finite-quotient construction.
Show proof
by
let N : Subgroup F := Subgroup.comap D.toHom.toMonoidHom (closedNormalClosure S)
haveI : N.Normal := by
dsimp [N]
infer_instance
have hNclosed : IsClosed (N : Set F) := by
change IsClosed (D.toHom ⁻¹' ((closedNormalClosure S : Subgroup E) : Set E))
exact (closedNormalClosure_isClosed (F := E) S).preimage D.toHom.continuous_toFun
exact closedNormalClosure_le_closed_normal (F := F) (N := N) hNclosed D.maps_relatorsProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem maps_target_closedNormalClosure (D : RelatorMapTietzeData R S) :
closedNormalClosure S ≤ Subgroup.comap D.invHom.toMonoidHom (closedNormalClosure R)The inverse relator map sends the target closed normal closure into the source closed normal closure.
Show proof
by
let N : Subgroup E := Subgroup.comap D.invHom.toMonoidHom (closedNormalClosure R)
haveI : N.Normal := by
dsimp [N]
infer_instance
have hNclosed : IsClosed (N : Set E) := by
change IsClosed (D.invHom ⁻¹' ((closedNormalClosure R : Subgroup F) : Set F))
exact (closedNormalClosure_isClosed (F := F) R).preimage D.invHom.continuous_toFun
exact closedNormalClosure_le_closed_normal (F := E) (N := N) hNclosed
D.maps_target_relatorsProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□def toKernelTietzeData (D : RelatorMapTietzeData R S) :
KernelTietzeData (closedNormalClosure R) (closedNormalClosure S) where
toHom := D.toHom
invHom := D.invHom
mapsKernel := D.maps_closedNormalClosure
mapsTargetKernel := D.maps_target_closedNormalClosure
inv_toHom := D.inv_toHom
to_invHom := D.to_invHomThe relator-equivalence calculation follows from the product, inverse, conjugation, and substitution closure rules for normal closures.
theorem presentation (D : RelatorMapTietzeData R S) :
IsRelatorPresentationOf C (G := G) R →
IsRelatorPresentationOf C (F := E) (G := G) SThe induced pro-\(C\) map agrees with the corresponding finite-quotient construction.
Show proof
isRelatorPresentationOf_of_kernelTietzeData C D.toKernelTietzeDataProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem isRelatorPresentationOf_delete_redundant_relators
{R D : Set F} (hD : D ⊆ closedNormalClosure R) :
IsRelatorPresentationOf C (G := G) (R ∪ D) →
IsRelatorPresentationOf C (G := G) RDeleting redundant Reidemeister--Schreier relators preserves the relator presentation of the corresponding open subgroup.
Show proof
by
intro h
simpa [IsRelatorPresentationOf, closedNormalClosure_union_eq_left (F := F) hD] using hProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem isRelatorPresentationOf_add_redundant_relators
{R D : Set F} (hD : D ⊆ closedNormalClosure R) :
IsRelatorPresentationOf C (G := G) R →
IsRelatorPresentationOf C (G := G) (R ∪ D)The resulting Reidemeister--Schreier relators present the corresponding open subgroup.
Show proof
by
intro h
simpa [IsRelatorPresentationOf, closedNormalClosure_union_eq_left (F := F) hD] using hProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem isRelatorPresentationOf_delete_trivial_relators
{R D : Set F} (hD : D ⊆ ({1} : Set F)) :
IsRelatorPresentationOf C (G := G) (R ∪ D) →
IsRelatorPresentationOf C (G := G) RThe resulting Reidemeister--Schreier relators present the corresponding open subgroup.
Show proof
isRelatorPresentationOf_delete_redundant_relators C
(subset_closedNormalClosure_of_subset_singleton_one (F := F) hD)Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem isRelatorPresentationOf_add_trivial_relators
{R D : Set F} (hD : D ⊆ ({1} : Set F)) :
IsRelatorPresentationOf C (G := G) R →
IsRelatorPresentationOf C (G := G) (R ∪ D)The resulting Reidemeister--Schreier relators present the corresponding open subgroup.
Show proof
isRelatorPresentationOf_add_redundant_relators C
(subset_closedNormalClosure_of_subset_singleton_one (F := F) hD)Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□structure ProfiniteSchreierRelatorSets (F : Type u) where
rewritten : Set F
degenerate : Set F
cleaned : Set Fdef raw (S : ProfiniteSchreierRelatorSets F) : Set F :=
S.rewritten ∪ S.degeneratetheorem closedNormalClosure_union_eq_left (H : RedundantRelatorDeletionData (F := F) R D) :
closedNormalClosure (R ∪ D) = closedNormalClosure RAdding relators already contained in the closed normal closure does not change the closed normal closure.
Show proof
by
exact _root_.ProCGroups.Presentations.closedNormalClosure_union_eq_left (F := F) H.redundantProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem relatorTietze_union_left (H : RedundantRelatorDeletionData (F := F) R D) :
RelatorTietzeData (R ∪ D) R where
left_relatorsRelator Tietze data remain valid after adjoining relators on the left by union.
Show proof
by
intro x hx
have hx' : x ∈ closedNormalClosure (R ∪ D) :=
subset_closedNormalClosure (F := F) (R ∪ D) hx
simpa [H.closedNormalClosure_union_eq_left] using hx'
right_relators := by
intro x hx
exact subset_closedNormalClosure (F := F) (R ∪ D) (Or.inl hx)Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem isRelatorPresentationOf_delete_redundant_relators
(H : RedundantRelatorDeletionData (F := F) R D) :
IsRelatorPresentationOf C (G := G) (R ∪ D) →
IsRelatorPresentationOf C (G := G) RDeleting redundant Reidemeister--Schreier relators preserves the relator presentation of the corresponding open subgroup.
Show proof
H.relatorTietze_union_left.presentationProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□structure GeneratorDeletionTietzeData
(Fraw Fclean : Type u)
[Group Fraw] [TopologicalSpace Fraw] [IsTopologicalGroup Fraw]
[Group Fclean] [TopologicalSpace Fclean] [IsTopologicalGroup Fclean]
(Rraw : Set Fraw) (Rclean : Set Fclean) where
mapRawToClean : Fraw →* Fclean
mapCleanToRaw : Fclean →* Fraw
relators_forward : mapRawToClean '' Rraw ⊆ closedNormalClosure Rclean
relators_backward : mapCleanToRaw '' Rclean ⊆ closedNormalClosure Rraw
inverse_mod_relators_raw :
∀ x : Fraw, mapCleanToRaw (mapRawToClean x) * x⁻¹ ∈ closedNormalClosure Rraw
inverse_mod_relators_clean :
∀ x : Fclean, mapRawToClean (mapCleanToRaw x) * x⁻¹ ∈ closedNormalClosure RcleanTietze data for genuine generator deletion, where the ambient free group may change. Unlike RedundantRelatorDeletionData, this records maps between two presentation sources and inverse data modulo the respective closed normal closures.
abbrev DegenerateRelatorDeletionData (S : ProfiniteSchreierRelatorSets F) : Prop :=
RedundantRelatorDeletionData S.rewritten S.degenerateSchreier-specific redundant-relator deletion for degenerate relators.
theorem closedNormalClosure_raw_eq_rewritten (D : DegenerateRelatorDeletionData S) :
closedNormalClosure S.raw = closedNormalClosure S.rewrittenRewriting the Schreier relators preserves the closed normal closure of the raw relator set.
Show proof
by
exact D.closedNormalClosure_union_eq_leftProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem relatorTietze_raw_rewritten (D : DegenerateRelatorDeletionData S) :
RelatorTietzeData S.raw S.rewrittenThe raw and rewritten Schreier relators give equivalent normal closures after deleting degenerate relators.
Show proof
D.relatorTietze_union_leftProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem isRelatorPresentationOf_delete_degenerate_relators
(D : DegenerateRelatorDeletionData S) :
IsRelatorPresentationOf C (G := G) S.raw →
IsRelatorPresentationOf C (G := G) S.rewrittenDeleting degenerate Reidemeister--Schreier relators preserves the relator presentation of the corresponding open subgroup.
Show proof
D.relatorTietze_raw_rewritten.presentationProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□structure CleaningData (S : ProfiniteSchreierRelatorSets F) : Prop where
degenerate_le : S.degenerate ⊆ closedNormalClosure S.rewritten
rewritten_le_cleaned : S.rewritten ⊆ closedNormalClosure S.cleaned
cleaned_le_rewritten : S.cleaned ⊆ closedNormalClosure S.rewrittenThe cleaning data record that degenerate relators are Tietze-redundant and that the cleaned family generates the same closed normal subgroup as the rewritten relators.
def toDegenerateRelatorDeletionData (D : CleaningData S) :
DegenerateRelatorDeletionData S where
redundant := D.degenerate_leCleaning data for degenerate Schreier relators gives the corresponding relator-deletion data.
theorem closedNormalClosure_raw_eq_rewritten (D : CleaningData S) :
closedNormalClosure S.raw = closedNormalClosure S.rewrittenRewriting the Schreier relators preserves the closed normal closure of the raw relator set.
Show proof
by
exact D.toDegenerateRelatorDeletionData.closedNormalClosure_raw_eq_rewrittenProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem relatorTietze_raw_rewritten (D : CleaningData S) :
RelatorTietzeData S.raw S.rewrittenThe raw and rewritten Schreier relators give equivalent normal closures for the cleaning data.
Show proof
D.toDegenerateRelatorDeletionData.relatorTietze_raw_rewrittenProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem relatorTietze_rewritten_cleaned (D : CleaningData S) :
RelatorTietzeData S.rewritten S.cleaned where
left_relatorsThe rewritten relators are included in the cleaned relator set used by the Tietze data.
Show proof
D.rewritten_le_cleaned
right_relators := D.cleaned_le_rewrittenProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem relatorTietze_raw_cleaned (D : CleaningData S) :
RelatorTietzeData S.raw S.cleanedThe raw relators are included in the cleaned relator set used by the Tietze data.
Show proof
(D.relatorTietze_raw_rewritten).trans D.relatorTietze_rewritten_cleanedProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem closedNormalClosure_raw_eq_cleaned (D : CleaningData S) :
closedNormalClosure S.raw = closedNormalClosure S.cleanedCleaning the Schreier relators preserves their closed normal closure.
Show proof
D.relatorTietze_raw_cleaned.closedNormalClosure_eqProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem isRelatorPresentationOf_cleaned
(D : CleaningData S) :
IsRelatorPresentationOf C (G := G) S.raw →
IsRelatorPresentationOf C (G := G) S.cleanedThe cleaned Reidemeister--Schreier relators still present the corresponding open subgroup.
Show proof
D.relatorTietze_raw_cleaned.presentationProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem isRelatorPresentationOf_cleaned_iff
(D : CleaningData S) :
IsRelatorPresentationOf C (G := G) S.raw ↔
IsRelatorPresentationOf C (G := G) S.cleanedThe cleaned Reidemeister--Schreier relators still present the corresponding open subgroup.
Show proof
D.relatorTietze_raw_cleaned.presentation_iffProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□structure ProfiniteSchreierRelatorLists (F : Type u) where
rewritten : List F
degenerate : List F
cleaned : List FA list-level spelling of the three Schreier relator families. It is useful for statements whose input is literally a relator list in a paper or construction.
def raw (S : ProfiniteSchreierRelatorLists F) : List F :=
S.rewritten ++ S.degeneratedef toRelatorSets (S : ProfiniteSchreierRelatorLists F) :
ProfiniteSchreierRelatorSets F where
rewritten := relatorListSet S.rewritten
degenerate := relatorListSet S.degenerate
cleaned := relatorListSet S.cleanedConverting the indexed relator data to relator sets preserves the represented relator family.
@[simp] theorem relatorListSet_raw (S : ProfiniteSchreierRelatorLists F) :
relatorListSet S.raw = S.toRelatorSets.rawThe relator set associated to the raw Schreier relator list is the underlying set of raw Schreier relators.
Show proof
by
ext x
simp only [raw, relatorListSet_append, Set.mem_union, mem_relatorListSet, ProfiniteSchreierRelatorSets.raw,
toRelatorSets]Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□abbrev DegenerateRelatorDeletionData (S : ProfiniteSchreierRelatorLists F) : Prop :=
ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData S.toRelatorSetsSchreier-specific redundant-relator deletion for degenerate relators.
abbrev CleaningData (S : ProfiniteSchreierRelatorLists F) : Prop :=
ProfiniteSchreierRelatorSets.CleaningData S.toRelatorSetsThe cleaning data record that degenerate relators are Tietze-redundant and that the cleaned family generates the same closed normal subgroup as the rewritten relators.
theorem isRelatorPresentationOf_delete_degenerate_relators
{S : ProfiniteSchreierRelatorLists F}
(D : DegenerateRelatorDeletionData S) :
IsRelatorPresentationOf C (G := G) (relatorListSet S.raw) →
IsRelatorPresentationOf C (G := G) (relatorListSet S.rewritten)Deleting degenerate Reidemeister--Schreier relators preserves the relator presentation of the corresponding open subgroup.
Show proof
by
intro h
have hraw : IsRelatorPresentationOf C (G := G) S.toRelatorSets.raw := by
simpa [relatorListSet_raw] using h
have hrewritten :
IsRelatorPresentationOf C (G := G) S.toRelatorSets.rewritten :=
ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData.isRelatorPresentationOf_delete_degenerate_relators
(C := C) (G := G) D hraw
simpa [toRelatorSets] using hrewrittenProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem isRelatorPresentationOf_cleaned
{S : ProfiniteSchreierRelatorLists F}
(D : CleaningData S) :
IsRelatorPresentationOf C (G := G) (relatorListSet S.raw) →
IsRelatorPresentationOf C (G := G) (relatorListSet S.cleaned)The cleaned Reidemeister--Schreier relators still present the corresponding open subgroup.
Show proof
by
intro h
have hraw : IsRelatorPresentationOf C (G := G) S.toRelatorSets.raw := by
simpa [relatorListSet_raw] using h
have hcleaned :
IsRelatorPresentationOf C (G := G) S.toRelatorSets.cleaned :=
ProfiniteSchreierRelatorSets.CleaningData.isRelatorPresentationOf_cleaned
(C := C) (G := G) D hraw
simpa [toRelatorSets] using hcleanedProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem isRelatorPresentationOf_cleaned_iff
{S : ProfiniteSchreierRelatorLists F}
(D : CleaningData S) :
IsRelatorPresentationOf C (G := G) (relatorListSet S.raw) ↔
IsRelatorPresentationOf C (G := G) (relatorListSet S.cleaned)The cleaned Reidemeister--Schreier relators still present the corresponding open subgroup.
Show proof
by
have hsets :
IsRelatorPresentationOf C (G := G) S.toRelatorSets.raw ↔
IsRelatorPresentationOf C (G := G) S.toRelatorSets.cleaned :=
ProfiniteSchreierRelatorSets.CleaningData.isRelatorPresentationOf_cleaned_iff
(C := C) (G := G) D
simpa [relatorListSet_raw, toRelatorSets] using hsetsProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□structure ProfiniteSchreierRelatorFinsets (F : Type u) where
rewritten : Finset F
degenerate : Finset F
cleaned : Finset FA finset-level spelling of the three Schreier relator families.
def raw [DecidableEq F] (S : ProfiniteSchreierRelatorFinsets F) : Finset F :=
S.rewritten ∪ S.degeneratedef toRelatorSets (S : ProfiniteSchreierRelatorFinsets F) :
ProfiniteSchreierRelatorSets F where
rewritten := relatorFinsetSet S.rewritten
degenerate := relatorFinsetSet S.degenerate
cleaned := relatorFinsetSet S.cleanedConverting the indexed relator data to relator sets preserves the represented relator family.
@[simp] theorem relatorFinsetSet_raw [DecidableEq F] (S : ProfiniteSchreierRelatorFinsets F) :
relatorFinsetSet S.raw = S.toRelatorSets.rawThe relator set associated to the raw Schreier relator finset is the underlying set of raw Schreier relators.
Show proof
by
ext x
simp only [raw, relatorFinsetSet_union, Set.mem_union, mem_relatorFinsetSet, ProfiniteSchreierRelatorSets.raw,
toRelatorSets]Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□abbrev DegenerateRelatorDeletionData (S : ProfiniteSchreierRelatorFinsets F) : Prop :=
ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData S.toRelatorSetsSchreier-specific redundant-relator deletion for degenerate relators.
abbrev CleaningData (S : ProfiniteSchreierRelatorFinsets F) : Prop :=
ProfiniteSchreierRelatorSets.CleaningData S.toRelatorSetsThe cleaning data record that degenerate relators are Tietze-redundant and that the cleaned family generates the same closed normal subgroup as the rewritten relators.
theorem isRelatorPresentationOf_delete_degenerate_relators
[DecidableEq F] {S : ProfiniteSchreierRelatorFinsets F}
(D : DegenerateRelatorDeletionData S) :
IsRelatorPresentationOf C (G := G) (relatorFinsetSet S.raw) →
IsRelatorPresentationOf C (G := G) (relatorFinsetSet S.rewritten)Deleting degenerate Reidemeister--Schreier relators preserves the relator presentation of the corresponding open subgroup.
Show proof
by
intro h
have hraw : IsRelatorPresentationOf C (G := G) S.toRelatorSets.raw := by
simpa [relatorFinsetSet_raw] using h
have hrewritten :
IsRelatorPresentationOf C (G := G) S.toRelatorSets.rewritten :=
ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData.isRelatorPresentationOf_delete_degenerate_relators
(C := C) (G := G) D hraw
simpa [toRelatorSets] using hrewrittenProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem isRelatorPresentationOf_cleaned
[DecidableEq F] {S : ProfiniteSchreierRelatorFinsets F}
(D : CleaningData S) :
IsRelatorPresentationOf C (G := G) (relatorFinsetSet S.raw) →
IsRelatorPresentationOf C (G := G) (relatorFinsetSet S.cleaned)The cleaned Reidemeister--Schreier relators still present the corresponding open subgroup.
Show proof
by
intro h
have hraw : IsRelatorPresentationOf C (G := G) S.toRelatorSets.raw := by
simpa [relatorFinsetSet_raw] using h
have hcleaned :
IsRelatorPresentationOf C (G := G) S.toRelatorSets.cleaned :=
ProfiniteSchreierRelatorSets.CleaningData.isRelatorPresentationOf_cleaned
(C := C) (G := G) D hraw
simpa [toRelatorSets] using hcleanedProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□structure ProfiniteSchreierRewritingRelatorSets
(Q : Type v) (A : Type w) (F : Type u) where
tau : Q → A → F
transversal : Set Q
originalRelators : Set A
degenerate : Set F
cleaned : Set FSchreier relator data built directly from a rewriting map \(\tau\). The rewritten relators are definitionally \(\{\\(\tau\)(t,r) \mid t \in \mathrm{transversal},\ r \in \mathrm{originalRelators}\}\).
def rewritten (S : ProfiniteSchreierRewritingRelatorSets Q A F) : Set F :=
schreierRelatorSet S.tau S.transversal S.originalRelatorsThe rewritten relator family is obtained by applying Schreier rewriting to each transversal-relator pair.
def toRelatorSets (S : ProfiniteSchreierRewritingRelatorSets Q A F) :
ProfiniteSchreierRelatorSets F where
rewritten := S.rewritten
degenerate := S.degenerate
cleaned := S.cleanedConverting the indexed relator data to relator sets preserves the represented relator family.
def raw (S : ProfiniteSchreierRewritingRelatorSets Q A F) : Set F :=
S.toRelatorSets.rawabbrev DegenerateRelatorDeletionData
(S : ProfiniteSchreierRewritingRelatorSets Q A F) : Prop :=
ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData S.toRelatorSetsSchreier-specific redundant-relator deletion for degenerate relators.
abbrev CleaningData
(S : ProfiniteSchreierRewritingRelatorSets Q A F) : Prop :=
ProfiniteSchreierRelatorSets.CleaningData S.toRelatorSetsThe cleaning data record that degenerate relators are Tietze-redundant and that the cleaned family generates the same closed normal subgroup as the rewritten relators.
theorem isRelatorPresentationOf_delete_degenerate_relators
{S : ProfiniteSchreierRewritingRelatorSets Q A F}
(D : DegenerateRelatorDeletionData S) :
IsRelatorPresentationOf C (G := G) S.toRelatorSets.raw →
IsRelatorPresentationOf C (G := G) S.toRelatorSets.rewrittenDeleting degenerate Reidemeister--Schreier relators preserves the relator presentation of the corresponding open subgroup.
Show proof
by
intro h
exact
ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData.isRelatorPresentationOf_delete_degenerate_relators
(C := C) (G := G) D hProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem isRelatorPresentationOf_cleaned
{S : ProfiniteSchreierRewritingRelatorSets Q A F}
(D : CleaningData S) :
IsRelatorPresentationOf C (G := G) S.toRelatorSets.raw →
IsRelatorPresentationOf C (G := G) S.toRelatorSets.cleanedThe cleaned Reidemeister--Schreier relators still present the corresponding open subgroup.
Show proof
by
intro h
exact ProfiniteSchreierRelatorSets.CleaningData.isRelatorPresentationOf_cleaned
(C := C) (G := G) D hProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□structure ProfiniteSchreierRewritingRelatorLists
(Q : Type v) (A : Type w) (F : Type u) where
tau : Q → A → F
transversal : List Q
originalRelators : List A
degenerate : List F
cleaned : List FList-level Schreier relator data built from a rewriting map \(\tau\).
def rewritten (S : ProfiniteSchreierRewritingRelatorLists Q A F) : List F :=
schreierRelatorList S.tau S.transversal S.originalRelatorsThe rewritten relator family is obtained by applying Schreier rewriting to each transversal-relator pair.
def toRelatorLists (S : ProfiniteSchreierRewritingRelatorLists Q A F) :
ProfiniteSchreierRelatorLists F where
rewritten := S.rewritten
degenerate := S.degenerate
cleaned := S.cleanedConverting the rewritten relator data to lists preserves the represented relator family.
def raw (S : ProfiniteSchreierRewritingRelatorLists Q A F) : List F :=
S.toRelatorLists.rawabbrev DegenerateRelatorDeletionData
(S : ProfiniteSchreierRewritingRelatorLists Q A F) : Prop :=
ProfiniteSchreierRelatorLists.DegenerateRelatorDeletionData S.toRelatorListsSchreier-specific redundant-relator deletion for degenerate relators.
abbrev CleaningData
(S : ProfiniteSchreierRewritingRelatorLists Q A F) : Prop :=
ProfiniteSchreierRelatorLists.CleaningData S.toRelatorListsThe cleaning data record that degenerate relators are Tietze-redundant and that the cleaned family generates the same closed normal subgroup as the rewritten relators.
theorem isRelatorPresentationOf_delete_degenerate_relators
{S : ProfiniteSchreierRewritingRelatorLists Q A F}
(D : DegenerateRelatorDeletionData S) :
IsRelatorPresentationOf C (G := G) (relatorListSet S.raw) →
IsRelatorPresentationOf C (G := G) (relatorListSet S.rewritten)Deleting degenerate Reidemeister--Schreier relators preserves the relator presentation of the corresponding open subgroup.
Show proof
ProfiniteSchreierRelatorLists.isRelatorPresentationOf_delete_degenerate_relators
(C := C) (G := G) DProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem isRelatorPresentationOf_cleaned
{S : ProfiniteSchreierRewritingRelatorLists Q A F}
(D : CleaningData S) :
IsRelatorPresentationOf C (G := G) (relatorListSet S.raw) →
IsRelatorPresentationOf C (G := G) (relatorListSet S.cleaned)The cleaned Reidemeister--Schreier relators still present the corresponding open subgroup.
Show proof
ProfiniteSchreierRelatorLists.isRelatorPresentationOf_cleaned
(C := C) (G := G) DProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□structure ProfiniteSchreierRewritingRelatorFinsets
(Q : Type v) (A : Type w) (F : Type u) where
tau : Q → A → F
transversal : Finset Q
originalRelators : Finset A
degenerate : Finset F
cleaned : Finset FFinset-level Schreier relator data built from a rewriting map \(\tau\).
def rewritten [DecidableEq F] (S : ProfiniteSchreierRewritingRelatorFinsets Q A F) :
Finset F :=
schreierRelatorFinset S.tau S.transversal S.originalRelatorsThe rewritten relator family is obtained by applying Schreier rewriting to each transversal-relator pair.
def toRelatorFinsets [DecidableEq F] (S : ProfiniteSchreierRewritingRelatorFinsets Q A F) :
ProfiniteSchreierRelatorFinsets F where
rewritten := S.rewritten
degenerate := S.degenerate
cleaned := S.cleanedConverting the rewritten relator data to finsets preserves the represented relator family.
def raw [DecidableEq F] (S : ProfiniteSchreierRewritingRelatorFinsets Q A F) :
Finset F :=
S.toRelatorFinsets.rawabbrev DegenerateRelatorDeletionData
[DecidableEq F] (S : ProfiniteSchreierRewritingRelatorFinsets Q A F) : Prop :=
ProfiniteSchreierRelatorFinsets.DegenerateRelatorDeletionData S.toRelatorFinsetsSchreier-specific redundant-relator deletion for degenerate relators.
abbrev CleaningData
[DecidableEq F] (S : ProfiniteSchreierRewritingRelatorFinsets Q A F) : Prop :=
ProfiniteSchreierRelatorFinsets.CleaningData S.toRelatorFinsetsThe cleaning data record that degenerate relators are Tietze-redundant and that the cleaned family generates the same closed normal subgroup as the rewritten relators.
theorem isRelatorPresentationOf_delete_degenerate_relators
[DecidableEq F] {S : ProfiniteSchreierRewritingRelatorFinsets Q A F}
(D : DegenerateRelatorDeletionData S) :
IsRelatorPresentationOf C (G := G) (relatorFinsetSet S.raw) →
IsRelatorPresentationOf C (G := G) (relatorFinsetSet S.rewritten)Deleting degenerate Reidemeister--Schreier relators preserves the relator presentation of the corresponding open subgroup.
Show proof
ProfiniteSchreierRelatorFinsets.isRelatorPresentationOf_delete_degenerate_relators
(C := C) (G := G) DProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem isRelatorPresentationOf_cleaned
[DecidableEq F] {S : ProfiniteSchreierRewritingRelatorFinsets Q A F}
(D : CleaningData S) :
IsRelatorPresentationOf C (G := G) (relatorFinsetSet S.raw) →
IsRelatorPresentationOf C (G := G) (relatorFinsetSet S.cleaned)The cleaned Reidemeister--Schreier relators still present the corresponding open subgroup.
Show proof
ProfiniteSchreierRelatorFinsets.isRelatorPresentationOf_cleaned
(C := C) (G := G) DProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□