CompletedGroupAlgebra.UniversalProperty

4 sections | 4 files | 35 declarations

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

Basic

1 files | 11 declarations | 10 Theorem | 1 Definition

The concrete inverse-limit construction satisfies the universal-property specification for the completed group algebra.

FiniteQuotient

1 files | 7 declarations | 5 Theorem | 2 Definition

Finite-quotient construction used in Lemma 5.3.5(d): a map on one finite quotient \(G/U\) extends linearly and continuously from \(\widehat{R[G]}\).

OpenSubmoduleQuotient

1 files | 4 declarations | 3 Theorem | 1 Definition

The quotient-target form of the existence step in Lemma 5.3.5(d): after quotienting a profinite target module by an open submodule, the prescribed continuous map from \(G\) exte...

ProfiniteModule

1 files | 13 declarations | 10 Theorem | 3 Definition

The closed fiber in a profinite target determined by the quotient-valued extension modulo one open submodule.