ProCGroups.CompletedGroupAlgebra.Basic.InClass
This is the public aggregate for the completion indexed by a finite-group class \(C\). It exports the in-class quotient indices and stages, their inverse system, the opaque named carrier, its coefficient algebra, canonical bundled projections, and the inherited inverse-limit topology.
The API deliberately mirrors the all-finite aggregate: use completedGroupAlgebraProjectionInClass, completedGroupAlgebraInClass_ext, and completedGroupAlgebraInClassCompatibleFamilyEquiv instead of constructing or projecting the compatible-family subtype directly.
Imported by
Index
This module defines the reverse-ordered open normal subgroups whose quotients lie in a finite-group class \(C\), together with their finite quotient groups and canonical quotien...
LimitAlgebra
This module gives the \(C\)-indexed completion the same opaque-carrier API as the all-finite completion. Its inverse-limit representation is exchanged explicitly, while projecti...
Projection
This module bundles the canonical \(C\)-indexed finite-stage projection as ring, algebra, linear, and continuous linear maps. The underlying projection and compatibility theorem...
Stage
This module defines the \(C\)-indexed finite group-algebra stages, their transition and coefficient-change ring homomorphisms, and the compatibility identities used by the inver...
System
This module assembles the \(C\)-indexed stages into a topological inverse system and supplies the single `IsRingSystem` witness from which the completed carrier inherits its rin...
Topology
This module transports finite-stage topological structures through the named \(C\)-indexed inverse-limit carrier and records its compactness and separation properties.