ReidemeisterSchreier.Profinite.OpenSubgroups.MinimalPower
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.
theorem exists_compactPointedBasis_openSubgroup_of_minGeneratorPower
(C : ProCGroups.FiniteGroupClass.{u})
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
(hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
(hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
(hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
{X : Type u}
[TopologicalSpace X] [DiscreteTopology X]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
(hF : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
(H : OpenSubgroup F) (x : X) {N : ℕ}
(hN : 0 < N)
(hpow : (ι x) ^ N ∈ (H : Subgroup F))
(hmin : ∀ m : ℕ, 0 < m → m < N → (ι x) ^ m ∉ (H : Subgroup F)) :
∃ κ : OpenSubgroupRightQuotient H × OnePoint X → ↥(H : Subgroup F),
Continuous κ ∧
(∀ q : OpenSubgroupRightQuotient H, κ (q, OnePoint.infty) = 1) ∧
κ (openSubgroupRightCoset H (1 : F), OnePoint.infty) = 1 ∧
(⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) ∈ Set.range κ ∧
IsCompact (Set.range κ) ∧
IsClosed (Set.range κ) ∧
IsPointedFreeProCGroupOn
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
(Set.range κ)
⟨κ (openSubgroupRightCoset H (1 : F), OnePoint.infty),
⟨(openSubgroupRightCoset H (1 : F), OnePoint.infty), rfl⟩⟩
↥(H : Subgroup F) Subtype.valThis is the pointed profinite Reidemeister--Schreier theorem over a converging-set basis, with a prescribed minimal generator power landing in the open subgroup.
Show proof
by
classical
let iInf : OnePoint X → F := fun z => z.elim 1 ι
have hιTendsto : Filter.Tendsto ι Filter.cofinite (𝓝 (1 : F)) := by
letI : CompactSpace F := IsProCGroup.compactSpace hF.isProC
letI : T2Space F := IsProCGroup.t2Space hF.isProC
letI : TotallyDisconnectedSpace F := IsProCGroup.totallyDisconnectedSpace hF.isProC
rw [Filter.tendsto_def]
intro s hs
rcases mem_nhds_iff.mp hs with ⟨W, hWs, hWopen, h1W⟩
rcases ProCGroups.ProC.exists_openNormalSubgroup_sub_open_nhds_of_one
(G := F) hWopen h1W with
⟨U, hUW⟩
have hfinite : {x : X | ι x ∉ (U : Set F)}.Finite :=
hF.convergesToOne U.toOpenSubgroup
have hcof : ∀ᶠ x : X in Filter.cofinite, ι x ∈ (U : Set F) :=
Filter.eventually_cofinite.2 hfinite
exact hcof.mono fun x hx => hWs (hUW hx)
have hPointed :
IsPointedFreeProCGroupOn
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
(OnePoint X) OnePoint.infty F iInf := by
refine ⟨hF.isProC, ?_, by simp only [OnePoint.elim_infty, iInf], ?_, ?_⟩
· rw [OnePoint.continuous_iff_from_discrete]
simpa [iInf] using hιTendsto
· have hsub : Set.range ι ⊆ Set.range iInf := by
rintro y ⟨x, rfl⟩
exact ⟨(x : OnePoint X), rfl⟩
exact Generation.topologicallyGenerates_mono (G := F) hF.generates_range hsub
· intro G _ _ _ hG φ hφ hφ0 hgenφ
let ψ : X → G := fun x => φ x
have hψTendsto : Filter.Tendsto ψ Filter.cofinite (𝓝 (1 : G)) := by
have hraw := (OnePoint.continuous_iff_from_discrete (f := φ)).1 hφ
simpa [ψ, hφ0] using hraw
have hψconv : FamilyConvergesToOne (G := G) ψ := by
intro U
exact Filter.eventually_cofinite.mp <|
hψTendsto (U.isOpen'.mem_nhds U.one_mem')
have hφrange : Set.range φ = Set.range ψ ∪ ({1} : Set G) := by
ext z
constructor
· rintro ⟨x, rfl⟩
refine OnePoint.rec ?_ ?_ x
· right
simpa [iInf] using hφ0
· intro y
left
exact ⟨y, rfl⟩
· intro hz
rcases hz with hz | hz
· rcases hz with ⟨y, rfl⟩
exact ⟨(y : OnePoint X), rfl⟩
· exact ⟨OnePoint.infty, hφ0.trans hz.symm⟩
have hψgen : Generation.TopologicallyGenerates (G := G) (Set.range ψ) := by
have hgenφ' :
Generation.TopologicallyGenerates (G := G) (Set.range ψ ∪ ({1} : Set G)) := by
simpa [hφrange] using hgenφ
exact (Generation.topologicallyGenerates_union_one_iff (G := G) (X := Set.range ψ)).1
hgenφ'
rcases hF.existsUnique_lift hG ψ hψconv hψgen with ⟨f, hf, huniq⟩
refine ⟨f, ⟨hf.1, ?_⟩, ?_⟩
· intro z
refine OnePoint.rec ?_ ?_ z
· calc
f (iInf OnePoint.infty) = f 1 := rfl
_ = 1 := map_one f
_ = φ OnePoint.infty := hφ0.symm
· intro y
exact hf.2 y
· intro g hg
apply huniq g
refine ⟨hg.1, ?_⟩
intro y
simpa [iInf, ψ] using hg.2 (y : OnePoint X)
let x' : OnePoint X := x
have hpow' : (iInf x') ^ N ∈ (H : Subgroup F) := by
simpa [iInf, x'] using hpow
have hmin' : ∀ m : ℕ, 0 < m → m < N → (iInf x') ^ m ∉ (H : Subgroup F) := by
intro m hm hlt
simpa [iInf, x'] using hmin m hm hlt
exact
exists_pointedFreeRightSchreierGeneratorFamily_of_openSubgroup_of_minimalGeneratorPower
(C := C) hForm hSub hIso hQuot hExt hPointed H x' hN hpow' hmin'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. 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. 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 exists_finiteConvergingSetBasis_openSubgroup_of_minimalGeneratorPower
{C : ProCGroups.FiniteGroupClass.{u}}
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
(hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
(hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
(hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
{X : Type u} [Finite X]
{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) (x : X) {N : ℕ}
(hN : 0 < N)
(hpow : (ι x) ^ N ∈ (H : Subgroup F))
(hpow_ne : (ι x) ^ N ≠ 1)
(hmin : ∀ m : ℕ, 0 < m → m < N → (ι x) ^ m ∉ (H : Subgroup F)) :
∃ Fdata : FreeProCGroupOnConvergingSetData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
∃ e : Fdata.carrier ≃ₜ* ↥(H : Subgroup F),
(⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) ∈
Set.range (e ∘ Fdata.inclusion) ∧
Finite Fdata.basisFinite-rank pointed control over a converging-set free pro-\(C\) group: if \(x^N\) is the first positive power of a basis element landing in \(H\), and this power is nontrivial, the finite converging-set basis model for \(H\) can be chosen so that \(x^N\) lies in the basis image.
Show proof
by
classical
letI : CompactSpace F := IsProCGroup.compactSpace hF.isProC
letI : T2Space F := IsProCGroup.t2Space hF.isProC
letI : TopologicalSpace X := ⊥
letI : DiscreteTopology X := ⟨rfl⟩
letI : Fintype X := Fintype.ofFinite X
rcases
exists_compactPointedBasis_openSubgroup_of_minGeneratorPower
C hForm hSub hIso hQuot hExt hF H x hN hpow hmin with
⟨κ, _hκcont, _hκbase, hκone, hxpowRange, _hκcompact, _hκclosed, hκfree⟩
letI : Finite (OpenSubgroupRightQuotient H) :=
finite_openSubgroupRightQuotient (F := F) H
letI : Finite (OnePoint X) := Finite.of_fintype (OnePoint X)
letI : Finite (Set.range κ) := (Set.finite_range κ).to_subtype
let x0 : Set.range κ :=
⟨κ (openSubgroupRightCoset H (1 : F), OnePoint.infty),
⟨(openSubgroupRightCoset H (1 : F), OnePoint.infty), rfl⟩⟩
letI : DiscreteTopology (Set.range κ) :=
DiscreteTopology.of_finite_of_isClosed_singleton fun _ => isClosed_singleton
let B : Type u := {y : Set.range κ // y ≠ x0}
let μ : B → ↥(H : Subgroup F) := fun y => y.1.1
have hμfree :
IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) B ↥(H : Subgroup F) μ := by
simpa [B, μ, x0] using
freeOnFinitePointedDiscreteSpace_has_convergingSetBasis
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) hκfree
let Fdata : FreeProCGroupOnConvergingSetData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) :=
{ basis := B
carrier := ↥(H : Subgroup F)
instGroup := inferInstance
instTopologicalSpace := inferInstance
instIsTopologicalGroup := inferInstance
inclusion := μ
isFree := hμfree }
let ypow : Set.range κ := ⟨⟨(ι x) ^ N, hpow⟩, hxpowRange⟩
have hypow_ne_x0 : ypow ≠ x0 := by
intro hEq
apply hpow_ne
have hval : (ypow : ↥(H : Subgroup F)) = (x0 : ↥(H : Subgroup F)) :=
congrArg Subtype.val hEq
have hx0val : (x0 : ↥(H : Subgroup F)) = 1 := by
simpa [x0] using hκone
simpa [ypow] using hval.trans hx0val
let bpow : B := ⟨ypow, hypow_ne_x0⟩
have hbpow : μ bpow = (⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) := rfl
refine ⟨Fdata, ContinuousMulEquiv.refl _, ?_, ?_⟩
· refine ⟨bpow, ?_⟩
simpa [Fdata, μ] using hbpow
· dsimp [Fdata, B]
infer_instanceProof. 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. 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. 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 exists_basis_openSubgroup_of_extensionClosed_finiteRank_of_minimalGeneratorPower
(C : ProCGroups.FiniteGroupClass.{u})
(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} [Finite X]
{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) (x : X) {N : ℕ}
(hN : 0 < N)
(hpow : (ι x) ^ N ∈ (H : Subgroup F))
(hpow_ne : (ι x) ^ N ≠ 1)
(hmin : ∀ m : ℕ, 0 < m → m < N → (ι x) ^ m ∉ (H : Subgroup F)) :
∃ Fdata : FreeProCGroupOnConvergingSetData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
∃ e : Fdata.carrier ≃ₜ* ↥(H : Subgroup F),
(⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) ∈
Set.range (e ∘ Fdata.inclusion) ∧
Cardinal.mk Fdata.basis =
(_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) :
Cardinal)Show proof
by
classical
rcases hVar.closureBundle_of_isomClosed_extensionClosed hIso hExt with
⟨hForm, hSub, hIso', hQuot, hExt'⟩
rcases
exists_finiteConvergingSetBasis_openSubgroup_of_minimalGeneratorPower
(C := C) hForm hSub hIso' hQuot hExt' hF H x hN hpow hpow_ne hmin with
⟨Fdata, eData, hxrange, hFin⟩
letI : Finite Fdata.basis := hFin
rcases exists_basis_openSubgroup_of_extensionClosed_finiteRank
(C := C) hVar hIso hExt hcyc hF H with
⟨Fexact, hFexactEquiv, hExactCard⟩
have hFexactLt : Cardinal.mk Fexact.basis < Cardinal.aleph0 := by
calc
Cardinal.mk Fexact.basis =
(_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) :
Cardinal) := hExactCard
_ < Cardinal.aleph0 := Cardinal.natCast_lt_aleph0
letI : Finite Fexact.basis := Cardinal.lt_aleph0_iff_finite.mp hFexactLt
have hExactBasis :
Cardinal.mk Fexact.basis = Generation.topologicalRank Fexact.carrier :=
basisCard_eq_topologicalRank_of_finiteBasis C hQuot hcyc Fexact
have hDataBasis :
Cardinal.mk Fdata.basis = Generation.topologicalRank Fdata.carrier :=
basisCard_eq_topologicalRank_of_finiteBasis C hQuot hcyc Fdata
rcases hFexactEquiv with ⟨eExact⟩
have hExactProf : ProCGroups.IsProfiniteGroup Fexact.carrier :=
ProCGroups.ProC.isProfiniteGroup_of_finiteGroupClassProCPredicate C Fexact.isFree.isProC
have hDataProf : ProCGroups.IsProfiniteGroup Fdata.carrier :=
ProCGroups.ProC.isProfiniteGroup_of_finiteGroupClassProCPredicate C Fdata.isFree.isProC
have hRankEq :
Generation.topologicalRank Fexact.carrier =
Generation.topologicalRank Fdata.carrier := by
exact Generation.topologicalRank_eq_of_continuousMulEquiv
hExactProf hDataProf (eExact.trans eData.symm)
have hCard :
Cardinal.mk Fdata.basis =
(_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) :
Cardinal) := by
calc
Cardinal.mk Fdata.basis = Generation.topologicalRank Fdata.carrier := hDataBasis
_ = Generation.topologicalRank Fexact.carrier := hRankEq.symm
_ = Cardinal.mk Fexact.basis := hExactBasis.symm
_ = (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))) :
Cardinal) := hExactCard
exact ⟨Fdata, eData, hxrange, hCard⟩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_finiteConvergingSetBasis_comap_openSubgroup_of_minimalGeneratorPower
{C : ProCGroups.FiniteGroupClass.{u}}
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
(hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
(hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
(hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
{X : Type u} [Finite X]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
[DiscreteTopology (Set.range ι)]
(hF : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
{Q : Type u} [Group Q] [TopologicalSpace Q]
(π : F →* Q) (hπcont : Continuous π)
(H : OpenSubgroup Q) (x : X) {N : ℕ}
(hN : 0 < N)
(hpow : (ι x) ^ N ∈ ((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F))
(hpow_ne : (ι x) ^ N ≠ 1)
(hmin :
∀ m : ℕ, 0 < m → m < N →
(ι x) ^ m ∉ ((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F)) :
∃ Fdata : FreeProCGroupOnConvergingSetData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
∃ e : Fdata.carrier ≃ₜ*
↥((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F),
(⟨(ι x) ^ N, hpow⟩ :
↥((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F)) ∈
Set.range (e ∘ Fdata.inclusion) ∧
Finite Fdata.basisPreimage form of the finite pointed-control theorem.
Show proof
by
exact
exists_finiteConvergingSetBasis_openSubgroup_of_minimalGeneratorPower
(C := C) hForm hSub hIso hQuot hExt hF
(OpenSubgroup.comap π hπcont H) x hN hpow hpow_ne hminProof. 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. 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. 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 exists_basis_comap_openSubgroup_of_extensionClosed_finiteRank_of_minimalGeneratorPower
(C : ProCGroups.FiniteGroupClass.{u})
(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} [Finite X]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
[DiscreteTopology (Set.range ι)]
(hF : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
{Q : Type u} [Group Q] [TopologicalSpace Q]
(π : F →* Q) (hπcont : Continuous π) (hπsurj : Function.Surjective π)
(H : OpenSubgroup Q) (x : X) {N : ℕ}
(hN : 0 < N)
(hpow : (ι x) ^ N ∈ ((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F))
(hpow_ne : (ι x) ^ N ≠ 1)
(hmin :
∀ m : ℕ, 0 < m → m < N →
(ι x) ^ m ∉ ((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F)) :
∃ Fdata : FreeProCGroupOnConvergingSetData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
∃ e : Fdata.carrier ≃ₜ*
↥((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F),
(⟨(ι x) ^ N, hpow⟩ :
↥((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F)) ∈
Set.range (e ∘ Fdata.inclusion) ∧
Cardinal.mk Fdata.basis =
(_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (Q ⧸ (H : Subgroup Q))) :
Cardinal)Preimage form of the finite-rank pointed Reidemeister--Schreier theorem. This is the version for \(\pi^{-1}(H)\), with the Schreier rank transform expressed using the quotient-side cardinality of \(Q/H\).
Show proof
by
classical
rcases exists_basis_openSubgroup_of_extensionClosed_finiteRank_of_minimalGeneratorPower
(C := C) hVar hIso hExt hcyc hF
(OpenSubgroup.comap π hπcont H) x hN hpow hpow_ne hmin with
⟨Fdata, e, hxNrange, hCard⟩
have hIndex :
Nat.card
(F ⧸ (((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F))) =
Nat.card (Q ⧸ (H : Subgroup Q)) := by
simpa [OpenSubgroup.comap] using
(Subgroup.index_comap_of_surjective (H := (H : Subgroup Q)) (f := π) hπsurj)
refine ⟨Fdata, e, hxNrange, ?_⟩
calc
Cardinal.mk Fdata.basis =
(_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X)
(Nat.card
(F ⧸
(((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F)))) :
Cardinal) := hCard
_ = (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (Q ⧸ (H : Subgroup Q))) :
Cardinal) := by
exact_mod_cast congrArg (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X)) hIndexProof. 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. 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. 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 exists_finiteConvergingSetBasis_comap_openSubgroup_of_minimalRightCosetPower
{C : ProCGroups.FiniteGroupClass.{u}}
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
(hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
(hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
(hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
{X : Type u} [Finite X]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
[DiscreteTopology (Set.range ι)]
(hF : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
{Q : Type u} [Group Q] [TopologicalSpace Q]
(π : F →* Q) (hπcont : Continuous π)
(H : OpenSubgroup Q) (x : X) {N : ℕ}
(hN : 0 < N)
(hcosetPow :
openSubgroupRightCoset H ((π (ι x)) ^ N) = openSubgroupRightCoset H (1 : Q))
(hcosetMin :
∀ m : ℕ, 0 < m → m < N →
openSubgroupRightCoset H ((π (ι x)) ^ m) ≠ openSubgroupRightCoset H (1 : Q))
(hpow_ne : (ι x) ^ N ≠ 1) :
∃ Fdata : FreeProCGroupOnConvergingSetData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
∃ e : Fdata.carrier ≃ₜ*
↥((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F),
(⟨(ι x) ^ N,
by
change π ((ι x) ^ N) ∈ (H : Subgroup Q)
have hmemQ : (π (ι x)) ^ N ∈ (H : Subgroup Q) :=
(openSubgroupRightCoset_eq_basepoint_iff_mem (H := H)).mp hcosetPow
simpa [map_pow] using hmemQ
⟩ :
↥((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F)) ∈
Set.range (e ∘ Fdata.inclusion) ∧
Finite Fdata.basisThis is the right-coset formulation of the finite pointed-control theorem for preimages of open subgroups.
Show proof
by
have hpow :
(ι x) ^ N ∈ ((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F) := by
change π ((ι x) ^ N) ∈ (H : Subgroup Q)
have hmemQ : (π (ι x)) ^ N ∈ (H : Subgroup Q) :=
(openSubgroupRightCoset_eq_basepoint_iff_mem (H := H)).mp hcosetPow
simpa [map_pow] using hmemQ
have hmin :
∀ m : ℕ, 0 < m → m < N →
(ι x) ^ m ∉ ((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F) := by
intro m hm hlt hmcomap
have hmemQ : (π (ι x)) ^ m ∈ (H : Subgroup Q) := by
change π ((ι x) ^ m) ∈ (H : Subgroup Q) at hmcomap
simpa [map_pow] using hmcomap
exact hcosetMin m hm hlt <|
(openSubgroupRightCoset_eq_basepoint_iff_mem (H := H)).2 hmemQ
simpa [hpow] using
exists_finiteConvergingSetBasis_comap_openSubgroup_of_minimalGeneratorPower
(C := C) hForm hSub hIso hQuot hExt hF π hπcont H x hN hpow hpow_ne hminProof. 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. 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. 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 exists_basis_comap_openSubgroup_of_extensionClosed_finiteRank_of_minimalRightCosetPower
(C : ProCGroups.FiniteGroupClass.{u})
(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} [Finite X]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
[DiscreteTopology (Set.range ι)]
(hF : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
{Q : Type u} [Group Q] [TopologicalSpace Q]
(π : F →* Q) (hπcont : Continuous π) (hπsurj : Function.Surjective π)
(H : OpenSubgroup Q) (x : X) {N : ℕ}
(hN : 0 < N)
(hcosetPow :
openSubgroupRightCoset H ((π (ι x)) ^ N) = openSubgroupRightCoset H (1 : Q))
(hcosetMin :
∀ m : ℕ, 0 < m → m < N →
openSubgroupRightCoset H ((π (ι x)) ^ m) ≠ openSubgroupRightCoset H (1 : Q))
(hpow_ne : (ι x) ^ N ≠ 1) :
∃ Fdata : FreeProCGroupOnConvergingSetData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
∃ e : Fdata.carrier ≃ₜ*
↥((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F),
(⟨(ι x) ^ N,
by
change π ((ι x) ^ N) ∈ (H : Subgroup Q)
have hmemQ : (π (ι x)) ^ N ∈ (H : Subgroup Q) :=
(openSubgroupRightCoset_eq_basepoint_iff_mem (H := H)).mp hcosetPow
simpa [map_pow] using hmemQ
⟩ :
↥((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F)) ∈
Set.range (e ∘ Fdata.inclusion) ∧
Cardinal.mk Fdata.basis =
(_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (Q ⧸ (H : Subgroup Q))) :
Cardinal)This is the right-coset formulation of the finite-rank theorem for preimages of open subgroups.
Show proof
by
have hpow :
(ι x) ^ N ∈ ((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F) := by
change π ((ι x) ^ N) ∈ (H : Subgroup Q)
have hmemQ : (π (ι x)) ^ N ∈ (H : Subgroup Q) :=
(openSubgroupRightCoset_eq_basepoint_iff_mem (H := H)).mp hcosetPow
simpa [map_pow] using hmemQ
have hmin :
∀ m : ℕ, 0 < m → m < N →
(ι x) ^ m ∉ ((OpenSubgroup.comap π hπcont H : OpenSubgroup F) : Subgroup F) := by
intro m hm hlt hmcomap
have hmemQ : (π (ι x)) ^ m ∈ (H : Subgroup Q) := by
change π ((ι x) ^ m) ∈ (H : Subgroup Q) at hmcomap
simpa [map_pow] using hmcomap
exact hcosetMin m hm hlt <|
(openSubgroupRightCoset_eq_basepoint_iff_mem (H := H)).2 hmemQ
simpa [hpow] using
exists_basis_comap_openSubgroup_of_extensionClosed_finiteRank_of_minimalGeneratorPower
(C := C) hVar hIso hExt hcyc hF π hπcont hπsurj H x hN hpow hpow_ne hminProof. 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. 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. 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.
□