ProCGroups.CompletedGroupAlgebra.InClassFunctoriality

6 sections | 6 files | 49 declarations

This aggregate exports \(C\)-indexed functoriality from quotient-index comaps through completed ring and algebra maps, group-like elements, comparison results, and the resulting continuous unit representation.

import

ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.UnitRepresentation

Imported by

ProCGroups.CompletedGroupAlgebra

ComapIndex

1 file | 7 declarations | 5 Theorems | 2 Definitions

An open-normal quotient index on the target pulls back along a continuous group homomorphism to an index on the source. This file defines that comap, the induced finite quotient...

Comparison

1 file | 8 declarations | 8 Theorems

This file computes the canonical maps between all-finite and in-class completed group algebras on group-like elements and their differences from one. It also records the corresp...

GroupLike

1 file | 6 declarations | 5 Theorems | 1 Definition

This module constructs the \(C\)-indexed completed group-like map through the canonical dense map, and characterizes it by finite-stage projections, multiplication, and continuity.

Maps

1 file | 14 declarations | 12 Theorems | 2 Definitions

This module lifts hereditary \(C\)-indexed finite-stage maps to the named completed carrier and proves their algebraic, topological, and dense-subalgebra characterizations.

StageMaps

1 file | 9 declarations | 8 Theorems | 1 Definition

This file constructs the finite-stage group-algebra map induced by a continuous group homomorphism. It proves formulas on basis elements and scalars and compatibility with coeff...

UnitRepresentation

1 file | 5 declarations | 5 Theorems

This file studies the continuous group-like unit representation in an in-class completed group algebra. Its image spans densely, and scalar restriction along it equips profinite...