ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic

5 sections | 5 files | 44 declarations

This aggregate exports the bundled definitions of profinite rings and modules, their open submodules and ideals, finite quotient separation, and generating sets converging to zero.

import

ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.OpenIdeals

Imported by

ProCGroups.CompletedGroupAlgebra.ProfiniteModules

Definitions

1 file | 12 declarations | 6 Definitions | 3 Structures | 3 Instances

This file defines profinite rings, commutative profinite coefficient rings, and profinite modules. It also states their free-extension, discreteness, and finite-index submodule-...

FiniteQuotients

1 file | 6 declarations | 5 Theorems | 1 Abbreviation

Open submodules of a profinite module have finite quotients and separate continuous linear maps. This file packages open submodules and supplies quotient-continuity and finite-r...

Generators

1 file | 11 declarations | 8 Theorems | 3 Definitions

This file defines sets and maps converging to zero through open submodules and relates them to one-point extensions and dense additive generation. Every profinite module is show...

OpenIdeals

1 file | 7 declarations | 5 Theorems | 2 Definitions

This file develops open-ideal bases at zero in profinite rings, proves their quotients finite, and derives the finite-open-ideal quotient basis and linear-topology properties.

OpenSubmodule

1 file | 8 declarations | 7 Theorems | 1 Definition

This file constructs open submodules inside identity neighborhoods using scalar multiples of open additive subgroups. It proves the resulting linear topology and the finiteness ...