CompletedGroupAlgebra.Basic.AllFinite

6 sections | 6 files | 95 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.

Additive

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\).

Index

The index set for the Section 5.3 completed group algebra tower, ordered so that larger indices give finer finite quotients.

Projections

1 files | 5 declarations | 1 Theorem | 4 Definition

The coefficient-ring map \(R \to \widehat{R[G]}\) is continuous.

Ring

1 files | 23 declarations | 12 Theorem | 2 Definition | 9 Instance

The unit of the completed group algebra is defined coordinatewise through the finite-stage units.

Stage

1 files | 13 declarations | 9 Theorem | 3 Definition | 1 Abbreviation

The finite-stage group algebra \(R[G/U]\) from Ribes--Zalesskii, Section 5.3.

Topology

1 files | 13 declarations | 8 Theorem | 5 Instance

Each finite stage \(R[G/U]\) is a topological ring for its product topology.