ReidemeisterSchreier.Profinite.SchreierFormula
This module develops Reidemeister--Schreier rewriting, Schreier generators, finite quotient transversals, and presentation transformations.
import
def HasFreeProCConvergingSetModel
(ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] : Prop :=
∃ Fdata : FreeProCGroupOnConvergingSetData (ProC := ProC),
Nonempty (Fdata.carrier ≃ₜ* G)G admits a free pro-\(C\) model on a converging set.
def HasFreeProCConvergingSetModelOfRank
(ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G]
(m : Cardinal) : Prop :=
∃ Fdata : FreeProCGroupOnConvergingSetData (ProC := ProC),
Nonempty (Fdata.carrier ≃ₜ* G) ∧ Cardinal.mk Fdata.basis = mG admits a free pro-\(C\) model on a converging set of cardinal m.
def SatisfiesOpenNormalSchreierFormulaAtRank
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(r : ℕ) : Prop :=
∀ U : OpenNormalSubgroup G,
Generation.topologicalRank ↥(U : Subgroup G) =
(_root_.ReidemeisterSchreier.Schreier.rankTransform r (Nat.card (G ⧸ (U : Subgroup G))) : Cardinal)A group with topological rank r satisfies Schreier's formula at rank r if every open normal subgroup has the expected rank transform.
def SatisfiesOpenNormalSchreierFormula
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop :=
∃ r : ℕ,
Generation.topologicalRank G = r ∧ SatisfiesOpenNormalSchreierFormulaAtRank (G := G) rnoncomputable def chosenLeftSchreierGeneratorFamily
(H : OpenSubgroup F) :
(F ⧸ (H : Subgroup F)) × X → ↥(H : Subgroup F) :=
fun p =>
leftSchreierGenerator
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
(ι := ι) p.1 p.2The chosen left Schreier generator family attached to an open subgroup.
@[simp] theorem chosenLeftSchreierGeneratorFamily_apply
(H : OpenSubgroup F) (q : F ⧸ (H : Subgroup F)) (x : X) :
chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) =
leftSchreierGenerator
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
(ι := ι) q xThe left Schreier pair map is evaluated by applying the chosen section and then taking the corresponding generator value.
Show proof
rflProof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□def chosenLeftSchreierGeneratorSet
(H : OpenSubgroup F) : Set ↥(H : Subgroup F) :=
leftSchreierGeneratorSet
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
(ι := ι)The nontrivial chosen left Schreier generators attached to an open subgroup.
def chosenLeftNontrivialSchreierPairs
(H : OpenSubgroup F) : Type u :=
leftNontrivialSchreierPairs
(F := F) H
(openSubgroupLeftSchreierSection (F := F) H)
(openSubgroupLeftSchreierSection_rightInverse (F := F) H)
ιThe nontrivial chosen left Schreier pairs attached to an open subgroup.
noncomputable def chosenLeftNontrivialSchreierPairsToGeneratorSet
(H : OpenSubgroup F) :
chosenLeftNontrivialSchreierPairs (F := F) (ι := ι) H →
↥(chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H) :=
leftNontrivialSchreierPairsToGeneratorSet
(F := F) H
(openSubgroupLeftSchreierSection (F := F) H)
(openSubgroupLeftSchreierSection_rightInverse (F := F) H)
ιThe tautological map from chosen nontrivial left pairs to the chosen generator set.
@[simp] theorem chosenLeftNontrivialSchreierPairsToGeneratorSet_apply
(H : OpenSubgroup F)
(p : chosenLeftNontrivialSchreierPairs (F := F) (ι := ι) H) :
((chosenLeftNontrivialSchreierPairsToGeneratorSet (F := F) (ι := ι) H p :
↥(chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H)) : ↥(H : Subgroup F)) =
chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H p.1Show proof
rflProof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem surjective_chosenLeftNontrivialSchreierPairsToGeneratorSet
(H : OpenSubgroup F) :
Function.Surjective
(chosenLeftNontrivialSchreierPairsToGeneratorSet (F := F) (ι := ι) H)The map from nontrivial left Schreier pairs onto the left Schreier generator set is surjective.
Show proof
by
simpa [chosenLeftNontrivialSchreierPairsToGeneratorSet,
chosenLeftNontrivialSchreierPairs, chosenLeftSchreierGeneratorSet] using
(surjective_leftNontrivialSchreierPairsToGeneratorSet
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
(ι := ι))Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem chosenLeftSchreierGeneratorSet_subset_range
(H : OpenSubgroup F) :
chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H ⊆
Set.range (chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H)Show proof
by
simpa [chosenLeftSchreierGeneratorSet, chosenLeftSchreierGeneratorFamily] using
(leftSchreierGeneratorSet_subset_range
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
(ι := ι))Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem subgroupClosure_chosenLeftSchreierGeneratorSet_eq_closure_range
(H : OpenSubgroup F) :
Subgroup.closure (chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H) =
Subgroup.closure (Set.range
(chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H))Show proof
by
simpa [chosenLeftSchreierGeneratorSet, chosenLeftSchreierGeneratorFamily] using
(subgroupClosure_leftSchreierGeneratorSet_eq_closure_range
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
(ι := ι))Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem topologicallyGenerates_chosenLeftSchreierGeneratorSet_iff
{H : OpenSubgroup F} :
ProCGroups.Generation.TopologicallyGenerates (G := ↥(H : Subgroup F))
(chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H) ↔
ProCGroups.Generation.TopologicallyGenerates (G := ↥(H : Subgroup F))
(Set.range (chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H))The Schreier generator family topologically generates precisely when the corresponding subgroup-generation condition holds.
Show proof
by
simpa [chosenLeftSchreierGeneratorSet, chosenLeftSchreierGeneratorFamily] using
(topologicallyGenerates_leftSchreierGeneratorSet_iff
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
(ι := ι))Proof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. When a quotient map is present, both sides use the same image coset and the same rewritten letter, so the chosen-representative equality descends to the quotient presentation. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem chosenLeftSchreierNextCoset_eq_of_mem
(H : OpenSubgroup F) {q : F ⧸ (H : Subgroup F)} {x : X}
(hx : ι x ∈ (H : Subgroup F)) :
leftSchreierNextCoset (F := F) H (openSubgroupLeftSchreierSection (F := F) H) ι q x =
qThe next left Schreier coset has the stated value under the membership hypothesis.
Show proof
leftSchreierNextCoset_eq_of_mem
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(ι := ι)
(openSubgroupLeftSchreierSection_rightInverse (F := F) H)
hxProof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem chosenLeftSchreierNextCoset_eq_basepoint_of_mul_mem
(H : OpenSubgroup F) {q : F ⧸ (H : Subgroup F)} {x : X}
(hx : openSubgroupLeftSchreierSection (F := F) H q * ι x ∈ (H : Subgroup F)) :
leftSchreierNextCoset (F := F) H (openSubgroupLeftSchreierSection (F := F) H) ι q x =
QuotientGroup.mk (s := (H : Subgroup F)) (1 : F)The next left Schreier coset is the basepoint when the chosen representative times the generator image lies in the subgroup.
Show proof
leftSchreierNextCoset_eq_basepoint_of_mul_mem
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(ι := ι)
hxProof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem chosenLeftSchreierGeneratorFamily_eq_of_mem
(H : OpenSubgroup F) {q : F ⧸ (H : Subgroup F)} {x : X}
(hx : ι x ∈ (H : Subgroup F)) :
chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) = ⟨ι x, hx⟩The left Schreier generator has the displayed value under the subgroup-membership hypothesis.
Show proof
by
simpa [chosenLeftSchreierGeneratorFamily] using
(leftSchreierGenerator_eq_of_mem
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
(ι := ι)
(q := q) (x := x) hx)Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem chosenLeftSchreierGeneratorFamily_eq_one
(H : OpenSubgroup F) {q : F ⧸ (H : Subgroup F)} {x : X}
(hx : ι x = 1) :
chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) = 1The chosen left Schreier generator family evaluates to the identity in the target subgroup presentation.
Show proof
by
exact leftSchreierGenerator_eq_one
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
(ι := ι) (q := q) (x := x) hxProof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. Relator and normal-closure claims follow because rewriting the defining relators gives the subgroup presentation relators, and conjugating by transversal representatives stays inside the generated normal closure. When a quotient map is present, both sides use the same image coset and the same rewritten letter, so the chosen-representative equality descends to the quotient presentation. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem chosenLeftSchreierGeneratorFamily_eq_one_iff
{H : OpenSubgroup F} {q : F ⧸ (H : Subgroup F)} {x : X} :
chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) = 1 ↔
openSubgroupLeftSchreierSection (F := F) H
(leftSchreierNextCoset (F := F) H
(openSubgroupLeftSchreierSection (F := F) H) ι q x) =
openSubgroupLeftSchreierSection (F := F) H q * ι xThe Schreier generator is trivial exactly under the corresponding coset condition.
Show proof
by
simpa [chosenLeftSchreierGeneratorFamily] using
(leftSchreierGenerator_eq_one_iff
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
(ι := ι) (q := q) (x := x))Proof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. When a quotient map is present, both sides use the same image coset and the same rewritten letter, so the chosen-representative equality descends to the quotient presentation. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem chosenLeftSchreierGeneratorFamily_eq_of_mul_mem
(H : OpenSubgroup F) {q : F ⧸ (H : Subgroup F)} {x : X}
(hx : openSubgroupLeftSchreierSection (F := F) H q * ι x ∈ (H : Subgroup F)) :
chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) =
⟨openSubgroupLeftSchreierSection (F := F) H q * ι x, hx⟩The left Schreier generator or next-coset formula is obtained by evaluating the chosen section cocycle.
Show proof
by
simpa [chosenLeftSchreierGeneratorFamily] using
(leftSchreierGenerator_eq_of_mul_mem
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
(ι := ι)
(openSubgroupLeftSchreierSection_one (F := F) H)
(q := q) (x := x) hx)Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem continuous_chosenLeftSchreierNextCoset
(H : OpenSubgroup F)
(hιcont : Continuous ι) :
Continuous (fun p : (F ⧸ (H : Subgroup F)) × X =>
leftSchreierNextCoset (F := F) H (openSubgroupLeftSchreierSection (F := F) H) ι
p.1 p.2)The corresponding Schreier next-coset map is continuous.
Show proof
by
exact continuous_leftSchreierNextCoset
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(ι := ι)
(continuous_openSubgroupLeftSchreierSection (F := F) H)
hιcontProof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. When a quotient map is present, both sides use the same image coset and the same rewritten letter, so the chosen-representative equality descends to the quotient presentation. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem continuous_chosenLeftSchreierGeneratorFamily
(H : OpenSubgroup F)
(hιcont : Continuous ι) :
Continuous (chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H)The corresponding Schreier generator map is continuous.
Show proof
by
simpa [chosenLeftSchreierGeneratorFamily] using
(continuous_leftSchreierGenerator
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
(ι := ι)
(continuous_openSubgroupLeftSchreierSection (F := F) H)
hιcont)Proof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The quotient presentation is generated by the Schreier generators, so equality of rewritten generator images determines the induced homomorphism. The normal-closure argument shows that replacing a word by an equivalent word in the original presentation does not change its rewritten image. This supplies the required presentation-level equality. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem natCard_chosenLeftSchreierGeneratorSet_le
(H : OpenSubgroup F) [CompactSpace F] [Finite X] :
Nat.card (chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H) ≤
Nat.card (F ⧸ (H : Subgroup F)) * Nat.card XShow proof
by
letI : Finite (F ⧸ (H : Subgroup F)) :=
ProCGroups.openSubgroup_finiteQuotient (G := F) H
exact natCard_leftSchreierGeneratorSet_le
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
(ι := ι)Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem natCard_chosenLeftNontrivialSchreierPairs_le
(H : OpenSubgroup F) [CompactSpace F] [Finite X] :
Nat.card (chosenLeftNontrivialSchreierPairs (F := F) (ι := ι) H) ≤
Nat.card (F ⧸ (H : Subgroup F)) * Nat.card XShow proof
by
letI : Finite (F ⧸ (H : Subgroup F)) :=
ProCGroups.openSubgroup_finiteQuotient (G := F) H
simpa [chosenLeftNontrivialSchreierPairs] using
(natCard_leftNontrivialSchreierPairs_le
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
(ι := ι))Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem natCard_chosenLeftSchreierGeneratorSet_le_nontrivialPairs
(H : OpenSubgroup F) [CompactSpace F] [Finite X] :
Nat.card (chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H) ≤
Nat.card (chosenLeftNontrivialSchreierPairs (F := F) (ι := ι) H)Show proof
by
letI : Finite (F ⧸ (H : Subgroup F)) :=
ProCGroups.openSubgroup_finiteQuotient (G := F) H
simpa [chosenLeftSchreierGeneratorSet, chosenLeftNontrivialSchreierPairs] using
(natCard_leftSchreierGeneratorSet_le_nontrivialPairs
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
(ι := ι))Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem natCard_range_chosenLeftSchreierGeneratorFamily_le_rankTransform
[Finite X] {x0 : X} (hx0 : ι x0 = 1)
(H : OpenSubgroup F) [CompactSpace F] :
Nat.card (Set.range (chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H)) ≤
_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F)))Show proof
by
letI : Nonempty X := ⟨x0⟩
letI : Finite (F ⧸ (H : Subgroup F)) :=
ProCGroups.openSubgroup_finiteQuotient (G := F) H
let q0 : F ⧸ (H : Subgroup F) := QuotientGroup.mk (s := (H : Subgroup F)) (1 : F)
let κ' : Option ((F ⧸ (H : Subgroup F)) × {x : X // x ≠ x0}) → ↥(H : Subgroup F)
| none => 1
| some p => chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H (p.1, p.2.1)
have hbase :
∀ q : F ⧸ (H : Subgroup F),
chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H (q, x0) = 1 := by
intro q
simpa [chosenLeftSchreierGeneratorFamily] using
(leftSchreierGenerator_eq_one
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
(ι := ι) (q := q) (x := x0) hx0)
have hrange :
Set.range (chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H) =
Set.range κ' := by
ext y
constructor
· rintro ⟨⟨q, x⟩, rfl⟩
by_cases hx : x = x0
· refine ⟨none, ?_⟩
subst hx
simp only [ne_eq, chosenLeftSchreierGeneratorFamily_apply, hbase q, κ']
· refine ⟨some (q, ⟨x, hx⟩), ?_⟩
simp only [ne_eq, chosenLeftSchreierGeneratorFamily_apply, κ']
· rintro ⟨p, rfl⟩
cases p with
| none =>
exact ⟨(q0, x0), by simp only [hbase q0, ne_eq, chosenLeftSchreierGeneratorFamily_apply, κ']⟩
| some p =>
rcases p with ⟨q, x⟩
exact ⟨(q, x), by simp only [ne_eq, chosenLeftSchreierGeneratorFamily_apply, κ']⟩
have hcardCompl : Nat.card {x : X // x ≠ x0} = Nat.card X - 1 := by
letI : Fintype X := Fintype.ofFinite X
letI : Fintype {x : X // x = x0} := Fintype.ofFinite _
letI : Fintype {x : X // x ≠ x0} := Fintype.ofFinite _
simp only [ne_eq, Nat.card_eq_fintype_card, Fintype.card_subtype_compl, Fintype.card_unique]
have hsucc : Nat.card X = Nat.card {x : X // x ≠ x0} + 1 := by
exact (Nat.sub_eq_iff_eq_add Nat.card_pos).1 hcardCompl.symm
calc
Nat.card (Set.range (chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H)) =
Nat.card (Set.range κ') := by
rw [hrange]
_ ≤ Nat.card (Option ((F ⧸ (H : Subgroup F)) × {x : X // x ≠ x0})) := by
exact Finite.card_range_le κ'
_ = Nat.card ((F ⧸ (H : Subgroup F)) × {x : X // x ≠ x0}) + 1 := by
rw [Finite.card_option]
_ = Nat.card (F ⧸ (H : Subgroup F)) * Nat.card {x : X // x ≠ x0} + 1 := by
rw [Nat.card_prod]
_ = 1 + Nat.card (F ⧸ (H : Subgroup F)) * Nat.card {x : X // x ≠ x0} := by
rw [Nat.add_comm]
_ = _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) := by
rw [hsucc, _root_.ReidemeisterSchreier.Schreier.rankTransform_succ]Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem natCard_chosenLeftSchreierGeneratorSet_le_rankTransform
[Finite X] {x0 : X} (hx0 : ι x0 = 1)
(H : OpenSubgroup F) [CompactSpace F] :
Nat.card (chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H) ≤
_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F)))Show proof
by
let f := chosenLeftSchreierGeneratorFamily (F := F) (ι := ι) H
have hsub : chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H ⊆ Set.range f := by
simpa [chosenLeftSchreierGeneratorSet, f, chosenLeftSchreierGeneratorFamily] using
(leftSchreierGeneratorSet_subset_range
(F := F) (H := H)
(σ := openSubgroupLeftSchreierSection (F := F) H)
(hσ := openSubgroupLeftSchreierSection_rightInverse (F := F) H)
(ι := ι))
letI : Finite (Set.range f) := Set.finite_range f
have hle :
Nat.card (chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H) ≤
Nat.card (Set.range f) := by
exact Nat.card_le_card_of_injective
(fun z : chosenLeftSchreierGeneratorSet (F := F) (ι := ι) H =>
(⟨z.1, hsub z.2⟩ : Set.range f))
(by
intro a b h
apply Subtype.ext
exact congrArg (fun y : Set.range f => (y : ↥(H : Subgroup F))) h)
exact hle.trans
(natCard_range_chosenLeftSchreierGeneratorFamily_le_rankTransform
(F := F) (ι := ι) hx0 H)Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□noncomputable def chosenRightSchreierGeneratorFamily
(H : OpenSubgroup F) :
OpenSubgroupRightQuotient H × X → ↥(H : Subgroup F) :=
fun p =>
rightSchreierGenerator
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι) p.1 p.2The chosen right Schreier generator family attached to an open subgroup.
@[simp] theorem chosenRightSchreierGeneratorFamily_apply
(H : OpenSubgroup F) (q : OpenSubgroupRightQuotient H) (x : X) :
chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) =
rightSchreierGenerator
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι) q xThe right Schreier pair map is evaluated by applying the chosen section and then taking the corresponding generator value.
Show proof
rflProof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□def chosenRightSchreierGeneratorSet
(H : OpenSubgroup F) : Set ↥(H : Subgroup F) :=
rightSchreierGeneratorSet
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι)The nontrivial chosen right Schreier generators attached to an open subgroup.
def chosenRightNontrivialSchreierPairs
(H : OpenSubgroup F) : Type u :=
rightNontrivialSchreierPairs
(F := F) H
(openSubgroupRightCosetSection (F := F) H)
(openSubgroupRightCosetSection_spec (F := F) H)
ιThe nontrivial chosen right Schreier pairs attached to an open subgroup.
noncomputable def chosenRightNontrivialSchreierPairsToGeneratorSet
(H : OpenSubgroup F) :
chosenRightNontrivialSchreierPairs (F := F) (ι := ι) H →
↥(chosenRightSchreierGeneratorSet (F := F) (ι := ι) H) :=
rightNontrivialSchreierPairsToGeneratorSet
(F := F) H
(openSubgroupRightCosetSection (F := F) H)
(openSubgroupRightCosetSection_spec (F := F) H)
ιThe tautological map from chosen nontrivial right pairs to the chosen generator set.
@[simp] theorem chosenRightNontrivialSchreierPairsToGeneratorSet_apply
(H : OpenSubgroup F)
(p : chosenRightNontrivialSchreierPairs (F := F) (ι := ι) H) :
((chosenRightNontrivialSchreierPairsToGeneratorSet (F := F) (ι := ι) H p :
↥(chosenRightSchreierGeneratorSet (F := F) (ι := ι) H)) : ↥(H : Subgroup F)) =
chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H p.1Show proof
rflProof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem surjective_chosenRightNontrivialSchreierPairsToGeneratorSet
(H : OpenSubgroup F) :
Function.Surjective
(chosenRightNontrivialSchreierPairsToGeneratorSet (F := F) (ι := ι) H)The map from nontrivial right Schreier pairs onto the right Schreier generator set is surjective.
Show proof
by
simpa [chosenRightNontrivialSchreierPairsToGeneratorSet,
chosenRightNontrivialSchreierPairs, chosenRightSchreierGeneratorSet] using
(surjective_rightNontrivialSchreierPairsToGeneratorSet
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι))Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem chosenRightSchreierGeneratorSet_subset_range
(H : OpenSubgroup F) :
chosenRightSchreierGeneratorSet (F := F) (ι := ι) H ⊆
Set.range (chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H)Show proof
by
simpa [chosenRightSchreierGeneratorSet, chosenRightSchreierGeneratorFamily] using
(rightSchreierGeneratorSet_subset_range
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι))Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem subgroupClosure_chosenRightSchreierGeneratorSet_eq_closure_range
(H : OpenSubgroup F) :
Subgroup.closure (chosenRightSchreierGeneratorSet (F := F) (ι := ι) H) =
Subgroup.closure (Set.range
(chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H))Show proof
by
simpa [chosenRightSchreierGeneratorSet, chosenRightSchreierGeneratorFamily] using
(subgroupClosure_rightSchreierGeneratorSet_eq_closure_range
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι))Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem topologicallyGenerates_chosenRightSchreierGeneratorSet_iff
{H : OpenSubgroup F} :
ProCGroups.Generation.TopologicallyGenerates (G := ↥(H : Subgroup F))
(chosenRightSchreierGeneratorSet (F := F) (ι := ι) H) ↔
ProCGroups.Generation.TopologicallyGenerates (G := ↥(H : Subgroup F))
(Set.range (chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H))The Schreier generator family topologically generates precisely when the corresponding subgroup-generation condition holds.
Show proof
by
simpa [chosenRightSchreierGeneratorSet, chosenRightSchreierGeneratorFamily] using
(topologicallyGenerates_rightSchreierGeneratorSet_iff
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι))Proof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. When a quotient map is present, both sides use the same image coset and the same rewritten letter, so the chosen-representative equality descends to the quotient presentation. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem chosenRightSchreierNextCoset_basepoint_eq_of_mem
(H : OpenSubgroup F) {x : X}
(hx : ι x ∈ (H : Subgroup F)) :
rightSchreierNextCoset (F := F) H ι (openSubgroupRightCoset H (1 : F)) x =
openSubgroupRightCoset H (1 : F)The next right Schreier coset is the basepoint when the relevant representative-generator product lies in the subgroup.
Show proof
rightSchreierNextCoset_basepoint_eq_of_mem
(F := F) (H := H) (ι := ι) hxProof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem chosenRightSchreierNextCoset_eq_basepoint_of_mul_mem
(H : OpenSubgroup F) {q : OpenSubgroupRightQuotient H} {x : X}
(hx : openSubgroupRightCosetSection (F := F) H q * ι x ∈ (H : Subgroup F)) :
rightSchreierNextCoset (F := F) H ι q x = openSubgroupRightCoset H (1 : F)The next right Schreier coset is the basepoint when the relevant representative-generator product lies in the subgroup.
Show proof
rightSchreierNextCoset_eq_basepoint_of_mul_mem
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι)
hxProof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem chosenRightSchreierGeneratorFamily_eq_one
(H : OpenSubgroup F) {q : OpenSubgroupRightQuotient H} {x : X}
(hx : ι x = 1) :
chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) = 1The chosen right Schreier generator family evaluates to the identity in the target subgroup presentation.
Show proof
by
exact rightSchreierGenerator_eq_one
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι) (q := q) (x := x) hxProof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. Relator and normal-closure claims follow because rewriting the defining relators gives the subgroup presentation relators, and conjugating by transversal representatives stays inside the generated normal closure. When a quotient map is present, both sides use the same image coset and the same rewritten letter, so the chosen-representative equality descends to the quotient presentation. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem chosenRightSchreierGeneratorFamily_eq_one_iff
{H : OpenSubgroup F} {q : OpenSubgroupRightQuotient H} {x : X} :
chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) = 1 ↔
openSubgroupRightCosetSection (F := F) H
(rightSchreierNextCoset (F := F) H ι q x) =
openSubgroupRightCosetSection (F := F) H q * ι xThe Schreier generator is trivial exactly under the corresponding coset condition.
Show proof
by
simpa [chosenRightSchreierGeneratorFamily] using
(rightSchreierGenerator_eq_one_iff_nextCoset
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι) (q := q) (x := x))Proof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. When a quotient map is present, both sides use the same image coset and the same rewritten letter, so the chosen-representative equality descends to the quotient presentation. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem chosenRightSchreierGeneratorFamily_basepoint_eq_of_mem
(H : OpenSubgroup F) {x : X}
(hx : ι x ∈ (H : Subgroup F)) :
chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H
(openSubgroupRightCoset H (1 : F), x) =
⟨ι x, hx⟩The right Schreier generator has the displayed value under the subgroup-membership hypothesis.
Show proof
by
simpa [chosenRightSchreierGeneratorFamily] using
(rightSchreierGenerator_basepoint_eq_of_mem
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι)
(openSubgroupRightCosetSection_one (F := F) H)
(x := x) hx)Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem chosenRightSchreierGeneratorFamily_eq_of_mul_mem
(H : OpenSubgroup F) {q : OpenSubgroupRightQuotient H} {x : X}
(hx : openSubgroupRightCosetSection (F := F) H q * ι x ∈ (H : Subgroup F)) :
chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H (q, x) =
⟨openSubgroupRightCosetSection (F := F) H q * ι x, hx⟩The right Schreier generator or next-coset formula is obtained by evaluating the chosen section cocycle.
Show proof
by
simpa [chosenRightSchreierGeneratorFamily] using
(rightSchreierGenerator_eq_of_mul_mem
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι)
(openSubgroupRightCosetSection_one (F := F) H)
(q := q) (x := x) hx)Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem continuous_chosenRightSchreierNextCoset
(H : OpenSubgroup F)
(hιcont : Continuous ι) :
Continuous (fun p : OpenSubgroupRightQuotient H × X =>
rightSchreierNextCoset (F := F) H ι p.1 p.2)The corresponding Schreier next-coset map is continuous.
Show proof
by
exact continuous_rightSchreierNextCoset
(F := F) (H := H)
(ι := ι)
hιcontProof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. When a quotient map is present, both sides use the same image coset and the same rewritten letter, so the chosen-representative equality descends to the quotient presentation. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem continuous_chosenRightSchreierGeneratorFamily
(H : OpenSubgroup F)
(hιcont : Continuous ι) :
Continuous (chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H)The corresponding Schreier generator map is continuous.
Show proof
by
simpa [chosenRightSchreierGeneratorFamily] using
(continuous_rightSchreierGenerator
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι)
(continuous_openSubgroupRightCosetSection (F := F) H)
hιcont)Proof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The quotient presentation is generated by the Schreier generators, so equality of rewritten generator images determines the induced homomorphism. The normal-closure argument shows that replacing a word by an equivalent word in the original presentation does not change its rewritten image. This supplies the required presentation-level equality. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem natCard_chosenRightSchreierGeneratorSet_le
(H : OpenSubgroup F) [CompactSpace F] [Finite X] :
Nat.card (chosenRightSchreierGeneratorSet (F := F) (ι := ι) H) ≤
Nat.card (OpenSubgroupRightQuotient H) * Nat.card XShow proof
by
exact natCard_rightSchreierGeneratorSet_le
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι)Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem natCard_chosenRightNontrivialSchreierPairs_le
(H : OpenSubgroup F) [CompactSpace F] [Finite X] :
Nat.card (chosenRightNontrivialSchreierPairs (F := F) (ι := ι) H) ≤
Nat.card (OpenSubgroupRightQuotient H) * Nat.card XShow proof
by
letI : Finite (OpenSubgroupRightQuotient H) := finite_openSubgroupRightQuotient (F := F) H
simpa [chosenRightNontrivialSchreierPairs] using
(natCard_rightNontrivialSchreierPairs_le
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι))Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem natCard_chosenRightSchreierGeneratorSet_le_nontrivialPairs
(H : OpenSubgroup F) [CompactSpace F] [Finite X] :
Nat.card (chosenRightSchreierGeneratorSet (F := F) (ι := ι) H) ≤
Nat.card (chosenRightNontrivialSchreierPairs (F := F) (ι := ι) H)Show proof
by
letI : Finite (OpenSubgroupRightQuotient H) := finite_openSubgroupRightQuotient (F := F) H
simpa [chosenRightSchreierGeneratorSet, chosenRightNontrivialSchreierPairs] using
(natCard_rightSchreierGeneratorSet_le_nontrivialPairs
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι))Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem natCard_range_chosenRightSchreierGeneratorFamily_le_rankTransform
[Finite X] {x0 : X} (hx0 : ι x0 = 1)
(H : OpenSubgroup F) [CompactSpace F] :
Nat.card (Set.range (chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H)) ≤
_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (OpenSubgroupRightQuotient H))Show proof
by
letI : Nonempty X := ⟨x0⟩
letI : Finite (OpenSubgroupRightQuotient H) := finite_openSubgroupRightQuotient (F := F) H
let q0 : OpenSubgroupRightQuotient H := openSubgroupRightCoset H (1 : F)
let κ' : Option (OpenSubgroupRightQuotient H × {x : X // x ≠ x0}) → ↥(H : Subgroup F)
| none => 1
| some p => chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H (p.1, p.2.1)
have hbase :
∀ q : OpenSubgroupRightQuotient H,
chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H (q, x0) = 1 := by
intro q
simpa [chosenRightSchreierGeneratorFamily] using
(rightSchreierGenerator_eq_one
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι) (q := q) (x := x0) hx0)
have hrange :
Set.range (chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H) =
Set.range κ' := by
ext y
constructor
· rintro ⟨⟨q, x⟩, rfl⟩
by_cases hx : x = x0
· refine ⟨none, ?_⟩
subst hx
simp only [ne_eq, chosenRightSchreierGeneratorFamily_apply, hbase q, κ']
· refine ⟨some (q, ⟨x, hx⟩), ?_⟩
simp only [ne_eq, chosenRightSchreierGeneratorFamily_apply, κ']
· rintro ⟨p, rfl⟩
cases p with
| none =>
exact ⟨(q0, x0), by simp only [hbase q0, ne_eq, chosenRightSchreierGeneratorFamily_apply, κ']⟩
| some p =>
rcases p with ⟨q, x⟩
exact ⟨(q, x), by simp only [ne_eq, chosenRightSchreierGeneratorFamily_apply, κ']⟩
have hcardCompl : Nat.card {x : X // x ≠ x0} = Nat.card X - 1 := by
letI : Fintype X := Fintype.ofFinite X
letI : Fintype {x : X // x = x0} := Fintype.ofFinite _
letI : Fintype {x : X // x ≠ x0} := Fintype.ofFinite _
simp only [ne_eq, Nat.card_eq_fintype_card, Fintype.card_subtype_compl, Fintype.card_unique]
have hsucc : Nat.card X = Nat.card {x : X // x ≠ x0} + 1 := by
exact (Nat.sub_eq_iff_eq_add Nat.card_pos).1 hcardCompl.symm
calc
Nat.card (Set.range (chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H)) =
Nat.card (Set.range κ') := by
rw [hrange]
_ ≤ Nat.card (Option (OpenSubgroupRightQuotient H × {x : X // x ≠ x0})) := by
exact Finite.card_range_le κ'
_ = Nat.card (OpenSubgroupRightQuotient H × {x : X // x ≠ x0}) + 1 := by
rw [Finite.card_option]
_ = Nat.card (OpenSubgroupRightQuotient H) * Nat.card {x : X // x ≠ x0} + 1 := by
rw [Nat.card_prod]
_ = 1 + Nat.card (OpenSubgroupRightQuotient H) * Nat.card {x : X // x ≠ x0} := by
rw [Nat.add_comm]
_ = _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (OpenSubgroupRightQuotient H)) := by
rw [hsucc, _root_.ReidemeisterSchreier.Schreier.rankTransform_succ]Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□theorem natCard_chosenRightSchreierGeneratorSet_le_rankTransform
[Finite X] {x0 : X} (hx0 : ι x0 = 1)
(H : OpenSubgroup F) [CompactSpace F] :
Nat.card (chosenRightSchreierGeneratorSet (F := F) (ι := ι) H) ≤
_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (OpenSubgroupRightQuotient H))Show proof
by
let f := chosenRightSchreierGeneratorFamily (F := F) (ι := ι) H
have hsub : chosenRightSchreierGeneratorSet (F := F) (ι := ι) H ⊆ Set.range f := by
simpa [chosenRightSchreierGeneratorSet, f, chosenRightSchreierGeneratorFamily] using
(rightSchreierGeneratorSet_subset_range
(F := F) (H := H)
(τ := openSubgroupRightCosetSection (F := F) H)
(hτ := openSubgroupRightCosetSection_spec (F := F) H)
(ι := ι))
letI : Finite (Set.range f) := Set.finite_range f
have hle :
Nat.card (chosenRightSchreierGeneratorSet (F := F) (ι := ι) H) ≤
Nat.card (Set.range f) := by
exact Nat.card_le_card_of_injective
(fun z : chosenRightSchreierGeneratorSet (F := F) (ι := ι) H =>
(⟨z.1, hsub z.2⟩ : Set.range f))
(by
intro a b h
apply Subtype.ext
exact congrArg (fun y : Set.range f => (y : ↥(H : Subgroup F))) h)
exact hle.trans
(natCard_range_chosenRightSchreierGeneratorFamily_le_rankTransform
(F := F) (ι := ι) hx0 H)Proof. Unfold the Schreier section, next-coset operation, and cocycle. Generator formulas are obtained by comparing the chosen representative before and after multiplying by the selected generator. The finite generator-set and cardinality bounds follow by viewing generator values as images of the finite set of nontrivial pairs; closure and generation statements then follow from this image description.
□