CompletedGroupAlgebra/ProfiniteModules.lean
1import CompletedGroupAlgebra.ProfiniteModules.Basic.OpenIdeals
2import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Topology
3import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Functoriality
4import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Abstract
5import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Completed
6import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.UnitRepresentation
8/-
9PUBLIC_PAGE_SNAPSHOT
10generated_at: 2026-05-27T09:47:29+09:00
11lean_source: lean4/CompletedGroupAlgebra/ProfiniteModules.lean
12translation_root: data/translation
13purpose: identifies the local data snapshot used to build pages/
14placement: after imports, never before imports
15-/
16/-!
17# Profinite module structure
19The completed group algebra is presented as an inverse limit of finite group algebras, together with canonical augmentation, augmentation ideal, finite-stage maps, functoriality, and profinite module universal properties.
20-/