ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality

6 sections | 6 files | 37 declarations

This aggregate exports functoriality of the all-finite completed group algebra for continuous group homomorphisms: inverse-image quotient indices, finite-stage and completed algebra maps, group-like compatibility, surjectivity, and naturality of the comparison with \(C\)-indexed completions.

imports

Imported by

ProCGroups.CompletedGroupAlgebra

Comap

1 file | 6 declarations | 4 Theorems | 2 Definitions

This module constructs the inverse-image finite quotient attached to a continuous group homomorphism and the induced quotient homomorphism. It is the index-level input for all-f...

GroupLike

1 file | 8 declarations | 7 Theorems | 1 Definition

This module records the action of the all-finite functorial map on canonical group-like elements.

InClassNaturality

1 file | 9 declarations | 9 Theorems

This module proves that the comparison between the all-finite and \(C\)-indexed completions is natural for continuous group homomorphisms, in ring-, algebra-, and equivalence-va...

Map

1 file | 6 declarations | 4 Theorems | 2 Definitions

This module lifts the functorial finite-stage maps to the named all-finite completed carrier and proves their algebraic, topological, and dense-subalgebra characterizations.

StageMap

1 file | 7 declarations | 6 Theorems | 1 Definition

This module lifts the quotient homomorphism from `Comap` to finite group algebras and proves its continuity, transition compatibility, and compatibility with the canonical dense...

Surjectivity

1 file | 1 declaration | 1 Theorem

A surjective continuous group homomorphism induces a surjective map of all-finite completed group algebras. The proof combines finite-stage surjectivity with the inverse-limit l...