CompletedGroupAlgebra.AllFiniteAugmentation
This module develops completed group algebras through finite quotient stages, transition maps, coefficient change, augmentation, comparison maps, and inverse-limit topology.
AugmentationIdeal
The canonical augmentation ideal \(I_G\subseteq \widehat{R[G]}\) is the kernel of the completed augmentation \(\varepsilon:\widehat{R[G]}\to R\).
CanonicalAugmentation
The completed augmentation evaluated at a finite stage.
InClassComparison
Completed Group Algebra / All Finite Augmentation / Within a Class Comparison.
StageAugmentation
The augmentation map on a finite stage is the ring homomorphism \(R[G/U]\to R\) that sends every group-like basis element to \(1\).
TerminalIndex
The finite quotient index type is nonempty, witnessed by the terminal quotient or canonical base object.