ProCGroups.FreeProC.FinitelyGenerated
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
Imported by
theorem existsUnique_liftHom_of_finite
(C : ProCGroups.FiniteGroupClass.{u})
[hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
[hIso : Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
{X : Type v} [Finite X]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
(hι :
IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(hG : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G))
(φ : X → G) :
∃! f : F →ₜ* G, ∀ x, f (ι x) = φ xShow proof
by
exact
hι.existsUnique_liftHom_of_convergesToOne_of_finiteGroupClass
C hIso.out hVar.out.subgroupClosed hVar.out.quotientClosed
hG φ (FamilyConvergesToOne.of_finite_domain (G := G) φ)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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.
□noncomputable def liftHomOfFinite
(C : ProCGroups.FiniteGroupClass.{u})
[Fact (ProCGroups.FiniteGroupClass.Variety C)]
[Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
{X : Type v} [Finite X]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
(hι :
IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(hG : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G))
(φ : X → G) :
F →ₜ* G :=
Classical.choose
(ExistsUnique.exists
(hι.existsUnique_liftHom_of_finite C hG φ))@[simp] theorem liftHomOfFinite_apply
(C : ProCGroups.FiniteGroupClass.{u})
[Fact (ProCGroups.FiniteGroupClass.Variety C)]
[Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
{X : Type v} [Finite X]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
(hι :
IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(hG : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G))
(φ : X → G) (x : X) :
hι.liftHomOfFinite C hG φ (ι x) = φ xShow proof
Classical.choose_spec
(ExistsUnique.exists
(hι.existsUnique_liftHom_of_finite C hG φ)) xProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For density or closed-generation statements, the calculation is first made on the algebraic span of the group-like generators. The image of this span is dense in the completed target, and closedness of the kernel, image, or generated submodule allows the containment obtained on generators to pass to the completed closure. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem liftHomOfFinite_unique
(C : ProCGroups.FiniteGroupClass.{u})
[Fact (ProCGroups.FiniteGroupClass.Variety C)]
[Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
{X : Type v} [Finite X]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
(hι :
IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(hG : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G))
(φ : X → G)
{f : F →ₜ* G} (hf : ∀ x, f (ι x) = φ x) :
f = hι.liftHomOfFinite C hG φThe finite-rank lift is unique among continuous homomorphisms with the prescribed basis values.
Show proof
by
rcases hι.existsUnique_liftHom_of_finite C hG φ with
⟨g, _hg, huniq⟩
have hchosen :
hι.liftHomOfFinite C hG φ = g := by
apply huniq
intro x
exact hι.liftHomOfFinite_apply C hG φ x
exact (huniq f hf).trans hchosen.symmProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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 isFreeProCGroup_of_finite
(C : ProCGroups.FiniteGroupClass.{u})
[hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
[hIso : Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
{X : Type u} [TopologicalSpace X] [DiscreteTopology X] [Finite X]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
(hι :
IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι) :
IsFreeProCGroup (ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ιShow proof
by
refine
{ isProC := hι.isProC
continuous_ι := continuous_of_discreteTopology
generates_range := hι.generates_range
existsUnique_lift := ?_ }
intro G _ _ _ hG φ _hφ
rcases hι.existsUnique_liftHom_of_finite C hG φ with
⟨f, hf, huniq⟩
refine ⟨f.toMonoidHom, ⟨f.continuous, hf⟩, ?_⟩
intro g hg
let gc : F →ₜ* G := { toMonoidHom := g, continuous_toFun := hg.1 }
exact congrArg ContinuousMonoidHom.toMonoidHom (huniq gc hg.2)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For density or closed-generation statements, the calculation is first made on the algebraic span of the group-like generators. The image of this span is dense in the completed target, and closedness of the kernel, image, or generated submodule allows the containment obtained on generators to pass to the completed closure.
□structure FiniteRankData
(ProC : ProCGroups.ProC.ProCGroupPredicate.{u}) (n : ℕ) where
carrier : Type u
instGroup : Group carrier
instTopologicalSpace : TopologicalSpace carrier
instIsTopologicalGroup : IsTopologicalGroup carrier
inclusion : Fin n → carrier
isFree : IsFreeProCGroupOnConvergingSet (ProC := ProC) (Fin n) carrier inclusionA free pro-\(C\) group with an explicit finite basis \(\operatorname{Fin} n\).
theorem isProC (Fdata : FiniteRankData ProC n) :
ProC (G := Fdata.carrier)The carrier of finite-rank free pro-\(C\) data is a pro-\(C\) group.
Show proof
Fdata.isFree.isProCProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For density or closed-generation statements, the calculation is first made on the algebraic span of the group-like generators. The image of this span is dense in the completed target, and closedness of the kernel, image, or generated submodule allows the containment obtained on generators to pass to the completed closure. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem hom_ext
(Fdata : FiniteRankData ProC n)
{G : Type u} [Group G] [TopologicalSpace G] [T2Space G]
{f g : Fdata.carrier →ₜ* G}
(hfg : ∀ i, f (Fdata.inclusion i) = g (Fdata.inclusion i)) :
f = gShow proof
Fdata.isFree.hom_ext hfgProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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.
□noncomputable def liftHom
(C : ProCGroups.FiniteGroupClass.{u})
[Fact (ProCGroups.FiniteGroupClass.Variety C)]
[Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
{n : ℕ}
(Fdata :
FiniteRankData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) n)
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(hG : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G))
(φ : Fin n → G) :
Fdata.carrier →ₜ* G :=
Fdata.isFree.liftHomOfFinite C hG φ@[simp] theorem liftHom_apply
(C : ProCGroups.FiniteGroupClass.{u})
[Fact (ProCGroups.FiniteGroupClass.Variety C)]
[Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
{n : ℕ}
(Fdata :
FiniteRankData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) n)
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(hG : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G))
(φ : Fin n → G) (i : Fin n) :
Fdata.liftHom C hG φ (Fdata.inclusion i) = φ iShow proof
Fdata.isFree.liftHomOfFinite_apply C hG φ iProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For density or closed-generation statements, the calculation is first made on the algebraic span of the group-like generators. The image of this span is dense in the completed target, and closedness of the kernel, image, or generated submodule allows the containment obtained on generators to pass to the completed closure. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem liftHom_unique
(C : ProCGroups.FiniteGroupClass.{u})
[Fact (ProCGroups.FiniteGroupClass.Variety C)]
[Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
{n : ℕ}
(Fdata :
FiniteRankData
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) n)
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(hG : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G))
(φ : Fin n → G)
{f : Fdata.carrier →ₜ* G} (hf : ∀ i, f (Fdata.inclusion i) = φ i) :
f = Fdata.liftHom C hG φShow proof
Fdata.isFree.liftHomOfFinite_unique C hG φ hfProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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.
□noncomputable def equivOfSameRank
(Fdata Edata : FiniteRankData ProC n) :
Fdata.carrier ≃ₜ* Edata.carrier :=
Fdata.isFree.continuousMulEquivOfSameBasis Edata.isFreeThe canonical continuous multiplicative equivalence between two finite-rank free pro-\(C\) groups with the same rank.
@[simp] theorem equivOfSameRank_apply
(Fdata Edata : FiniteRankData ProC n) (i : Fin n) :
Fdata.equivOfSameRank Edata (Fdata.inclusion i) = Edata.inclusion iThe finite-rank comparison equivalence evaluates according to the chosen rank data.
Show proof
Fdata.isFree.continuousMulEquivOfSameBasis_apply Edata.isFree iProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For equivalence and homeomorphism statements, the two comparison maps are composed in both orders and evaluated on the coordinates that determine the source. Each composite reduces to the identity transition or to the chosen representative identity on finite stages, so the algebraic inverse laws and the topological inverse laws follow simultaneously. For density or closed-generation statements, the calculation is first made on the algebraic span of the group-like generators. The image of this span is dense in the completed target, and closedness of the kernel, image, or generated submodule allows the containment obtained on generators to pass to the completed closure.
□structure FiniteSubsetSystem
(ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
(X : Type u)
(F : Type u) [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
(ι : X → F) where
system : TopologicalGroupInverseSystemData (I := FiniteSubset X)
basis : ∀ s : FiniteSubset X, ↥s.1 → system.toInverseSystem.X s
stage_isFree :
∀ s : FiniteSubset X,
IsFreeProCGroupOnConvergingSet (ProC := ProC)
↥s.1 (system.toInverseSystem.X s) (basis s)
transition_basis :
∀ {s t : FiniteSubset X} (hst : s ≤ t) (x : ↥t.1),
system.toInverseSystem.map hst (basis t x) =
by
classical
exact if hx : x.1 ∈ s.1 then basis s ⟨x.1, hx⟩ else 1
stage_embedding :
∀ s : FiniteSubset X,
∃ e : system.toInverseSystem.X s →* F,
Continuous e ∧
Function.Injective e ∧
IsClosed (Set.range e) ∧
∀ x : ↥s.1, e (basis s x) = ι x.1
limitEquiv : Nonempty (F ≃ₜ* system.toInverseSystem.inverseLimit)theorem exists_finiteSubsetSystem
{ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}
{X : Type u}
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
(hProfinite :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
@ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _ →
InverseSystems.IsProfiniteSpace G)
(hClosed :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
(H : Subgroup G), IsClosed (H : Set G) →
@ProCGroups.ProC.ProCGroupPredicate.holds ProC H _ _ _)
(hFiniteQuot :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
(U : OpenNormalSubgroup G),
@ProCGroups.ProC.ProCGroupPredicate.holds ProC (G ⧸ (U : Subgroup G)) _ _ _)
(hF : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι) :
Nonempty (FiniteSubsetSystem ProC X F ι)Show proof
by
rcases exists_finiteSubsetSystem_raw
(ProC := ProC) (X := X) (F := F) (ι := ι)
hProfinite hClosed hFiniteQuot hF with
⟨S, basis, hbasis, htransition, hembed, hlimit⟩
exact
⟨{ system := S
basis := basis
stage_isFree := hbasis
transition_basis := htransition
stage_embedding := hembed
limitEquiv := hlimit }⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For density or closed-generation statements, the calculation is first made on the algebraic span of the group-like generators. The image of this span is dense in the completed target, and closedness of the kernel, image, or generated submodule allows the containment obtained on generators to pass to the completed closure.
□theorem isLimit_finiteSubsets
{ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}
{X : Type u}
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
(hProfinite :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
@ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _ →
InverseSystems.IsProfiniteSpace G)
(hClosed :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
(H : Subgroup G), IsClosed (H : Set G) →
@ProCGroups.ProC.ProCGroupPredicate.holds ProC H _ _ _)
(hFiniteQuot :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
(U : OpenNormalSubgroup G),
@ProCGroups.ProC.ProCGroupPredicate.holds ProC (G ⧸ (U : Subgroup G)) _ _ _)
(hF : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι) :
∃ S : FiniteSubsetSystem ProC X F ι,
Nonempty (F ≃ₜ* S.system.toInverseSystem.inverseLimit)Show proof
by
rcases exists_finiteSubsetSystem
(ProC := ProC) (X := X) (F := F) (ι := ι)
hProfinite hClosed hFiniteQuot hF with
⟨S⟩
exact ⟨S, S.limitEquiv⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For density or closed-generation statements, the calculation is first made on the algebraic span of the group-like generators. The image of this span is dense in the completed target, and closedness of the kernel, image, or generated submodule allows the containment obtained on generators to pass to the completed closure.
□theorem isLimit_finiteSubsets_of_infinite
{ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}
{X : Type u} [Infinite X]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
(hProfinite :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
@ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _ →
InverseSystems.IsProfiniteSpace G)
(hClosed :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
(H : Subgroup G), IsClosed (H : Set G) →
@ProCGroups.ProC.ProCGroupPredicate.holds ProC H _ _ _)
(hFiniteQuot :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(_hG : @ProCGroups.ProC.ProCGroupPredicate.holds ProC G _ _ _)
(U : OpenNormalSubgroup G),
@ProCGroups.ProC.ProCGroupPredicate.holds ProC (G ⧸ (U : Subgroup G)) _ _ _)
(hF : IsFreeProCGroupOnConvergingSet (ProC := ProC) X F ι) :
∃ S : FiniteSubsetSystem ProC X F ι,
Nonempty (F ≃ₜ* S.system.toInverseSystem.inverseLimit)Infinite-basis spelling of the finite-subset projective-limit theorem. The argument is the same as in the arbitrary-basis theorem, but this name is convenient for the standard infinite-rank use case.
Show proof
isLimit_finiteSubsets
(ProC := ProC) (X := X) (F := F) (ι := ι)
hProfinite hClosed hFiniteQuot hFProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For density or closed-generation statements, the calculation is first made on the algebraic span of the group-like generators. The image of this span is dense in the completed target, and closedness of the kernel, image, or generated submodule allows the containment obtained on generators to pass to the completed closure.
□theorem exists_finiteSubsetSystem_of_class
(C : ProCGroups.FiniteGroupClass.{u})
[hVar : Fact (ProCGroups.FiniteGroupClass.Variety C)]
[hIso : Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
{X : Type u}
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
(hF :
IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι) :
Nonempty
(FiniteSubsetSystem
(ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι)For a chosen finite group class, the finite-subset projective-limit system exists.
Show proof
by
refine exists_finiteSubsetSystem
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C)
(X := X) (F := F) (ι := ι) ?_ ?_ ?_ hF
· intro G _ _ _ hG
let hGprof : ProCGroups.IsProfiniteGroup G :=
ProCGroups.ProC.isProfiniteGroup_of_finiteGroupClassProCPredicate C hG
exact (InverseSystems.isProfiniteSpace_iff_compact_t2_totallyDisconnected (X := G)).2
⟨ProCGroups.IsProfiniteGroup.compactSpace hGprof,
ProCGroups.IsProfiniteGroup.t2Space hGprof,
ProCGroups.IsProfiniteGroup.totallyDisconnectedSpace hGprof⟩
· intro G _ _ _ hG H hH
exact
ProCGroups.ProC.IsProCGroup.of_isClosed_subgroup
hIso.out hVar.out.subgroupClosed hVar.out.quotientClosed hG H hH
· intro G _ _ _ hG U
let hGprof : ProCGroups.IsProfiniteGroup G :=
ProCGroups.ProC.isProfiniteGroup_of_finiteGroupClassProCPredicate C hG
letI : CompactSpace G := ProCGroups.IsProfiniteGroup.compactSpace hGprof
haveI : Finite (G ⧸ (U : Subgroup G)) :=
openNormalSubgroup_finiteQuotient (G := G) U
exact
ProCGroups.ProC.IsProCGroup.of_finite_discrete
(C := C) (G := G ⧸ (U : Subgroup G))
hVar.out.quotientClosed
(ProCGroups.ProC.IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
hIso.out hVar.out.quotientClosed hG U)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For density or closed-generation statements, the calculation is first made on the algebraic span of the group-like generators. The image of this span is dense in the completed target, and closedness of the kernel, image, or generated submodule allows the containment obtained on generators to pass to the completed closure.
□theorem isLimit_finiteSubsets_of_class_of_infinite
(C : ProCGroups.FiniteGroupClass.{u})
[Fact (ProCGroups.FiniteGroupClass.Variety C)]
[Fact (ProCGroups.FiniteGroupClass.IsomClosed C)]
{X : Type u} [Infinite X]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ι : X → F}
(hF :
IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι) :
∃ S : FiniteSubsetSystem
(ProCGroups.ProC.finiteGroupClassProCPredicate C) X F ι,
Nonempty (F ≃ₜ* S.system.toInverseSystem.inverseLimit)For a chosen finite group class, a free pro-\(C\) group on an infinite basis is the projective limit of its finite-subset free pro-\(C\) groups.
Show proof
by
rcases exists_finiteSubsetSystem_of_class
(C := C) (X := X) (F := F) (ι := ι) hF with
⟨S⟩
exact ⟨S, S.limitEquiv⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For density or closed-generation statements, the calculation is first made on the algebraic span of the group-like generators. The image of this span is dense in the completed target, and closedness of the kernel, image, or generated submodule allows the containment obtained on generators to pass to the completed closure.
□