CompletedGroupAlgebra.Basic

3 sections | 15 files | 184 declarations

This module develops completed group algebras through finite quotient stages, transition maps, coefficient change, augmentation, comparison maps, and inverse-limit topology.

AllFinite

7 files | 95 declarations | 44 Theorem | 17 Definition | 5 Abbreviation | 29 Instance
The carrier of the completed group algebra is the inverse limit \(\widehat{R[G]}=\varprojlim_U R[G/U]\) over the open-normal finite quotients of \(G\).

ClassComparison

1 files | 32 declarations | 22 Theorem | 10 Definition
The projection from the all-finite completed group algebra to a stage indexed by a finite quotient class \(C\).

InClass

7 files | 57 declarations | 31 Theorem | 11 Definition | 5 Abbreviation | 10 Instance
Completed Group Algebra / Basic / Within a Class.