ProCGroups.Presentations.SchreierTietze.Data
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 schreierPresentationHom
(π : F →ₜ* G) (U : Subgroup G)
(α : E →ₜ* presentationSubgroupPreimage π U) : E →ₜ* U :=
(restrictPresentationHom π U).comp αThe presentation map to an open-subgroup target after a proposed Schreier source maps into the source preimage.
def openSchreierPresentationHom
(π : F →ₜ* G) (U : OpenSubgroup G)
(α : E →ₜ* presentationSubgroupPreimage π (U : Subgroup G)) :
E →ₜ* ↥(U : Subgroup G) :=
schreierPresentationHom π (U : Subgroup G) αThe same map, specialized to an open subgroup target.
structure SchreierRelatorPresentationData
(π : F →ₜ* G) (U : Subgroup G) (R : Set E) where
targetProC : ProCGroups.ProC.IsProCGroup C U
sourceToPreimage : E →ₜ* presentationSubgroupPreimage π U
sourceToOpen_surjective :
Function.Surjective (schreierPresentationHom π U sourceToPreimage)
kernel_eq_closedNormalClosure :
(schreierPresentationHom π U sourceToPreimage).toMonoidHom.ker =
closedNormalClosure RThe Reidemeister--Schreier relator transformation Schreier Relator Presentation Data preserves the normal-closure relation in the presented group.
structure OpenSubgroupSchreierRelatorPresentationData
(π : F →ₜ* G) (U : OpenSubgroup G) (R : Set E) where
sourceToPreimage : E →ₜ* presentationSubgroupPreimage π (U : Subgroup G)
sourceToOpen_surjective :
Function.Surjective (openSchreierPresentationHom π U sourceToPreimage)
kernel_eq_closedNormalClosure :
(openSchreierPresentationHom π U sourceToPreimage).toMonoidHom.ker =
closedNormalClosure ROpen-subgroup Schreier presentation data with the rewriting map, surjectivity, and kernel identity recorded explicitly.
theorem isRelatorPresentationOf
(D : SchreierRelatorPresentationData C π U R) :
IsRelatorPresentationOf C (F := E) (G := U) RThe resulting Reidemeister--Schreier relators present the corresponding open subgroup.
Show proof
by
exact ⟨D.targetProC, schreierPresentationHom π U D.sourceToPreimage,
D.sourceToOpen_surjective, D.kernel_eq_closedNormalClosure⟩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 clean
(D : SchreierRelatorPresentationData C π U R)
(T : RelatorTietzeData R S) :
SchreierRelatorPresentationData C π U S where
targetProC := D.targetProC
sourceToPreimage := D.sourceToPreimage
sourceToOpen_surjective := D.sourceToOpen_surjective
kernel_eq_closedNormalClosure := by
simpa [T.closedNormalClosure_eq] using D.kernel_eq_closedNormalClosureTietze-cleaning the relator set transports Schreier relator presentation data to the cleaned relators.
def delete_redundant_relators
(Ddata : SchreierRelatorPresentationData C π U (R ∪ D))
(hD : D ⊆ closedNormalClosure R) :
SchreierRelatorPresentationData C π U R where
targetProC := Ddata.targetProC
sourceToPreimage := Ddata.sourceToPreimage
sourceToOpen_surjective := Ddata.sourceToOpen_surjective
kernel_eq_closedNormalClosure := by
simpa [closedNormalClosure_union_eq_left (F := E) hD] using
Ddata.kernel_eq_closedNormalClosureDeleting redundant Reidemeister--Schreier relators preserves the relator presentation of the corresponding open subgroup.
def add_redundant_relators
(Ddata : SchreierRelatorPresentationData C π U R)
(hD : D ⊆ closedNormalClosure R) :
SchreierRelatorPresentationData C π U (R ∪ D) where
targetProC := Ddata.targetProC
sourceToPreimage := Ddata.sourceToPreimage
sourceToOpen_surjective := Ddata.sourceToOpen_surjective
kernel_eq_closedNormalClosure := by
simpa [closedNormalClosure_union_eq_left (F := E) hD] using
Ddata.kernel_eq_closedNormalClosureAdding redundant relators preserves the corresponding relator presentation data.
def delete_trivial_relators
(Ddata : SchreierRelatorPresentationData C π U (R ∪ D))
(hD : D ⊆ ({1} : Set E)) :
SchreierRelatorPresentationData C π U R :=
Ddata.delete_redundant_relators
(subset_closedNormalClosure_of_subset_singleton_one (F := E) hD)Deleting trivial relators preserves the corresponding presentation data.
def add_trivial_relators
(Ddata : SchreierRelatorPresentationData C π U R)
(hD : D ⊆ ({1} : Set E)) :
SchreierRelatorPresentationData C π U (R ∪ D) :=
Ddata.add_redundant_relators
(subset_closedNormalClosure_of_subset_singleton_one (F := E) hD)Adding trivial relators preserves the corresponding relator presentation data.
def delete_degenerate_schreier_relators
{T : ProfiniteSchreierRelatorSets E}
(Ddata : SchreierRelatorPresentationData C π U T.raw)
(H : ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData T) :
SchreierRelatorPresentationData C π U T.rewritten :=
Ddata.clean H.relatorTietze_raw_rewrittenDeleting degenerate Schreier relators preserves the corresponding presentation data.
def clean_schreier_relators
{T : ProfiniteSchreierRelatorSets E}
(Ddata : SchreierRelatorPresentationData C π U T.raw)
(H : ProfiniteSchreierRelatorSets.CleaningData T) :
SchreierRelatorPresentationData C π U T.cleaned :=
Ddata.clean H.relatorTietze_raw_cleaneddef targetProC
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hG : ProCGroups.ProC.IsProCGroup C G) :
ProCGroups.ProC.IsProCGroup C ↥(U : Subgroup G) := by
have hUclosed : IsClosed (((U : Subgroup G) : Set G)) :=
ProCGroups.openSubgroup_isClosed (G := G) U
exact ProCGroups.ProC.IsProCGroup.of_isClosed_subgroup_of_fullFormation
hC hG (U : Subgroup G) hUclosedThe target of a free presentation is pro-\(C\).
def toSchreierRelatorPresentationData
(Ddata : OpenSubgroupSchreierRelatorPresentationData π U R)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hG : ProCGroups.ProC.IsProCGroup C G) :
SchreierRelatorPresentationData C π (U : Subgroup G) R where
targetProC := targetProC (C := C) (U := U) hC hG
sourceToPreimage := Ddata.sourceToPreimage
sourceToOpen_surjective := Ddata.sourceToOpen_surjective
kernel_eq_closedNormalClosure := Ddata.kernel_eq_closedNormalClosureOpen-subgroup Schreier relator presentation data forgets to the ordinary Schreier relator presentation data.
theorem isRelatorPresentationOf
(Ddata : OpenSubgroupSchreierRelatorPresentationData π U R)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hG : ProCGroups.ProC.IsProCGroup C G) :
IsRelatorPresentationOf C (F := E) (G := ↥(U : Subgroup G)) RThe resulting Reidemeister--Schreier relators present the corresponding open subgroup.
Show proof
(Ddata.toSchreierRelatorPresentationData hC hG).isRelatorPresentationOfProof. 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_of_ambientPresentation
{R₀ : Set F}
(Ddata : OpenSubgroupSchreierRelatorPresentationData π U R)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hambient : IsRelatorPresentationOf C (F := F) (G := G) R₀) :
IsRelatorPresentationOf C (F := E) (G := ↥(U : Subgroup G)) RThe resulting Reidemeister--Schreier relators present the corresponding open subgroup.
Show proof
Ddata.isRelatorPresentationOf hC hambient.1Proof. 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 clean
(Ddata : OpenSubgroupSchreierRelatorPresentationData π U R)
(T : RelatorTietzeData R S) :
OpenSubgroupSchreierRelatorPresentationData π U S where
sourceToPreimage := Ddata.sourceToPreimage
sourceToOpen_surjective := Ddata.sourceToOpen_surjective
kernel_eq_closedNormalClosure := by
simpa [T.closedNormalClosure_eq] using Ddata.kernel_eq_closedNormalClosureTietze-cleaning the relator set transports open-subgroup Schreier relator presentation data to the cleaned relators.
def delete_redundant_relators
(Ddata : OpenSubgroupSchreierRelatorPresentationData π U (R ∪ D))
(hD : D ⊆ closedNormalClosure R) :
OpenSubgroupSchreierRelatorPresentationData π U R where
sourceToPreimage := Ddata.sourceToPreimage
sourceToOpen_surjective := Ddata.sourceToOpen_surjective
kernel_eq_closedNormalClosure := by
simpa [closedNormalClosure_union_eq_left (F := E) hD] using
Ddata.kernel_eq_closedNormalClosureDeleting redundant Reidemeister--Schreier relators preserves the relator presentation of the corresponding open subgroup.
def add_redundant_relators
(Ddata : OpenSubgroupSchreierRelatorPresentationData π U R)
(hD : D ⊆ closedNormalClosure R) :
OpenSubgroupSchreierRelatorPresentationData π U (R ∪ D) where
sourceToPreimage := Ddata.sourceToPreimage
sourceToOpen_surjective := Ddata.sourceToOpen_surjective
kernel_eq_closedNormalClosure := by
simpa [closedNormalClosure_union_eq_left (F := E) hD] using
Ddata.kernel_eq_closedNormalClosureAdding redundant relators preserves the corresponding relator presentation data.
def delete_trivial_relators
(Ddata : OpenSubgroupSchreierRelatorPresentationData π U (R ∪ D))
(hD : D ⊆ ({1} : Set E)) :
OpenSubgroupSchreierRelatorPresentationData π U R :=
Ddata.delete_redundant_relators
(subset_closedNormalClosure_of_subset_singleton_one (F := E) hD)Deleting trivial relators preserves the corresponding presentation data.
def add_trivial_relators
(Ddata : OpenSubgroupSchreierRelatorPresentationData π U R)
(hD : D ⊆ ({1} : Set E)) :
OpenSubgroupSchreierRelatorPresentationData π U (R ∪ D) :=
Ddata.add_redundant_relators
(subset_closedNormalClosure_of_subset_singleton_one (F := E) hD)Adding trivial relators preserves the corresponding relator presentation data.
def delete_degenerate_schreier_relators
{T : ProfiniteSchreierRelatorSets E}
(Ddata : OpenSubgroupSchreierRelatorPresentationData π U T.raw)
(H : ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData T) :
OpenSubgroupSchreierRelatorPresentationData π U T.rewritten :=
Ddata.clean H.relatorTietze_raw_rewrittenDeleting degenerate Schreier relators preserves the corresponding presentation data.
def clean_schreier_relators
{T : ProfiniteSchreierRelatorSets E}
(Ddata : OpenSubgroupSchreierRelatorPresentationData π U T.raw)
(H : ProfiniteSchreierRelatorSets.CleaningData T) :
OpenSubgroupSchreierRelatorPresentationData π U T.cleaned :=
Ddata.clean H.relatorTietze_raw_cleanedtheorem cleanedRelatorPresentationOf_of_ambientPresentation
{R₀ : Set F} {T : ProfiniteSchreierRelatorSets E}
(Ddata : OpenSubgroupSchreierRelatorPresentationData π U T.raw)
(H : ProfiniteSchreierRelatorSets.CleaningData T)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hambient : IsRelatorPresentationOf C (F := F) (G := G) R₀) :
IsRelatorPresentationOf C (F := E) (G := ↥(U : Subgroup G)) T.cleanedThe cleaned Reidemeister--Schreier relators still present the corresponding open subgroup.
Show proof
(Ddata.clean_schreier_relators H).isRelatorPresentationOf hC hambient.1Proof. 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 SchreierStandardPresentationData
(π : F →ₜ* G) (U : Subgroup G)
(rawRelators : Set E) (standardRelators : Set Eₛ) where
rawData : SchreierRelatorPresentationData C π U rawRelators
standardTietze : RelatorMapTietzeData rawRelators standardRelatorsA standard-form Schreier presentation package when the final Tietze step may change the presentation source, as in deletion of redundant Schreier generators.
theorem isRelatorPresentationOf
(D : SchreierStandardPresentationData C π U rawRelators standardRelators) :
IsRelatorPresentationOf C (F := Eₛ) (G := U) standardRelatorsThe resulting Reidemeister--Schreier relators present the corresponding open subgroup.
Show proof
D.standardTietze.presentation (C := C) (G := U) D.rawData.isRelatorPresentationOfProof. 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 ofCleaningData
{T : ProfiniteSchreierRelatorSets E}
(Ddata : SchreierRelatorPresentationData C π U T.raw)
(H : ProfiniteSchreierRelatorSets.CleaningData T) :
SchreierStandardPresentationData C π U T.raw T.cleaned where
rawData := Ddata
standardTietze :=
RelatorMapTietzeData.ofRelatorTietzeData H.relatorTietze_raw_cleanedCleaning data produces the corresponding standard Schreier presentation data.
structure OpenSubgroupSchreierStandardPresentationData
(π : F →ₜ* G) (U : OpenSubgroup G)
(rawRelators : Set E) (standardRelators : Set Eₛ) where
rawData : OpenSubgroupSchreierRelatorPresentationData π U rawRelators
standardTietze : RelatorMapTietzeData rawRelators standardRelatorsStandard-form data for an open subgroup, consisting of a raw Schreier presentation datum and a Tietze datum from the raw source to the final standard source.
theorem isRelatorPresentationOf
(D : OpenSubgroupSchreierStandardPresentationData π U rawRelators standardRelators)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hG : ProCGroups.ProC.IsProCGroup C G) :
IsRelatorPresentationOf C (F := Eₛ) (G := ↥(U : Subgroup G)) standardRelatorsThe resulting Reidemeister--Schreier relators present the corresponding open subgroup.
Show proof
D.standardTietze.presentation (C := C) (G := ↥(U : Subgroup G))
(D.rawData.isRelatorPresentationOf hC hG)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_of_ambientPresentation
{R₀ : Set F}
(D : OpenSubgroupSchreierStandardPresentationData π U rawRelators standardRelators)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hambient : IsRelatorPresentationOf C (F := F) (G := G) R₀) :
IsRelatorPresentationOf C (F := Eₛ) (G := ↥(U : Subgroup G)) standardRelatorsThe resulting Reidemeister--Schreier relators present the corresponding open subgroup.
Show proof
D.isRelatorPresentationOf hC hambient.1Proof. 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_of_ambientFreeRelatorPresentation
{X : Type u} [TopologicalSpace X] {ι : X → F} {R₀ : Set F}
(D : OpenSubgroupSchreierStandardPresentationData π U rawRelators standardRelators)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hambient : IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι R₀) :
IsRelatorPresentationOf C (F := Eₛ) (G := ↥(U : Subgroup G)) standardRelatorsThe resulting Reidemeister--Schreier relators present the corresponding open subgroup.
Show proof
D.isRelatorPresentationOf hC
(IsFreeRelatorPresentationOfClass.isRelatorPresentationOf (C := C) (G := G) hambient).1Proof. 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 ofCleaningData
{T : ProfiniteSchreierRelatorSets E}
(Ddata : OpenSubgroupSchreierRelatorPresentationData π U T.raw)
(H : ProfiniteSchreierRelatorSets.CleaningData T) :
OpenSubgroupSchreierStandardPresentationData π U T.raw T.cleaned where
rawData := Ddata
standardTietze :=
RelatorMapTietzeData.ofRelatorTietzeData H.relatorTietze_raw_cleanedCleaning data produces the corresponding standard Schreier presentation data.
theorem isRelatorPresentationOf_ofCleaningData
{T : ProfiniteSchreierRelatorSets E}
(Ddata : OpenSubgroupSchreierRelatorPresentationData π U T.raw)
(H : ProfiniteSchreierRelatorSets.CleaningData T)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hG : ProCGroups.ProC.IsProCGroup C G) :
IsRelatorPresentationOf C (F := E) (G := ↥(U : Subgroup G)) T.cleanedThe resulting Reidemeister--Schreier relators present the corresponding open subgroup.
Show proof
(ofCleaningData Ddata H).isRelatorPresentationOf hC hGProof. 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_ofCleaningData_of_ambientFreeRelatorPresentation
{X : Type u} [TopologicalSpace X] {ι : X → F} {R₀ : Set F}
{T : ProfiniteSchreierRelatorSets E}
(Ddata : OpenSubgroupSchreierRelatorPresentationData π U T.raw)
(H : ProfiniteSchreierRelatorSets.CleaningData T)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hambient : IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι R₀) :
IsRelatorPresentationOf C (F := E) (G := ↥(U : Subgroup G)) T.cleanedThe resulting Reidemeister--Schreier relators present the corresponding open subgroup.
Show proof
(ofCleaningData Ddata H).isRelatorPresentationOf_of_ambientFreeRelatorPresentation
hC hambientProof. 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 SchreierFreeRelatorPresentationData
(η : Y → E) (π : F →ₜ* G) (U : Subgroup G) (R : Set E) where
freeSource :
ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) η
relatorData : SchreierRelatorPresentationData C π U RA Schreier relator-presentation datum whose source is explicitly the free pro-\(C\) group on the chosen Schreier generators. This is the direct mathematical shape of \(U=(\text{Schreier generators}\mid\text{rewritten relators})_{\mathrm{pro}-C}\).
theorem isFreeRelatorPresentationOfClass
(Ddata : SchreierFreeRelatorPresentationData C η π U R) :
IsFreeRelatorPresentationOfClass C (F := E) (G := U) η RThe resulting Reidemeister--Schreier free-relator presentation belongs to the required class.
Show proof
by
exact ⟨Ddata.freeSource, by simpa using Ddata.relatorData.targetProC,
schreierPresentationHom π U Ddata.relatorData.sourceToPreimage,
Ddata.relatorData.sourceToOpen_surjective,
Ddata.relatorData.kernel_eq_closedNormalClosure⟩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
(Ddata : SchreierFreeRelatorPresentationData C η π U R) :
IsRelatorPresentationOf C (F := E) (G := U) RThe resulting Reidemeister--Schreier relators present the corresponding open subgroup.
Show proof
Ddata.isFreeRelatorPresentationOfClass.isRelatorPresentationOfProof. 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 clean
(Ddata : SchreierFreeRelatorPresentationData C η π U R)
(T : RelatorTietzeData R S) :
SchreierFreeRelatorPresentationData C η π U S where
freeSource := Ddata.freeSource
relatorData := Ddata.relatorData.clean TTietze-cleaning the relator set preserves the free Schreier relator presentation package.
def delete_redundant_relators
(Ddata : SchreierFreeRelatorPresentationData C η π U (R ∪ D))
(hD : D ⊆ closedNormalClosure R) :
SchreierFreeRelatorPresentationData C η π U R where
freeSource := Ddata.freeSource
relatorData := Ddata.relatorData.delete_redundant_relators hDDeleting redundant Reidemeister--Schreier relators preserves the relator presentation of the corresponding open subgroup.
def delete_trivial_relators
(Ddata : SchreierFreeRelatorPresentationData C η π U (R ∪ D))
(hD : D ⊆ ({1} : Set E)) :
SchreierFreeRelatorPresentationData C η π U R where
freeSource := Ddata.freeSource
relatorData := Ddata.relatorData.delete_trivial_relators hDDeleting trivial relators preserves the corresponding presentation data.
def delete_degenerate_schreier_relators
{T : ProfiniteSchreierRelatorSets E}
(Ddata : SchreierFreeRelatorPresentationData C η π U T.raw)
(H : ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData T) :
SchreierFreeRelatorPresentationData C η π U T.rewritten :=
Ddata.clean H.relatorTietze_raw_rewrittenDeleting degenerate Schreier relators preserves the corresponding presentation data.
def clean_schreier_relators
{T : ProfiniteSchreierRelatorSets E}
(Ddata : SchreierFreeRelatorPresentationData C η π U T.raw)
(H : ProfiniteSchreierRelatorSets.CleaningData T) :
SchreierFreeRelatorPresentationData C η π U T.cleaned :=
Ddata.clean H.relatorTietze_raw_cleanedstructure OpenSubgroupSchreierFreeRelatorPresentationData
(η : Y → E) (π : F →ₜ* G) (U : OpenSubgroup G) (R : Set E) where
freeSource :
ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) η
relatorData : OpenSubgroupSchreierRelatorPresentationData π U RThe open-subgroup version of Schreier free-relator presentation data. The open subgroup is shown to be pro-\(C\) from the ambient presentation and full-formation hypothesis.
theorem isFreeRelatorPresentationOfClass
(Ddata : OpenSubgroupSchreierFreeRelatorPresentationData C η π U R)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hG : ProCGroups.ProC.IsProCGroup C G) :
IsFreeRelatorPresentationOfClass C (F := E) (G := ↥(U : Subgroup G)) η RThe resulting Reidemeister--Schreier free-relator presentation belongs to the required class.
Show proof
by
have hU : ProCGroups.ProC.IsProCGroup C ↥(U : Subgroup G) :=
OpenSubgroupSchreierRelatorPresentationData.targetProC (C := C) (U := U) hC hG
exact ⟨Ddata.freeSource, by simpa using hU,
openSchreierPresentationHom π U Ddata.relatorData.sourceToPreimage,
Ddata.relatorData.sourceToOpen_surjective,
Ddata.relatorData.kernel_eq_closedNormalClosure⟩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 isFreeRelatorPresentationOfClass_of_ambientPresentation
{R₀ : Set F}
(Ddata : OpenSubgroupSchreierFreeRelatorPresentationData C η π U R)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hambient : IsRelatorPresentationOf C (F := F) (G := G) R₀) :
IsFreeRelatorPresentationOfClass C (F := E) (G := ↥(U : Subgroup G)) η RThe resulting Reidemeister--Schreier free-relator presentation belongs to the required class.
Show proof
Ddata.isFreeRelatorPresentationOfClass hC hambient.1Proof. 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 isFreeRelatorPresentationOfClass_of_ambientFreeRelatorPresentation
{X : Type u} [TopologicalSpace X] {ι : X → F} {R₀ : Set F}
(Ddata : OpenSubgroupSchreierFreeRelatorPresentationData C η π U R)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hambient : IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι R₀) :
IsFreeRelatorPresentationOfClass C (F := E) (G := ↥(U : Subgroup G)) η RThe resulting Reidemeister--Schreier free-relator presentation belongs to the required class.
Show proof
Ddata.isFreeRelatorPresentationOfClass hC
(IsFreeRelatorPresentationOfClass.isRelatorPresentationOf
(C := C) (G := G) hambient).1Proof. 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 clean
(Ddata : OpenSubgroupSchreierFreeRelatorPresentationData C η π U R)
(T : RelatorTietzeData R S) :
OpenSubgroupSchreierFreeRelatorPresentationData C η π U S where
freeSource := Ddata.freeSource
relatorData := Ddata.relatorData.clean TTietze-cleaning the relator set preserves the open-subgroup free Schreier relator presentation package.
def delete_redundant_relators
(Ddata : OpenSubgroupSchreierFreeRelatorPresentationData C η π U (R ∪ D))
(hD : D ⊆ closedNormalClosure R) :
OpenSubgroupSchreierFreeRelatorPresentationData C η π U R where
freeSource := Ddata.freeSource
relatorData := Ddata.relatorData.delete_redundant_relators hDDeleting redundant Reidemeister--Schreier relators preserves the relator presentation of the corresponding open subgroup.
def delete_trivial_relators
(Ddata : OpenSubgroupSchreierFreeRelatorPresentationData C η π U (R ∪ D))
(hD : D ⊆ ({1} : Set E)) :
OpenSubgroupSchreierFreeRelatorPresentationData C η π U R where
freeSource := Ddata.freeSource
relatorData := Ddata.relatorData.delete_trivial_relators hDDeleting trivial relators preserves the corresponding presentation data.
def delete_degenerate_schreier_relators
{T : ProfiniteSchreierRelatorSets E}
(Ddata : OpenSubgroupSchreierFreeRelatorPresentationData C η π U T.raw)
(H : ProfiniteSchreierRelatorSets.DegenerateRelatorDeletionData T) :
OpenSubgroupSchreierFreeRelatorPresentationData C η π U T.rewritten :=
Ddata.clean H.relatorTietze_raw_rewrittenDeleting degenerate Schreier relators preserves the corresponding presentation data.
def clean_schreier_relators
{T : ProfiniteSchreierRelatorSets E}
(Ddata : OpenSubgroupSchreierFreeRelatorPresentationData C η π U T.raw)
(H : ProfiniteSchreierRelatorSets.CleaningData T) :
OpenSubgroupSchreierFreeRelatorPresentationData C η π U T.cleaned :=
Ddata.clean H.relatorTietze_raw_cleanedtheorem cleanedFreeRelatorPresentationOf_of_ambientFreeRelatorPresentation
{X : Type u} [TopologicalSpace X] {ι : X → F} {R₀ : Set F}
{T : ProfiniteSchreierRelatorSets E}
(Ddata : OpenSubgroupSchreierFreeRelatorPresentationData C η π U T.raw)
(H : ProfiniteSchreierRelatorSets.CleaningData T)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hambient : IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι R₀) :
IsFreeRelatorPresentationOfClass C (F := E) (G := ↥(U : Subgroup G)) η T.cleanedThe cleaned Reidemeister--Schreier free-relator presentation induced from the ambient presentation presents the open subgroup.
Show proof
(Ddata.clean_schreier_relators H)
|>.isFreeRelatorPresentationOfClass_of_ambientFreeRelatorPresentation hC hambientProof. 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 OpenSubgroupSchreierStandardFreeRelatorPresentationData
(ηₛ : Yₛ → Eₛ) (π : F →ₜ* G) (U : OpenSubgroup G)
(rawRelators : Set E) (standardRelators : Set Eₛ) where
freeStandardSource :
ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ηₛ
standardData :
OpenSubgroupSchreierStandardPresentationData π U rawRelators standardRelatorsStandard-form free Schreier presentation data. The final source is explicitly free on the surviving Schreier generators after generator deletion.
theorem isFreeRelatorPresentationOfClass
(D : OpenSubgroupSchreierStandardFreeRelatorPresentationData
C ηₛ π U rawRelators standardRelators)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hG : ProCGroups.ProC.IsProCGroup C G) :
IsFreeRelatorPresentationOfClass C
(F := Eₛ) (G := ↥(U : Subgroup G)) ηₛ standardRelatorsThe resulting Reidemeister--Schreier free-relator presentation belongs to the required class.
Show proof
by
rcases D.standardData.isRelatorPresentationOf hC hG with
⟨hU, ρ, hρsurj, hρker⟩
exact ⟨D.freeStandardSource, by simpa using hU, ρ, hρsurj, hρker⟩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 isFreeRelatorPresentationOfClass_of_ambientFreeRelatorPresentation
{X : Type u} [TopologicalSpace X] {ι : X → F} {R₀ : Set F}
(D : OpenSubgroupSchreierStandardFreeRelatorPresentationData
C ηₛ π U rawRelators standardRelators)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hambient : IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι R₀) :
IsFreeRelatorPresentationOfClass C
(F := Eₛ) (G := ↥(U : Subgroup G)) ηₛ standardRelatorsThe resulting Reidemeister--Schreier free-relator presentation belongs to the required class.
Show proof
D.isFreeRelatorPresentationOfClass hC
(IsFreeRelatorPresentationOfClass.isRelatorPresentationOf
(C := C) (G := G) hambient).1Proof. 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 OpenSubgroupSchreierFreeRewritingPresentationData
(η : Y → E) (π : F →ₜ* G) (U : OpenSubgroup G)
(Srw : ProfiniteSchreierRewritingRelatorSets Q F E) where
freeSource :
ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) η
relatorData :
OpenSubgroupSchreierRelatorPresentationData π U Srw.toRelatorSets.rawOpen-subgroup free Schreier presentation data whose rewritten relators are definitionally constructed from a map \(\tau\).
def toRawFreeRelatorPresentationData
(Ddata : OpenSubgroupSchreierFreeRewritingPresentationData C η π U Srw) :
OpenSubgroupSchreierFreeRelatorPresentationData C η π U Srw.toRelatorSets.raw where
freeSource := Ddata.freeSource
relatorData := Ddata.relatorDataThe free rewriting presentation data forgets to the corresponding raw free-relator presentation data.
theorem rawFreeRelatorPresentationOf_of_ambientFreeRelatorPresentation
{X : Type u} [TopologicalSpace X] {ι : X → F}
(Ddata : OpenSubgroupSchreierFreeRewritingPresentationData C η π U Srw)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hambient :
IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι Srw.originalRelators) :
IsFreeRelatorPresentationOfClass C
(F := E) (G := ↥(U : Subgroup G)) η Srw.toRelatorSets.rawThe raw Reidemeister--Schreier free-relator presentation induced from the ambient presentation presents the open subgroup.
Show proof
Ddata.toRawFreeRelatorPresentationData
|>.isFreeRelatorPresentationOfClass_of_ambientFreeRelatorPresentation hC hambientProof. 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 rewrittenFreeRelatorPresentationOf_of_ambientFreeRelatorPresentation
{X : Type u} [TopologicalSpace X] {ι : X → F}
(Ddata : OpenSubgroupSchreierFreeRewritingPresentationData C η π U Srw)
(H : ProfiniteSchreierRewritingRelatorSets.DegenerateRelatorDeletionData Srw)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hambient :
IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι Srw.originalRelators) :
IsFreeRelatorPresentationOfClass C
(F := E) (G := ↥(U : Subgroup G)) η Srw.toRelatorSets.rewrittenThe rewritten Reidemeister--Schreier free-relator presentation induced from the ambient presentation presents the open subgroup.
Show proof
(Ddata.toRawFreeRelatorPresentationData.delete_degenerate_schreier_relators H)
|>.isFreeRelatorPresentationOfClass_of_ambientFreeRelatorPresentation hC hambientProof. 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 cleanedFreeRelatorPresentationOf_of_ambientFreeRelatorPresentation
{X : Type u} [TopologicalSpace X] {ι : X → F}
(Ddata : OpenSubgroupSchreierFreeRewritingPresentationData C η π U Srw)
(H : ProfiniteSchreierRewritingRelatorSets.CleaningData Srw)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hambient :
IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι Srw.originalRelators) :
IsFreeRelatorPresentationOfClass C
(F := E) (G := ↥(U : Subgroup G)) η Srw.toRelatorSets.cleanedThe cleaned Reidemeister--Schreier free-relator presentation induced from the ambient presentation presents the open subgroup.
Show proof
(Ddata.toRawFreeRelatorPresentationData.clean_schreier_relators H)
|>.isFreeRelatorPresentationOfClass_of_ambientFreeRelatorPresentation hC hambientProof. 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 OpenSubgroupSchreierStandardFreeRewritingPresentationData
(ηₛ : Yₛ → Eₛ) (π : F →ₜ* G) (U : OpenSubgroup G)
(Srw : ProfiniteSchreierRewritingRelatorSets Q F E)
(standardRelators : Set Eₛ) where
freeStandardSource :
ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ηₛ
standardData :
OpenSubgroupSchreierStandardPresentationData π U Srw.toRelatorSets.raw standardRelatorsStandard-form free Schreier presentation data whose raw relators are built from \(\tau\). The standard source may differ from the raw source after deleting redundant Schreier generators.
def toStandardFreeRelatorPresentationData
(D : OpenSubgroupSchreierStandardFreeRewritingPresentationData
C ηₛ π U Srw standardRelators) :
OpenSubgroupSchreierStandardFreeRelatorPresentationData
C ηₛ π U Srw.toRelatorSets.raw standardRelators where
freeStandardSource := D.freeStandardSource
standardData := D.standardDataThe standard free rewriting presentation data forgets to standard free-relator presentation data.
theorem isFreeRelatorPresentationOfClass_of_ambientFreeRelatorPresentation
{X : Type u} [TopologicalSpace X] {ι : X → F}
(D : OpenSubgroupSchreierStandardFreeRewritingPresentationData
C ηₛ π U Srw standardRelators)
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hambient :
IsFreeRelatorPresentationOfClass C (F := F) (G := G) ι Srw.originalRelators) :
IsFreeRelatorPresentationOfClass C
(F := Eₛ) (G := ↥(U : Subgroup G)) ηₛ standardRelatorsThe resulting Reidemeister--Schreier free-relator presentation belongs to the required class.
Show proof
D.toStandardFreeRelatorPresentationData
|>.isFreeRelatorPresentationOfClass_of_ambientFreeRelatorPresentation hC hambientProof. 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.
□