ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit
This aggregate exports the two-parameter inverse limit \(\varprojlim_{I,U}(R/I)[G/U]\), its opaque named carrier, canonical bundled quotient projections, inherited topological-ring structure, and the dense canonical map from \(R[G]\).
The carrier's compatible-family realization is available only through completedGroupAlgebraOpenFiniteQuotientCompatibleFamilyEquiv; ordinary consumers should use completedGroupAlgebraOpenFiniteQuotientLimitProjection and completedGroupAlgebraOpenFiniteQuotientLimit_ext.
CanonicalMap
This module lifts the compatible open-finite quotient maps from the abstract group algebra to the named two-parameter completion, and proves its projection, continuity, and dens...
System
This module defines the two-parameter open-finite quotient system and its named inverse-limit carrier. The compatible-family representation is exposed only by an explicit equiva...
Topology
This module transports the discrete topological-ring structures of the open-finite quotient stages through the single two-parameter inverse limit, and records compactness and se...