CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit

4 sections | 4 files | 59 declarations

The completed group algebra is presented as an inverse limit of finite group algebras, together with canonical augmentation, augmentation ideal, finite-stage maps, functoriality, and profinite module universal properties.

Algebra

1 files | 36 declarations | 18 Theorem | 1 Definition | 17 Instance
The zero element is defined coordinatewise as the compatible family of zero elements at all finite stages.

CanonicalMap

1 files | 9 declarations | 7 Theorem | 2 Definition
The abstract group-algebra map onto an open-finite quotient stage is surjective.

System

1 files | 3 declarations | 1 Definition | 2 Abbreviation
The two-parameter inverse system \(K = (I, U) \mapsto (R/I)[G/U]\) for the kernel-neighborhood topology.

Topology

1 files | 11 declarations | 7 Theorem | 4 Instance
Each two-parameter finite quotient stage is a topological ring for its discrete topology.