ProCGroups.CompletedGroupAlgebra.UniversalProperty

4 sections | 4 files | 68 declarations

This aggregate exports canonical inverse-limit models and their lift constructions to finite, discrete, open-submodule quotient, and general profinite modules.

imports

Imported by

ProCGroups.CompletedGroupAlgebra

Basic

1 file | 52 declarations | 35 Theorems | 15 Definitions | 2 Structures

This module packages canonical completed-group-algebra models by their finite-stage cone and inverse-limit universal property, derives comparison equivalences, and develops the ...

FiniteQuotient

1 file | 9 declarations | 7 Theorems | 2 Definitions

Maps from the algebraic group algebra that factor through a finite stage extend uniquely from the completion. This file constructs those lifts, specializes them to discrete modu...

OpenSubmoduleQuotient

1 file | 4 declarations | 3 Theorems | 1 Definition

The finite-quotient universal property yields a unique continuous linear lift to the quotient of a profinite module by an open submodule. This file constructs the lift and recor...

ProfiniteModule

1 file | 3 declarations | 2 Theorems | 1 Definition

Compatible lifts to all open-submodule quotients are assembled by compactness into a continuous linear map to a profinite module. This file proves existence and uniqueness and a...