Source: ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit
1import ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.CanonicalMap
3/-!
4# Completed Group Algebra / Open Finite Quotient Topology / Open Finite Limit
6This aggregate exports the two-parameter inverse limit
7\(\varprojlim_{I,U}(R/I)[G/U]\), its opaque named carrier, canonical bundled quotient
8projections, inherited topological-ring structure, and the dense canonical map from \(R[G]\).
10The carrier's compatible-family realization is available only through
11`completedGroupAlgebraOpenFiniteQuotientCompatibleFamilyEquiv`; ordinary consumers should use
12`completedGroupAlgebraOpenFiniteQuotientLimitProjection` and
13`completedGroupAlgebraOpenFiniteQuotientLimit_ext`.
14-/