ProCGroups.CompletedGroupAlgebra

10 sections | 71 files | 697 declarations

Completed group algebras are constructed as inverse limits of finite-quotient group algebras. The library develops their additive, ring, and topological structures together with projections, augmentation maps and ideals, finite-stage functoriality, separation, and universal properties for profinite modules.

The completed carriers are opaque; their compatible-family inverse limits are implementation models exposed through canonical projections, extensionality, and representation equivalences. CanonicalCompletedGroupAlgebraModel is the specification-level API: its inverse-limit universal property determines comparison, continuity, density, and uniqueness rather than storing parallel certificates.

This file is the public aggregate for every maintained CompletedGroupAlgebra component.

imports

Imported by

ProCGroups

AllFiniteAugmentation

6 files | 37 declarations | 32 Theorems | 4 Definitions | 1 Instance

This aggregate exports terminal-index and finite-stage augmentations, the canonical all-finite augmentation, its comparison with the \(C\)-indexed augmentation, and the complete...

AllFiniteFunctoriality

7 files | 37 declarations | 31 Theorems | 6 Definitions

This module constructs the inverse-image finite quotient attached to a continuous group homomorphism and the induced quotient homomorphism. It is the index-level input for all-f...

Augmentation

5 files | 30 declarations | 26 Theorems | 4 Definitions

This aggregate exports the \(C\)-indexed stage and canonical augmentations, the augmentation ideal, and functoriality of these constructions.

Basic

16 files | 137 declarations | 70 Theorems | 40 Definitions | 6 Abbreviations | 21 Instances

This aggregate exports both opaque completed-group-algebra carriers, their finite-stage systems, bundled projections and topological structures, and the canonical comparison equ...

FunctorialityComposition

1 file | 2 declarations | 2 Theorems

This module records compatibility of completed group algebra functoriality with composition.

InClassFunctoriality

7 files | 49 declarations | 43 Theorems | 6 Definitions

This aggregate exports \(C\)-indexed functoriality from quotient-index comaps through completed ring and algebra maps, group-like elements, comparison results, and the resulting...

OpenFiniteQuotientTopology

9 files | 178 declarations | 111 Theorems | 51 Definitions | 4 Abbreviations | 2 Structures | 10 Instances

This module constructs the canonical dense maps from the abstract group algebra to the \(C\)-indexed and all-finite named completions, together with their bundled ring, algebra,...

ProfiniteModules

14 files | 140 declarations | 100 Theorems | 33 Definitions | 1 Abbreviation | 3 Structures | 3 Instances

This aggregate exports the bundled definitions of profinite rings and modules, their open submodules and ideals, finite quotient separation, and generating sets converging to zero.

Separation

1 file | 19 declarations | 19 Theorems

This module contains separation lemmas for completed group algebras using finite quotients.

UniversalProperty

5 files | 68 declarations | 47 Theorems | 19 Definitions | 2 Structures

This aggregate exports canonical inverse-limit models and their lift constructions to finite, discrete, open-submodule quotient, and general profinite modules.