ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation
This aggregate exports terminal-index and finite-stage augmentations, the canonical all-finite augmentation, its comparison with the \(C\)-indexed augmentation, and the completed augmentation ideal.
Imported by
AugmentationIdeal
This file defines the kernel of the canonical augmentation on the all-finite completed group algebra, packages its short exact sequence, and proves comparison and functoriality ...
CanonicalAugmentation
This module defines the all-finite canonical augmentation as the composition of a terminal finite-stage augmentation with the canonical bundled projection, and proves that it ca...
InClassComparison
The canonical comparison maps between the all-finite and in-class completions commute with their augmentations. This file records both directions of that compatibility.
StageAugmentation
This file defines augmentation on each finite coefficient-and-group stage of the all-finite system and proves its formulas on basis elements and compatibility with transition, c...
TerminalIndex
This file constructs a canonical inhabitant of the open-quotient index used by the all-finite completed group algebra, ensuring that its inverse system is nonempty.