ProCGroups.CompletedGroupAlgebra.Basic.AllFinite
This is the public aggregate for the all-finite completion \(\widehat{R[G]}\). It exports:
finite-quotient indices, stages, and transition maps; the opaque named carrier and its explicit compatible-family equivalence; the generic inverse-limit ring, module, and coefficient-algebra structures; canonical bundled finite-stage projections and their linear, algebra, and continuous forms; and the inverse-limit topological-ring, compactness, Hausdorff, and disconnectedness results.
Downstream code should use completedGroupAlgebraProjection, completedGroupAlgebra_ext, and completedGroupAlgebraCompatibleFamilyEquiv; the concrete compatible-family subtype is not a second public carrier.
Imported by
Carrier
This module defines the all-finite completed group algebra as a named inverse-limit carrier. Its compatible-family realization is available only through the explicit equivalence...
Index
This module defines the reverse-ordered finite-quotient indices for the all-finite completion, their quotient groups and quotient projections, and the mutually inverse conversio...
Projections
This module bundles the canonical all-finite stage projections and proves continuity of the coefficient map through the inverse-limit lifting property.
Ring
The carrier and its algebraic structures come from the single generic inverse-limit construction. This module adds the stagewise coefficient-change map and the coefficient algeb...
Stage
This module defines the finite group-algebra stages \(R[G/U]\), coefficient-change maps, quotient-transition ring homomorphisms, their compatibility laws, and the topological in...
Topology
This module transports the finite-stage topological ring and scalar-action structures through the single all-finite inverse limit, and records its compactness and separation pro...