import
structure SchreierBasisCardinalRankHypotheses
(C : ProCGroups.FiniteGroupClass.{u}) : Prop where
bridge : PointedToConvergingSetBasisBridge
(ProCGroups.ProC.finiteGroupClassProCPredicate C)
variety : ProCGroups.FiniteGroupClass.Variety C
isomClosed : ProCGroups.FiniteGroupClass.IsomClosed C
extensionClosed : ProCGroups.FiniteGroupClass.ExtensionClosed C
hasNontrivialCyclic :
∃ (A : Type u) (_ : Group A) (_ : Finite A),
C A ∧ IsCyclic A ∧ Nontrivial AHypotheses used by the cardinal-rank Schreier basis theorem. The bridge is only needed in the infinite-rank branch, but bundling it here gives a single public theorem whose conclusion uses schreierRankTransformCardinal.
theorem exists_basis_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) :
∃ Fdata : FreeProCGroupOnConvergingSetData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧
Cardinal.mk Fdata.basis =
schreierRankTransformCardinal (Cardinal.mk X)
(Nat.card (F ⧸ (H : Subgroup F)))Show proof
by
classical
by_cases hXfin : Finite X
· letI : Finite X := hXfin
rcases exists_basis_openSubgroup_of_extensionClosed_finiteRank
(C := C) hVar hIso hExt hcyc hF H with
⟨Fdata, hFdataEquiv, hFdataCard⟩
refine ⟨Fdata, hFdataEquiv, ?_⟩
calc
Cardinal.mk Fdata.basis =
(_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X)
(Nat.card (F ⧸ (H : Subgroup F))) : Cardinal) := hFdataCard
_ = schreierRankTransformCardinal (Cardinal.mk X)
(Nat.card (F ⧸ (H : Subgroup F))) := by
exact (schreierRankTransformCardinal_mk_finite X
(Nat.card (F ⧸ (H : Subgroup F)))).symm
· haveI : Infinite X := not_finite_iff_infinite.1 hXfin
rcases exists_basis_openSubgroup_of_extensionClosed_infiniteRank
(C := C) hBridge hVar hIso hExt hcyc hF H with
⟨Fdata, hFdataEquiv, hFdataCard⟩
refine ⟨Fdata, hFdataEquiv, ?_⟩
calc
Cardinal.mk Fdata.basis = Cardinal.mk X := hFdataCard
_ = schreierRankTransformCardinal (Cardinal.mk X)
(Nat.card (F ⧸ (H : Subgroup F))) := by
exact (schreierRankTransformCardinal_mk_infinite X
(Nat.card (F ⧸ (H : Subgroup F)))).symmProof. 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_basis_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) :
∃ Fdata : FreeProCGroupOnConvergingSetData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧
Cardinal.mk Fdata.basis =
schreierRankTransformCardinal (Cardinal.mk X)
(Nat.card (F ⧸ (H : Subgroup F)))The cardinal-rank Schreier basis result using the bundled cardinal-rank hypotheses.
Show proof
exists_basis_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_basis_openSubgroup_of_melnikovFormation_cardinalRank_of_subgroupClosed
(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) :
∃ Fdata : FreeProCGroupOnConvergingSetData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧
Cardinal.mk Fdata.basis =
schreierRankTransformCardinal (Cardinal.mk X)
(Nat.card (F ⧸ (H : Subgroup F)))Cardinal-rank Melnikov-formation variant with explicit subgroup closure.
Show proof
by
classical
by_cases hXfin : Finite X
· letI : Finite X := hXfin
rcases exists_basis_openSubgroup_of_melnikovFormation_finiteRank_of_subgroupClosed
(C := C) hC hSub hcyc hF H with
⟨Fdata, hFdataEquiv, hFdataCard⟩
refine ⟨Fdata, hFdataEquiv, ?_⟩
calc
Cardinal.mk Fdata.basis =
(_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X)
(Nat.card (F ⧸ (H : Subgroup F))) : Cardinal) := hFdataCard
_ = schreierRankTransformCardinal (Cardinal.mk X)
(Nat.card (F ⧸ (H : Subgroup F))) := by
exact (schreierRankTransformCardinal_mk_finite X
(Nat.card (F ⧸ (H : Subgroup F)))).symm
· haveI : Infinite X := not_finite_iff_infinite.1 hXfin
rcases exists_basis_openSubgroup_of_melnikovFormation_infiniteRank_of_subgroupClosed
(C := C) hBridge hC hSub hcyc hF H with
⟨Fdata, hFdataEquiv, hFdataCard⟩
refine ⟨Fdata, hFdataEquiv, ?_⟩
calc
Cardinal.mk Fdata.basis = Cardinal.mk X := hFdataCard
_ = schreierRankTransformCardinal (Cardinal.mk X)
(Nat.card (F ⧸ (H : Subgroup F))) := by
exact (schreierRankTransformCardinal_mk_infinite X
(Nat.card (F ⧸ (H : Subgroup F)))).symmProof. 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_basis_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) :
∃ Fdata : FreeProCGroupOnConvergingSetData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧
Cardinal.mk Fdata.basis =
schreierRankTransformCardinal (Cardinal.mk X)
(Nat.card (F ⧸ (H : Subgroup F)))Cardinal-rank Melnikov formation case of the open-normal-subgroup Schreier basis theorem.
Show proof
by
classical
by_cases hXfin : Finite X
· letI : Finite X := hXfin
rcases exists_basis_openNormalSubgroup_of_melnikovFormation_finiteRank
(C := C) hC hSub hcyc hF H with
⟨Fdata, hFdataEquiv, hFdataCard⟩
refine ⟨Fdata, hFdataEquiv, ?_⟩
calc
Cardinal.mk Fdata.basis =
(_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X)
(Nat.card (F ⧸ (H : Subgroup F))) : Cardinal) := hFdataCard
_ = schreierRankTransformCardinal (Cardinal.mk X)
(Nat.card (F ⧸ (H : Subgroup F))) := by
exact (schreierRankTransformCardinal_mk_finite X
(Nat.card (F ⧸ (H : Subgroup F)))).symm
· haveI : Infinite X := not_finite_iff_infinite.1 hXfin
rcases exists_basis_openNormalSubgroup_of_melnikovFormation_infiniteRank
(C := C) hBridge hC hSub hcyc hF H with
⟨Fdata, hFdataEquiv, hFdataCard⟩
refine ⟨Fdata, hFdataEquiv, ?_⟩
calc
Cardinal.mk Fdata.basis = Cardinal.mk X := hFdataCard
_ = schreierRankTransformCardinal (Cardinal.mk X)
(Nat.card (F ⧸ (H : Subgroup F))) := by
exact (schreierRankTransformCardinal_mk_infinite X
(Nat.card (F ⧸ (H : Subgroup F)))).symmProof. 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. 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 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.
□