CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra.lean
1import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Topology
2import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Functoriality
3import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Abstract
4import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation.Completed
5import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.UnitRepresentation
7/-
8PUBLIC_PAGE_SNAPSHOT
9generated_at: 2026-05-27T09:47:29+09:00
10lean_source: lean4/CompletedGroupAlgebra/ProfiniteModules/FiniteGroupAlgebra.lean
11translation_root: data/translation
12purpose: identifies the local data snapshot used to build pages/
13placement: after imports, never before imports
14-/
15/-!
16# Profinite module structure
18The 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.
19-/