ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology

5 sections | 8 files | 178 declarations

This aggregate exports coefficient-and-group finite quotients, the associated kernel topology, the opaque two-parameter inverse limit, its dense canonical map, and the comparison with the all-finite completed group algebra.

imports
Imported by

CanonicalMaps

1 file | 37 declarations | 27 Theorems | 10 Definitions
This module constructs the canonical dense maps from the abstract group algebra to the \(C\)-indexed and all-finite named completions, together with their bundled ring, algebra,...

FiniteQuotients

1 file | 33 declarations | 25 Theorems | 7 Definitions | 1 Abbreviation
This file constructs the finite group-algebra stages obtained by quotienting both coefficients and the group. It develops their quotient maps, kernels, transition maps, basis fo...

OpenFiniteComparison

1 file | 54 declarations | 27 Theorems | 21 Definitions | 2 Structures | 4 Instances
This module compares the named fixed-coefficient completion with the named two-parameter open-finite quotient completion and studies the induced topology, injectivity, density, ...

OpenFiniteLimit

4 files | 25 declarations | 14 Theorems | 6 Definitions | 5 Instances
This module lifts the compatible open-finite quotient maps from the abstract group algebra to the named two-parameter completion, and proves its projection, continuity, and dens...

OpenFiniteQuotients

1 file | 29 declarations | 18 Theorems | 7 Definitions | 3 Abbreviations | 1 Instance
Open coefficient ideals and open normal group subgroups index a cofiltered system of finite group algebras. This file defines its stages, transitions, projections, and the kerne...