import
def DenseAbstractSchreierFiniteQuotientLiftProperty
(C : ProCGroups.FiniteGroupClass.{u})
{F : Type u} [Group F] [TopologicalSpace F]
(H : OpenSubgroup F)
{Y : Type u}
(φY : FreeGroup Y →* ↥(H : Subgroup F)) : Prop :=
∀ {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
[Finite Q] [DiscreteTopology Q],
C Q →
∀ ψQ : FreeGroup Y →* Q,
∃! φbar : ↥(H : Subgroup F) →* Q,
Continuous φbar ∧ φbar.comp φY = ψQFinite-discrete quotient lift property for a dense abstract Schreier model of an open subgroup.
theorem denseAbstractSchreierFiniteQuotientLiftProperty_of_equiv
(C : ProCGroups.FiniteGroupClass.{u})
{F : Type u} [Group F] [TopologicalSpace F]
(H : OpenSubgroup F)
{L : Type u} [Group L]
{Y : Type u}
(eY : FreeGroup Y ≃* L)
(ψ : L →* ↥(H : Subgroup F))
(hψfinite :
∀ {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
[Finite Q] [DiscreteTopology Q],
C Q →
∀ χL : L →* Q,
∃! φbar : ↥(H : Subgroup F) →* Q,
Continuous φbar ∧ φbar.comp ψ = χL) :
DenseAbstractSchreierFiniteQuotientLiftProperty
(C := C) H (ψ.comp eY.toMonoidHom)Show proof
by
intro Q _ _ _ _ _ hQ ψQ
let χL : L →* Q := ψQ.comp eY.symm.toMonoidHom
have hχLFac : χL.comp eY.toMonoidHom = ψQ := by
apply MonoidHom.ext
intro w
simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply,
MulEquiv.symm_apply_apply, χL]
rcases hψfinite hQ χL with ⟨φbar, hφbar, hφbarUnique⟩
refine ⟨φbar, ?_, ?_⟩
· refine ⟨hφbar.1, ?_⟩
apply MonoidHom.ext
intro w
calc
(φbar.comp (ψ.comp eY.toMonoidHom)) w = (φbar.comp ψ) (eY w) := rfl
_ = χL (eY w) := by
exact congrArg (fun f : L →* Q => f (eY w)) hφbar.2
_ = ψQ w := by
exact congrArg (fun f : FreeGroup Y →* Q => f w) hχLFac
· intro φbar' hφbar'
apply hφbarUnique
refine ⟨hφbar'.1, ?_⟩
apply MonoidHom.ext
intro l
rcases eY.surjective l with ⟨w, rfl⟩
have hw' :
(φbar'.comp (ψ.comp eY.toMonoidHom)) w = ψQ w :=
congrArg (fun f : FreeGroup Y →* Q => f w) hφbar'.2
calc
(φbar'.comp ψ) (eY w) = (φbar'.comp (ψ.comp eY.toMonoidHom)) w := rfl
_ = ψQ w := hw'
_ = χL (eY w) := by simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply,
MulEquiv.symm_apply_apply, χL]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 isProCCompletion_denseAbstractSchreier_of_finiteQuotientLifts
(C : ProCGroups.FiniteGroupClass.{u})
(hForm : ProCGroups.FiniteGroupClass.Formation C)
(hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
(hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
(hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
{X : Type u}
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
(hF : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
(H : OpenSubgroup F)
{Y : Type u}
[TopologicalSpace (FreeGroup Y)] [IsTopologicalGroup (FreeGroup Y)]
[DiscreteTopology (FreeGroup Y)]
{φY : FreeGroup Y →ₜ* ↥(H : Subgroup F)}
(hφYdense : DenseRange φY)
(hfinite :
DenseAbstractSchreierFiniteQuotientLiftProperty (C := C) H φY.toMonoidHom) :
ProCGroups.Completion.IsProCCompletion
(ProCGroups.ProC.finiteGroupClassProCPredicate C)
(FreeGroup Y) ↥(H : Subgroup F) φYShow proof
by
have hHproC : ProCGroups.ProC.IsProCGroup C ↥(H : Subgroup F) := by
exact
ProCGroups.ProC.IsProCGroup.of_isClosed_subgroup
(C := C) hIso hSub hQuot hF.isProC (H : Subgroup F)
(Subgroup.isClosed_of_isOpen (H : Subgroup F) H.isOpen')
refine ProCGroups.Completion.isProCCompletion_of_finiteQuotientLifts
(C := C) (hForm := hForm) (G := FreeGroup Y) (Ghat := ↥(H : Subgroup F))
hHproC (ι := φY) hφYdense ?_
intro Q _ _ _ _ _ hQ ψQ
rcases hfinite hQ ψQ.toMonoidHom with ⟨φbar, hφbar, hφbarUnique⟩
let φbarCont : ↥(H : Subgroup F) →ₜ* Q :=
{ toMonoidHom := φbar
continuous_toFun := hφbar.1 }
refine ⟨φbarCont, ?_, ?_⟩
· apply ContinuousMonoidHom.toMonoidHom_injective
exact hφbar.2
· intro φbarCont' hφbarCont'
apply ContinuousMonoidHom.toMonoidHom_injective
exact hφbarUnique φbarCont'.toMonoidHom
⟨φbarCont'.continuous_toFun, congrArg ContinuousMonoidHom.toMonoidHom hφbarCont'⟩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 subgroup_le_topologicalClosure_of_topologicallyGenerates_local
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(H : OpenSubgroup G)
{S : Set ↥(H : Subgroup G)}
(hS : Generation.TopologicallyGenerates (G := ↥(H : Subgroup G)) S) :
(H : Subgroup G) ≤
(Subgroup.closure (((↑) : ↥(H : Subgroup G) → G) '' S)).topologicalClosureA topologically generating subset of an open subgroup generates a dense subgroup after including it into the ambient group.
Show proof
by
let D : Subgroup ↥(H : Subgroup G) := Subgroup.closure S
have hDense : Dense (D : Set ↥(H : Subgroup G)) :=
(Generation.topologicallyGenerates_iff_dense (G := ↥(H : Subgroup G)) (X := S)).1 hS
rw [Subtype.dense_iff] at hDense
have hmap :
D.map (H : Subgroup G).subtype =
Subgroup.closure (((↑) : ↥(H : Subgroup G) → G) '' S) := by
simpa [TopologicalGroup.image_subtype_eq_map] using ((H : Subgroup G).subtype.map_closure S)
have himage :
((↑) : ↥(H : Subgroup G) → G) '' (D : Set ↥(H : Subgroup G)) =
((D.map (H : Subgroup G).subtype : Subgroup G) : Set G) := by
exact TopologicalGroup.image_subtype_eq_map (H : Subgroup G).subtype D
intro g hg
have hg' :
g ∈ closure (((D.map (H : Subgroup G).subtype : Subgroup G) : Set G)) := by
have : g ∈ closure (((↑) : ↥(H : Subgroup G) → G) '' (D : Set ↥(H : Subgroup G))) :=
hDense hg
rwa [himage] at this
have hg'' :
g ∈ ((D.map (H : Subgroup G).subtype).topologicalClosure : Set G) := by
simpa [Subgroup.topologicalClosure_coe] using hg'
simpa [hmap] using hg''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 topologicallyFinitelyGenerated_of_openSubgroup_local
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G]
(H : OpenSubgroup G)
(hH : ProCGroups.FiniteGeneration.TopologicallyFinitelyGenerated ↥(H : Subgroup G)) :
ProCGroups.FiniteGeneration.TopologicallyFinitelyGenerated GThe Reidemeister--Schreier identity follows from the corresponding rewriting calculation.
Show proof
by
classical
rcases hH with ⟨sH, hsH⟩
letI : Finite (OpenSubgroupRightQuotient H) :=
finite_openSubgroupRightQuotient (F := G) H
letI : Fintype (OpenSubgroupRightQuotient H) :=
Fintype.ofFinite (OpenSubgroupRightQuotient H)
let τ := openSubgroupRightCosetSection (F := G) H
let sReps : Finset G := Finset.univ.image τ
let s : Finset G := sReps ∪ sH.image Subtype.val
let K : Subgroup G := Subgroup.closure (s : Set G)
have hHle' :
(H : Subgroup G) ≤
(Subgroup.closure
(((↑) : ↥(H : Subgroup G) → G) ''
((sH : Finset ↥(H : Subgroup G)) : Set ↥(H : Subgroup G)))).topologicalClosure :=
subgroup_le_topologicalClosure_of_topologicallyGenerates_local H (by simpa using hsH)
have hImageLe : Subgroup.closure
(((↑) : ↥(H : Subgroup G) → G) ''
((sH : Finset ↥(H : Subgroup G)) : Set ↥(H : Subgroup G))) ≤ K := by
refine Subgroup.closure_mono ?_
intro g hg
rcases hg with ⟨x, hx, rfl⟩
have hx' : (x : G) ∈ sH.image Subtype.val := by
exact Finset.mem_image.mpr ⟨x, by simpa using hx, rfl⟩
exact Finset.mem_coe.2 (Finset.mem_union_right sReps hx')
have hImageLe' :
(Subgroup.closure
(((↑) : ↥(H : Subgroup G) → G) ''
((sH : Finset ↥(H : Subgroup G)) : Set ↥(H : Subgroup G)))).topologicalClosure ≤
K.topologicalClosure :=
Subgroup.topologicalClosure_minimal _
(hImageLe.trans (Subgroup.le_topologicalClosure _))
(Subgroup.isClosed_topologicalClosure _)
have hHle : (H : Subgroup G) ≤ K.topologicalClosure := fun g hg => hImageLe' (hHle' hg)
have htop : K.topologicalClosure = ⊤ := by
apply top_unique
intro g _hg
let q : OpenSubgroupRightQuotient H := openSubgroupRightCoset H g
have hEq0 : openSubgroupRightCoset H (τ q) = q :=
openSubgroupRightCosetSection_spec (F := G) H q
have hEq :
openSubgroupRightCoset H g = openSubgroupRightCoset H (τ q) := by
simpa [q] using hEq0.symm
have hrel : QuotientGroup.rightRel (H : Subgroup G) g (τ q) :=
Quotient.exact' hEq
have hgH0 : τ q * g⁻¹ ∈ (H : Subgroup G) := by
simpa using (QuotientGroup.rightRel_apply.mp hrel)
have hgH : g * (τ q)⁻¹ ∈ (H : Subgroup G) := by
simpa [mul_inv_rev, mul_assoc] using ((H : Subgroup G).inv_mem hgH0)
have hgH' : g * (τ q)⁻¹ ∈ (K.topologicalClosure : Subgroup G) :=
hHle hgH
have hτK : τ q ∈ (K.topologicalClosure : Subgroup G) := by
have hτmem : τ q ∈ (sReps : Set G) := by
exact Finset.mem_coe.2 <| Finset.mem_image.mpr ⟨q, Finset.mem_univ q, rfl⟩
have hτmem' : τ q ∈ (s : Set G) := by
exact Finset.mem_coe.2 (Finset.mem_union_left _ hτmem)
exact Subgroup.le_topologicalClosure K (Subgroup.subset_closure hτmem')
have hmul :
(g * (τ q)⁻¹) * τ q ∈ (K.topologicalClosure : Subgroup G) :=
(K.topologicalClosure).mul_mem hgH' hτK
simpa [mul_assoc] using hmul
refine ⟨s, ?_⟩
simpa [Generation.TopologicallyGenerates, K, s] using htopProof. 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 isProCCompletion_freeGroupLift_of_finiteBasis
{C : ProCGroups.FiniteGroupClass.{u}}
(hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
(hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
(hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
{X : Type u} [Finite X]
[TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
[DiscreteTopology (FreeGroup X)]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
(hF : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι) :
ProCGroups.Completion.IsProCCompletion
(ProCGroups.ProC.finiteGroupClassProCPredicate C)
(FreeGroup X) F
{ toMonoidHom := FreeGroup.lift ι
continuous_toFun := continuous_of_discreteTopology }A finite converging-set free pro-\(C\) basis realizes the pro-\(C\) completion of the abstract free group on the same basis.
Show proof
by
let φ : FreeGroup X →ₜ* F :=
{ toMonoidHom := FreeGroup.lift ι
continuous_toFun := continuous_of_discreteTopology }
change ProCGroups.Completion.IsProCCompletion
(ProCGroups.ProC.finiteGroupClassProCPredicate C) (FreeGroup X) F φ
refine
{ isProC := hF.isProC
denseRange := ?_
existsUnique_lift := ?_ }
· simpa [φ] using
denseRange_freeGroupLift_of_topologicallyGenerates
(F := F) (X := X) hF.generates_range
· intro G _ _ _ hG ψ
let φX : X → G := fun x => ψ (FreeGroup.of x)
let S : Subgroup G := (Subgroup.closure (Set.range φX)).topologicalClosure
have hSproC : ProCGroups.ProC.IsProCGroup C S := by
exact
ProCGroups.ProC.IsProCGroup.of_isClosed_subgroup
(C := C) hIso hSub hQuot hG S (Subgroup.isClosed_topologicalClosure _)
let φS : X → S := fun x =>
⟨φX x, Subgroup.le_topologicalClosure _
(Subgroup.subset_closure ⟨x, rfl⟩)⟩
have hφSconv : FamilyConvergesToOne (G := S) φS := by
exact FamilyConvergesToOne.of_finite_domain (G := S) φS
have hφSgen :
Generation.TopologicallyGenerates (G := S) (Set.range φS) := by
simpa [S, φS, φX] using
topologicallyGenerates_topologicalClosure_of_range φX
rcases hF.existsUnique_lift hSproC φS hφSconv hφSgen with
⟨σS, hσS, _⟩
let σ : F →ₜ* G :=
{ toMonoidHom := S.subtype.comp σS
continuous_toFun := by
simpa using continuous_subtype_val.comp hσS.1 }
have hσfac : σ.comp φ = ψ := by
apply ContinuousMonoidHom.toMonoidHom_injective
apply FreeGroup.ext_hom
intro x
change (S.subtype.comp σS) (FreeGroup.lift ι (FreeGroup.of x)) = ψ (FreeGroup.of x)
simpa [φS, φX] using congrArg Subtype.val (hσS.2 x)
refine ⟨σ, hσfac, ?_⟩
intro g hg
letI : T2Space G := ProCGroups.ProC.IsProCGroup.t2Space hG
apply ContinuousMonoidHom.toMonoidHom_injective
apply continuousMonoidHom_eq_of_agrees_on_topologicallyGeneratingSet
(G := F) (A := G) hF.generates_range g.continuous_toFun σ.continuous_toFun
intro y hy
rcases hy with ⟨x, rfl⟩
have hσx := congrArg (fun k : FreeGroup X →ₜ* G => k (FreeGroup.of x)) hσfac
have hgx := congrArg (fun k : FreeGroup X →ₜ* G => k (FreeGroup.of x)) hg
have hσx' : σ (ι x) = ψ (FreeGroup.of x) := by
change σ (FreeGroup.lift ι (FreeGroup.of x)) = ψ (FreeGroup.of x) at hσx
simpa using hσx
have hgx' : g (ι x) = ψ (FreeGroup.of x) := by
change g (FreeGroup.lift ι (FreeGroup.of x)) = ψ (FreeGroup.of x) at hgx
simpa using hgx
exact hgx'.trans hσx'.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. 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 isProCCompletion_freeGroupLift_of_exactGeneratingFamily_of_completion
{C : ProCGroups.FiniteGroupClass.{u}}
(hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
(hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
(hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
(hcyc :
∃ (A : Type u) (_ : Group A) (_ : Finite A),
C A ∧ IsCyclic A ∧ Nontrivial A)
{n : ℕ}
{H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
{Y : Type u}
[TopologicalSpace (FreeGroup Y)] [IsTopologicalGroup (FreeGroup Y)]
[DiscreteTopology (FreeGroup Y)]
[TopologicalSpace (FreeGroup (ULift.{u} (Fin n)))]
[IsTopologicalGroup (FreeGroup (ULift.{u} (Fin n)))]
[DiscreteTopology (FreeGroup (ULift.{u} (Fin n)))]
(hYcard : Nat.card Y = n)
{φY : FreeGroup Y →ₜ* H}
(hCompY :
ProCGroups.Completion.IsProCCompletion
(ProCGroups.ProC.finiteGroupClassProCPredicate C) (FreeGroup Y) H φY)
{κ : ULift.{u} (Fin n) → H}
(hκ : Generation.GeneratesAndConvergesToOne (G := H) (Set.range κ)) :
ProCGroups.Completion.IsProCCompletion
(ProCGroups.ProC.finiteGroupClassProCPredicate C)
(FreeGroup (ULift.{u} (Fin n))) H
{ toMonoidHom := FreeGroup.lift κ
continuous_toFun := continuous_of_discreteTopology }If a finite exact generating family has the same cardinality as an abstract free model whose completion is the target, then that exact family realizes the same pro-C completion.
Show proof
by
have hYfin : Finite Y := by
by_cases h0 : n = 0
· have hY0 : Nat.card Y = 0 := by rw [hYcard, h0]
letI : CompactSpace H := ProCGroups.ProC.IsProCGroup.compactSpace hCompY.isProC
letI : T2Space H := ProCGroups.ProC.IsProCGroup.t2Space hCompY.isProC
letI : TotallyDisconnectedSpace H :=
ProCGroups.ProC.IsProCGroup.totallyDisconnectedSpace hCompY.isProC
haveI : IsEmpty (ULift.{u} (Fin n)) := by
rw [h0]
infer_instance
have hκrange : Set.range κ = (∅ : Set H) := by
ext z
constructor
· rintro ⟨x, rfl⟩
exact isEmptyElim x
· intro hz
simp only [Set.mem_empty_iff_false] at hz
have hHtriv : ∀ x : H, x = 1 := by
intro x
have hxmem :
x ∈ ((Subgroup.closure (Set.range κ)).topologicalClosure : Set H) := by
have hκgen : Generation.TopologicallyGenerates (G := H) (Set.range κ) := hκ.1
rw [Generation.TopologicallyGenerates] at hκgen
rw [hκgen]
simp only [Subgroup.coe_top, Set.mem_univ]
have hxmem' :
x ∈ ((Subgroup.closure ((∅ : Set H))).topologicalClosure : Set H) := by
simpa [hκrange] using hxmem
simpa [Subgroup.coe_topologicalClosure_bot, closure_singleton] using hxmem'
have hYempty : IsEmpty Y := by
refine ⟨fun y => ?_⟩
rcases
exists_nontrivial_topologicallyCyclic_proC_of_finiteGroupClass
C hQuot hcyc with
⟨A, _instGroupA, _instTopA, _instTopGroupA, hA, a, ha1, _hgena⟩
let ψY : FreeGroup Y →ₜ* A :=
{ toMonoidHom := FreeGroup.lift (fun _ : Y => a)
continuous_toFun := continuous_of_discreteTopology }
have hψYne : ψY (FreeGroup.of y) ≠ 1 := by
change FreeGroup.lift (fun _ : Y => a) (FreeGroup.of y) ≠ 1
simpa using ha1
rcases hCompY.existsUnique_lift hA ψY with
⟨σ, hσ, _⟩
have hyfac :=
congrArg (fun f : FreeGroup Y →ₜ* A => f (FreeGroup.of y)) hσ
have hyEq : ψY (FreeGroup.of y) = 1 := by
calc
ψY (FreeGroup.of y) = σ (φY (FreeGroup.of y)) := hyfac.symm
_ = σ 1 := by rw [hHtriv (φY (FreeGroup.of y))]
_ = 1 := map_one σ
exact hψYne hyEq
letI : IsEmpty Y := hYempty
infer_instance
· exact Nat.finite_of_card_ne_zero (α := Y) (by rw [hYcard]; exact h0)
letI : Finite Y := hYfin
have hFreeY :
IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
Y H (fun y => φY (FreeGroup.of y)) := by
exact
proCCompletionOfAbstractFreeGroup_is_free
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
(X := Y) (Fhat := H) (ι := φY) hCompY
have hcard :
Cardinal.mk Y = Cardinal.mk (ULift.{u} (Fin n)) := by
exact Cardinal.mk_congr ((Finite.equivFinOfCardEq hYcard).trans Equiv.ulift.symm)
have hFreeκ :
IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
(ULift.{u} (Fin n)) H κ := by
exact
finite_generatingFamily_is_basis_of_finiteGroupClass
(C := C) (X := Y) (Y := ULift.{u} (Fin n)) hFreeY hcard hκ.1
exact
isProCCompletion_freeGroupLift_of_finiteBasis
(C := C) hSub hIso hQuot hFreeκProof. Choose an equivalence between the finite indexing types and compare the two free groups through the induced relabeling of generators. The given exact generating family supplies the same universal pro-C completion map after this relabeling.
□theorem exists_compactPointedBasis_openSubgroup_of_freeProCOnConvergingSet
(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) :
∃ κ : OpenSubgroupRightQuotient H × OnePoint X → ↥(H : Subgroup F),
Continuous κ ∧
(∀ q : OpenSubgroupRightQuotient H, κ (q, OnePoint.infty) = 1) ∧
κ (openSubgroupRightCoset H (1 : F), OnePoint.infty) = 1 ∧
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.valCompact pointed basis bridge: adjoining the point at infinity to a discrete converging basis, the open subgroup inherits a compact pointed right Schreier basis.
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 x
refine OnePoint.rec ?_ ?_ x
· 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)
exact
exists_pointedFreeRightSchreierGeneratorFamily_of_openSubgroup
(C := C) hForm hSub hIso hQuot hExt hPointed 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. 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_convergingSetBasis_openSubgroup_of_pointedFreeProCOnCompact
{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)
(hBridge :
PointedToConvergingSetBasisBridge (ProCGroups.ProC.finiteGroupClassProCPredicate C))
{X : Type u} [TopologicalSpace X] [CompactSpace X] {x0 : X}
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
(hF : IsPointedFreeProCGroupOn
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X x0 F ι)
(H : OpenSubgroup F) :
∃ Fdata : FreeProCGroupOnConvergingSetData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F))An open subgroup of a compact pointed free pro-\(C\) group admits a free pro-\(C\) model on a set converging to \(1\), using the explicit right Schreier family and the standard pointed-to-converging-set basis bridge.
Show proof
by
rcases
exists_pointedFreeRightSchreierGeneratorFamily_of_openSubgroup
(C := C) hForm hSub hIso hQuot hExt hF H with
⟨κ, _hκcont, _hκbase, _hκone, _hκcompact, _hκclosed, hκfree⟩
exact hBridge hκfreeProof. 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_convergingSetBasis_openSubgroup_of_freeProCOnConvergingSet
(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)
(hBridge :
PointedToConvergingSetBasisBridge (ProCGroups.ProC.finiteGroupClassProCPredicate 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) :
∃ Fdata : FreeProCGroupOnConvergingSetData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F))Converging-set version of the open-subgroup basis theorem under the finite-class closure bundle.
Show proof
by
rcases
exists_compactPointedBasis_openSubgroup_of_freeProCOnConvergingSet
C hForm hSub hIso hQuot hExt hF H with
⟨κ, _hκcont, _hκbase, _hκone, _hκcompact, _hκclosed, hκfree⟩
exact hBridge hκfreeProof. 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
(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)
{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) :
∃ Fdata : FreeProCGroupOnConvergingSetData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F))Show proof
by
rcases hVar.closureBundle_of_isomClosed_extensionClosed hIso hExt with
⟨hForm, hSub, hIso', hQuot, hExt'⟩
exact
exists_convergingSetBasis_openSubgroup_of_freeProCOnConvergingSet
C hForm hSub hIso' hQuot hExt' hBridge 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_of_subgroupClosed
(C : ProCGroups.FiniteGroupClass.{u})
(hBridge :
PointedToConvergingSetBasisBridge (ProCGroups.ProC.finiteGroupClassProCPredicate C))
(hC : ProCGroups.FiniteGroupClass.MelnikovFormation C)
(hSub : ProCGroups.FiniteGroupClass.SubgroupClosed 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) :
∃ Fdata : FreeProCGroupOnConvergingSetData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C),
Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F))Melnikov-formation variant with explicit subgroup closure. The conclusion is formulated for an arbitrary open subgroup because the pro-\(C\)-group closure bundle is already strong enough for the Schreier argument.
Show proof
by
rcases hC.closureBundle_of_subgroupClosed hSub with
⟨hForm, hSub', hIso, hQuot, hExt⟩
exact
exists_convergingSetBasis_openSubgroup_of_freeProCOnConvergingSet
C hForm hSub' hIso hQuot hExt hBridge 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.
□