CompletedGroupAlgebra.UniversalProperty.Basic
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.
theorem completedGroupAlgebra_isCompletedGroupAlgebraModel
(hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :
IsCompletedGroupAlgebraModel R G (Carrier R G)The concrete inverse-limit construction satisfies the universal-property specification for the completed group algebra.
Show proof
by
refine ⟨hR, hG, completedGroupAlgebra_isProfiniteRing (R := R) (G := G) hR, ?_⟩
refine ⟨completedGroupAlgebraNaturalTopology R G, ?_⟩
letI : TopologicalSpace (MonoidAlgebra R G) :=
completedGroupAlgebraNaturalTopology R G
exact ⟨toCompletedGroupAlgebraRingHom R G,
denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG,
continuous_toCompletedGroupAlgebraRingHom_naturalTopology (R := R) (G := G)⟩Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□def completedGroupAlgebraOf (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
[IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(g : G) : Carrier R G :=
toCompletedGroupAlgebra R G (MonoidAlgebra.of R G g)A group element maps to its image in the completed group algebra.
theorem completedGroupAlgebraProjection_of
(U : CompletedGroupAlgebraIndex G) (g : G) :
completedGroupAlgebraProjection R G U (completedGroupAlgebraOf R G g) =
MonoidAlgebra.single (openNormalSubgroupInClassProj
(C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) 1Projection of a completed group-like element to a finite quotient stage.
Show proof
by
rw [completedGroupAlgebraOf, completedGroupAlgebraProjection_toCompletedGroupAlgebra,
completedGroupAlgebraStageMap_of]Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. 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 completedGroupAlgebraOf_one :
completedGroupAlgebraOf R G 1 = (1 : Carrier R G)The completed group-like element attached to \(1\) is the unit.
Show proof
by
apply (completedGroupAlgebraSystem R G).ext
intro U
change completedGroupAlgebraProjection R G U (completedGroupAlgebraOf R G 1) =
completedGroupAlgebraProjection R G U (1 : Carrier R G)
rw [completedGroupAlgebraProjection_of, completedGroupAlgebraProjection_one]
change MonoidAlgebra.single
(openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U 1) (1 : R) = 1
rflProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem completedGroupAlgebraOf_mul (g h : G) :
completedGroupAlgebraOf R G (g * h) =
completedGroupAlgebraOf R G g * completedGroupAlgebraOf R G hCompleted group-like elements multiply according to the group law.
Show proof
by
apply (completedGroupAlgebraSystem R G).ext
intro U
change completedGroupAlgebraProjection R G U (completedGroupAlgebraOf R G (g * h)) =
completedGroupAlgebraProjection R G U (completedGroupAlgebraOf R G g * completedGroupAlgebraOf R G h)
rw [completedGroupAlgebraProjection_of, completedGroupAlgebraProjection_mul,
completedGroupAlgebraProjection_of, completedGroupAlgebraProjection_of]
change MonoidAlgebra.single
(openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U (g * h)) (1 : R) =
MonoidAlgebra.single
(openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) 1 *
MonoidAlgebra.single
(openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U h) 1
simp only [map_mul, MonoidAlgebra.single_mul_single, mul_one]Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem continuous_completedGroupAlgebraStageMap_of
(U : CompletedGroupAlgebraIndex G) :
letI : TopologicalSpace (CompletedGroupAlgebraStage R G U)The finite-stage group-like map \(G\to R[G/U]\) is continuous.
Show proof
(completedGroupAlgebraSystem R G).topologicalSpace U
Continuous fun g : G => completedGroupAlgebraStageMap R G U (MonoidAlgebra.of R G g) := by
letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
(completedGroupAlgebraSystem R G).topologicalSpace U
letI : DiscreteTopology (CompletedGroupAlgebraQuotient G U) :=
QuotientGroup.discreteTopology
(ProCGroups.openNormalSubgroup_isOpen (G := G) ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))
have hbasis :
Continuous fun q : CompletedGroupAlgebraQuotient G U =>
(MonoidAlgebra.of R (CompletedGroupAlgebraQuotient G U) q :
CompletedGroupAlgebraStage R G U) :=
continuous_of_discreteTopology
have hproj :
Continuous fun g : G =>
openNormalSubgroupInClassProj (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g := by
change Continuous
(QuotientGroup.mk' (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G))
exact continuous_quotient_mk'
simpa [MonoidAlgebra.of, completedGroupAlgebraStageMap_single] using hbasis.comp hprojProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. 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 continuous_completedGroupAlgebraOf :
Continuous (completedGroupAlgebraOf R G)The completed group-like map \(G \to \widehat{R[G]}\) is continuous.
Show proof
by
letI : ∀ U : CompletedGroupAlgebraIndex G, TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
fun U => (completedGroupAlgebraSystem R G).topologicalSpace U
have hval : Continuous fun g : G =>
fun U : CompletedGroupAlgebraIndex G =>
(show CompletedGroupAlgebraStage R G U from (completedGroupAlgebraOf R G g).1 U) := by
change Continuous fun g : G =>
fun U : CompletedGroupAlgebraIndex G =>
completedGroupAlgebraStageMap R G U (MonoidAlgebra.of R G g)
apply continuous_pi
intro U
exact continuous_completedGroupAlgebraStageMap_of (R := R) (G := G) U
exact Continuous.subtype_mk hval fun g => (completedGroupAlgebraOf R G g).2Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. 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 toCompletedGroupAlgebraRingHom_mem_span_completedGroupAlgebraOf
(x : MonoidAlgebra R G) :
toCompletedGroupAlgebraRingHom R G x ∈
Submodule.span R (Set.range (completedGroupAlgebraOf R G))The dense abstract group-algebra map lands in the span of the completed group-like elements.
Show proof
by
classical
induction x using Finsupp.induction with
| zero =>
rw [show toCompletedGroupAlgebraRingHom R G (0 : MonoidAlgebra R G) =
(0 : Carrier R G) by
exact map_zero (toCompletedGroupAlgebraRingHom R G)]
exact Submodule.zero_mem _
| single_add g r x _ _ ih =>
rw [map_add]
refine Submodule.add_mem _ ?_ ih
have hsingle :
toCompletedGroupAlgebraRingHom R G (MonoidAlgebra.single g r) =
r • completedGroupAlgebraOf R G g := by
rw [show MonoidAlgebra.single g r =
r • MonoidAlgebra.of R G g by
simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.smul_single, smul_eq_mul, mul_one]]
change toCompletedGroupAlgebra R G (r • MonoidAlgebra.of R G g) =
r • completedGroupAlgebraOf R G g
rw [toCompletedGroupAlgebra_smul]
rfl
rw [hsingle]
exact Submodule.smul_mem _ r (Submodule.subset_span ⟨g, rfl⟩)Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, quotient maps move the support from one coset space to another, while coefficient maps act only on coefficients; therefore the relevant formula is checked on singleton basis functions and then extended by additivity and multiplicativity. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem completedGroupAlgebraOf_dense_span (hG : ProCGroups.IsProfiniteGroup G) :
closure (Submodule.span R (Set.range (completedGroupAlgebraOf R G)) :
Set (Carrier R G)) = Set.univThe completed group-like elements topologically generate \(\widehat{R[G]}\) as an \(R\)-module.
Show proof
by
rw [Set.eq_univ_iff_forall]
intro y
have hy :
y ∈ closure (Set.range (toCompletedGroupAlgebraRingHom R G)) := by
rw [(denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG).closure_range]
exact Set.mem_univ y
exact closure_mono (by
intro z hz
rcases hz with ⟨x, rfl⟩
exact toCompletedGroupAlgebraRingHom_mem_span_completedGroupAlgebraOf
(R := R) (G := G) x) hyProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. 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 completedGroupAlgebraOf_freeProfiniteModule_prerequisites
(hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :
IsProfiniteRing R ∧ IsProfiniteModule R (Carrier R G) ∧
Continuous (completedGroupAlgebraOf R G) ∧
closure (Submodule.span R (Set.range (completedGroupAlgebraOf R G)) :
Set (Carrier R G)) = Set.univThese are the structural inputs for the free profinite-module statement in Lemma 5.3.5(d); the full continuous-linear universal property is proved below.
Show proof
by
exact ⟨hR, completedGroupAlgebra_isProfiniteModule (R := R) (G := G) hR,
continuous_completedGroupAlgebraOf (R := R) (G := G),
completedGroupAlgebraOf_dense_span (R := R) (G := G) hG⟩Proof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Kernel, image, and exactness assertions are proved by the two standard inclusions: an image element satisfies the required vanishing condition, and an element satisfying that condition is repackaged with the vanishing proof as a preimage. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. For dense-image and closure arguments, the equality is first established on the abstract group algebra and then passed to the completed object using finite-stage separation and closedness in the profinite topology. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. 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 completedGroupAlgebraContinuousLinearMap_ext_of_basis
(hG : ProCGroups.IsProfiniteGroup G)
{N : Type (max u v)} [AddCommGroup N] [TopologicalSpace N] [Module R N] [T2Space N]
{F K : Carrier R G →L[R] N}
(hbasis : ∀ g : G, F (completedGroupAlgebraOf R G g) =
K (completedGroupAlgebraOf R G g)) :
F = KThe uniqueness half of the universal property in Lemma 5.3.5(d): a continuous linear map out of \(\widehat{R[G]}\) is determined by its values on the completed group-like elements.
Show proof
by
apply ContinuousLinearMap.ext
intro x
have hclosed : IsClosed {x : Carrier R G | F x = K x} :=
isClosed_eq F.continuous K.continuous
have hspan :
(Submodule.span R (Set.range (completedGroupAlgebraOf R G)) :
Set (Carrier R G)) ⊆
{x : Carrier R G | F x = K x} := by
intro y hy
exact Submodule.span_induction
(fun z hz => by
rcases hz with ⟨g, rfl⟩
exact hbasis g)
(by simp only [Set.mem_setOf_eq, map_zero])
(fun z w _ _ hz hw => by
change F (z + w) = K (z + w)
rw [map_add, map_add, hz, hw])
(fun r z _ hz => by
change F (r • z) = K (r • z)
rw [map_smul, map_smul, hz])
hy
have hx :
x ∈ closure (Submodule.span R (Set.range (completedGroupAlgebraOf R G)) :
Set (Carrier R G)) := by
rw [completedGroupAlgebraOf_dense_span (R := R) (G := G) hG]
exact Set.mem_univ x
exact hclosed.closure_subset_iff.2 hspan hxProof. Let \(U\) range over the open normal finite-index subgroups of \(G\), and write the completed group algebra as the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\). An element or morphism of the completed algebra is determined by its composites with all finite-stage projections, so the proof is reduced to ordinary group-algebra calculations at the stages \(R[G/U]\). At a finite stage, the coordinate operations are those of the ordinary group algebra; checking zero, addition, multiplication, scalar action, or evaluation after projection is therefore a direct coordinatewise calculation. Finiteness is reduced to the finite quotient set together with the finite coefficient data, so the relevant finite-stage function space or quotient object is finite. Continuity is checked by the initial topology of the inverse limit: after composing with every finite-stage projection, the resulting map is a finite-stage homomorphism or a composition of such homomorphisms. Compatibility under refinement of finite quotients ensures that the verified finite-stage identities form a compatible family, and inverse-limit extensionality then proves the claimed completed statement. Every equality used in the completed algebra is therefore an equality of compatible families. The finite-stage maps respect refinement because they are induced by the same quotient homomorphisms of groups and the same coefficient homomorphisms. This also handles definitions and bundled structures: the data are first built at each finite stage, then the compatibility equations show that the family lies in the inverse limit. Consequently the coordinate calculation uniquely determines the completed object and verifies the required algebraic or topological property. 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.
□