Source: ProCGroups.CompletedGroupAlgebra.UniversalProperty
1import ProCGroups.CompletedGroupAlgebra.UniversalProperty.Basic
2import ProCGroups.CompletedGroupAlgebra.UniversalProperty.FiniteQuotient
3import ProCGroups.CompletedGroupAlgebra.UniversalProperty.OpenSubmoduleQuotient
4import ProCGroups.CompletedGroupAlgebra.UniversalProperty.ProfiniteModule
6/-!
7# Universal properties of completed group algebras
9This aggregate exports canonical inverse-limit models and their lift constructions to finite,
10discrete, open-submodule quotient, and general profinite modules.
11-/