ProCGroups.CompletedGroupAlgebra.Augmentation
This aggregate exports the \(C\)-indexed stage and canonical augmentations, the augmentation ideal, and functoriality of these constructions.
Imported by
AugmentationIdeal
This file defines the kernel of the canonical augmentation on the in-class completed group algebra, establishes the associated short exact sequence, and identifies the ideal thr...
CanonicalAugmentation
Compatible finite-stage augmentations assemble into the canonical augmentation of the in-class completed group algebra. This file proves its projection, coefficient-map, continu...
Functoriality
Maps of in-class completed group algebras commute with canonical augmentation. This file derives the corresponding comap and image formulas for augmentation ideals, including th...
StageAugmentation
This file defines augmentation on each in-class finite stage and proves its values on basis elements and compatibility with transition, coefficient-change, and functorial stage ...