Source: ProCGroups.CompletedGroupAlgebra
1import ProCGroups.CompletedGroupAlgebra.Basic
2import ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology
3import ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality
4import ProCGroups.CompletedGroupAlgebra.InClassFunctoriality
5import ProCGroups.CompletedGroupAlgebra.Augmentation
6import ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation
7import ProCGroups.CompletedGroupAlgebra.UniversalProperty
8import ProCGroups.CompletedGroupAlgebra.FunctorialityComposition
9import ProCGroups.CompletedGroupAlgebra.Separation
10import ProCGroups.CompletedGroupAlgebra.ProfiniteModules
12/-!
13# Completed group algebras
15Completed group algebras are constructed as inverse limits of finite-quotient group algebras.
16The library develops their additive, ring, and topological structures together with projections,
17augmentation maps and ideals, finite-stage functoriality, separation, and universal properties for
18profinite modules.
20The completed carriers are opaque; their compatible-family inverse limits are implementation
21models exposed through canonical projections, extensionality, and representation equivalences.
22`CanonicalCompletedGroupAlgebraModel` is the specification-level API: its inverse-limit universal
23property determines comparison, continuity, density, and uniqueness rather than storing parallel
24certificates.
26This file is the public aggregate for every maintained `CompletedGroupAlgebra` component.
27-/