ReidemeisterSchreier.Profinite.OpenSubgroups.GeneratingFamilies
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.
import
structure FreeProCBasis
(ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] where
index : Type u
inclusion : index → G
isFree : IsFreeProCGroupOnConvergingSet (ProC := ProC) index G inclusionA free pro-\(C\) basis on a fixed carrier.
instance instCoeFunFreeProCBasis : CoeFun (FreeProCBasis ProC G) (fun basis => basis.index → G) where
coe basis := basis.inclusionA free pro-\(C\) basis is coerced to its underlying family of basis elements.
@[simp] theorem inclusion_eq_coe (basis : FreeProCBasis ProC G) :
basis.inclusion = (basis : basis.index → G)The profinite Schreier basis has the stated cardinality or inclusion property.
Show proof
rflProof. 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. Finiteness is supplied by the finite quotient or finite list of Schreier generators used by the construction. 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.
□def cardinal (basis : FreeProCBasis ProC G) : Cardinal :=
Cardinal.mk basis.indexThe profinite Schreier basis has the stated cardinality or inclusion property.
def toGeneratingFamily (basis : FreeProCBasis ProC G) :
TopologicalGeneratingFamily G where
index := basis.index
toFun := basis
convergesToOne := basis.isFree.convergesToOne
generates := basis.isFree.generates_rangeA free pro-\(C\) basis forgets to a topological generating family.
def toData (basis : FreeProCBasis ProC G) :
FreeProCGroupOnConvergingSetData (ProC := ProC) where
basis := basis.index
carrier := G
instGroup := inferInstance
instTopologicalSpace := inferInstance
instIsTopologicalGroup := inferInstance
inclusion := basis.inclusion
isFree := basis.isFreeForget the fixed-carrier basis to the existing carrier-and-basis data structure.
def ofData (data : FreeProCGroupOnConvergingSetData (ProC := ProC)) :
FreeProCBasis ProC data.carrier where
index := data.basis
inclusion := data.inclusion
isFree := data.isFreeTurn existing carrier-and-basis data plus an equivalence to the target into a basis model.
structure FreeProCBasisModel
(ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] where
carrier : Type u
instGroup : Group carrier
instTopologicalSpace : TopologicalSpace carrier
instIsTopologicalGroup : IsTopologicalGroup carrier
basis : FreeProCBasis ProC carrier
equiv : carrier ≃ₜ* GA free pro-\(C\) basis model for a target group, up to continuous multiplicative equivalence.
def basisCardinal (model : FreeProCBasisModel ProC G) : Cardinal :=
model.basis.cardinalThe cardinality of the modeled free pro-\(C\) basis.
def ofData (data : FreeProCGroupOnConvergingSetData (ProC := ProC)) (e : data.carrier ≃ₜ* G) :
FreeProCBasisModel ProC G where
carrier := data.carrier
instGroup := data.instGroup
instTopologicalSpace := data.instTopologicalSpace
instIsTopologicalGroup := data.instIsTopologicalGroup
basis := FreeProCBasis.ofData data
equiv := eTurn existing carrier-and-basis data plus an equivalence to the target into a basis model.
theorem exists_generatingFamily_openSubnormalSubgroup_of_melnikovFormation_finiteRank
(C : ProCGroups.FiniteGroupClass.{u})
{X : Type u} [Finite X]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
(hF : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
(H : OpenSubgroup F) :
∃ family : TopologicalGeneratingFamily ↥(H : Subgroup F),
family.cardinal ≤
(_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) :
Cardinal)The generating-family form of the finite-rank open-subgroup result with the Schreier rank bound.
Show proof
by
classical
rcases exists_basis_openSubnormalSubgroup_of_melnikovFormation_finiteRank
(C := C) hF H with
⟨Y, κ, hκ, hκcard⟩
have hYfinite : Finite Y :=
(Cardinal.lt_aleph0_iff_finite (α := Y)).mp <|
lt_of_le_of_lt hκcard
(Cardinal.natCast_lt_aleph0
(n := _root_.ReidemeisterSchreier.Schreier.rankTransform
(Nat.card X) (Nat.card (F ⧸ (H : Subgroup F)))))
letI : Finite Y := hYfinite
let family : TopologicalGeneratingFamily ↥(H : Subgroup F) :=
{ index := Y
toFun := κ
convergesToOne := FamilyConvergesToOne.of_finite_domain (G := ↥(H : Subgroup F)) κ
generates := hκ.1 }
exact ⟨family, by simpa [TopologicalGeneratingFamily.cardinal, family] using hκcard⟩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. Finiteness is supplied by the finite quotient or finite list of Schreier generators used by the construction. 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 exists_freeProCBasisModel_openSubgroup_of_extensionClosed_cardinalRank
(C : ProCGroups.FiniteGroupClass.{u})
(hBridge :
PointedToConvergingSetBasisBridge (ProCGroups.ProC.finiteGroupClassProCPredicate C))
(hVar : ProCGroups.FiniteGroupClass.Variety C)
(hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
(hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
(hcyc :
∃ (A : Type u) (_ : Group A) (_ : Finite A),
C A ∧ IsCyclic A ∧ Nontrivial A)
{X : Type u}
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
[DiscreteTopology (Set.range ι)]
(hF : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
(H : OpenSubgroup F) :
∃ model : FreeProCBasisModel
(ProCGroups.ProC.finiteGroupClassProCPredicate C) ↥(H : Subgroup F),
model.basisCardinal =
schreierRankTransformCardinal (Cardinal.mk X)
(Nat.card (F ⧸ (H : Subgroup F)))Cardinal-rank extension-closed basis theorem, with the conclusion explicitly packaged as a free pro-\(C\) basis model rather than only a generating family.
Show proof
by
rcases exists_basis_openSubgroup_of_extensionClosed_cardinalRank
(C := C) hBridge hVar hIso hExt hcyc hF H with
⟨data, ⟨e⟩, hcard⟩
let model : FreeProCBasisModel
(ProCGroups.ProC.finiteGroupClassProCPredicate C) ↥(H : Subgroup F) :=
FreeProCBasisModel.ofData data e
refine ⟨model, ?_⟩
simpa [model, FreeProCBasisModel.basisCardinal, FreeProCBasisModel.ofData,
FreeProCBasis.cardinal, FreeProCBasis.ofData] using hcardProof. 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. Finiteness is supplied by the finite quotient or finite list of Schreier generators used by the construction. 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 exists_freeProCBasisModel_openSubgroup_of_cardinalRank_of_schreierBasisHypotheses
(C : ProCGroups.FiniteGroupClass.{u})
(hC : SchreierBasisCardinalRankHypotheses C)
{X : Type u}
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
[DiscreteTopology (Set.range ι)]
(hF : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
(H : OpenSubgroup F) :
∃ model : FreeProCBasisModel
(ProCGroups.ProC.finiteGroupClassProCPredicate C) ↥(H : Subgroup F),
model.basisCardinal =
schreierRankTransformCardinal (Cardinal.mk X)
(Nat.card (F ⧸ (H : Subgroup F)))Bundled-hypothesis cardinal-rank basis theorem, with a basis-model conclusion.
Show proof
exists_freeProCBasisModel_openSubgroup_of_extensionClosed_cardinalRank
(C := C) hC.bridge hC.variety hC.isomClosed hC.extensionClosed
hC.hasNontrivialCyclic hF HProof. 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. Finiteness is supplied by the finite quotient or finite list of Schreier generators used by the construction. 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 exists_freeProCBasisModel_openSubgroup_of_melnikovRank
(C : ProCGroups.FiniteGroupClass.{u})
(hBridge :
PointedToConvergingSetBasisBridge (ProCGroups.ProC.finiteGroupClassProCPredicate C))
(hC : ProCGroups.FiniteGroupClass.MelnikovFormation C)
(hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
(hcyc :
∃ (A : Type u) (_ : Group A) (_ : Finite A),
C A ∧ IsCyclic A ∧ Nontrivial A)
{X : Type u}
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
[DiscreteTopology (Set.range ι)]
(hF : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
(H : OpenSubgroup F) :
∃ model : FreeProCBasisModel
(ProCGroups.ProC.finiteGroupClassProCPredicate C) ↥(H : Subgroup F),
model.basisCardinal =
schreierRankTransformCardinal (Cardinal.mk X)
(Nat.card (F ⧸ (H : Subgroup F)))Cardinal-rank Melnikov-formation variant, with a basis-model conclusion.
Show proof
by
rcases exists_basis_openSubgroup_of_melnikovFormation_cardinalRank_of_subgroupClosed
(C := C) hBridge hC hSub hcyc hF H with
⟨data, ⟨e⟩, hcard⟩
let model : FreeProCBasisModel
(ProCGroups.ProC.finiteGroupClassProCPredicate C) ↥(H : Subgroup F) :=
FreeProCBasisModel.ofData data e
refine ⟨model, ?_⟩
simpa [model, FreeProCBasisModel.basisCardinal, FreeProCBasisModel.ofData,
FreeProCBasis.cardinal, FreeProCBasis.ofData] using hcardProof. 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. Finiteness is supplied by the finite quotient or finite list of Schreier generators used by the construction. 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 exists_freeProCBasisModel_openNormalSubgroup_of_melnikovFormation_cardinalRank
(C : ProCGroups.FiniteGroupClass.{u})
(hBridge :
PointedToConvergingSetBasisBridge (ProCGroups.ProC.finiteGroupClassProCPredicate C))
(hC : ProCGroups.FiniteGroupClass.MelnikovFormation C)
(hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
(hcyc :
∃ (A : Type u) (_ : Group A) (_ : Finite A),
C A ∧ IsCyclic A ∧ Nontrivial A)
{X : Type u}
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
[DiscreteTopology (Set.range ι)]
(hF : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
(H : OpenSubgroup F) :
∃ model : FreeProCBasisModel
(ProCGroups.ProC.finiteGroupClassProCPredicate C) ↥(H : Subgroup F),
model.basisCardinal =
schreierRankTransformCardinal (Cardinal.mk X)
(Nat.card (F ⧸ (H : Subgroup F)))Cardinal-rank Melnikov-formation open-subgroup variant, with a basis-model conclusion.
Show proof
by
rcases exists_basis_openNormalSubgroup_of_melnikovFormation_cardinalRank
(C := C) hBridge hC hSub hcyc hF H with
⟨data, ⟨e⟩, hcard⟩
let model : FreeProCBasisModel
(ProCGroups.ProC.finiteGroupClassProCPredicate C) ↥(H : Subgroup F) :=
FreeProCBasisModel.ofData data e
refine ⟨model, ?_⟩
simpa [model, FreeProCBasisModel.basisCardinal, FreeProCBasisModel.ofData,
FreeProCBasis.cardinal, FreeProCBasis.ofData] using hcardProof. 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. Finiteness is supplied by the finite quotient or finite list of Schreier generators used by the construction. 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.
□