CompletedGroupAlgebra/Basic/InClass/Index.lean
1import CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.UnitRepresentation
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/Basic/InClass/Index.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Class-Indexed Completed Group Algebras
14Finite-class-indexed inverse systems and inverse limits for completed group algebras.
15-/
17open scoped Topology
19namespace CompletedGroupAlgebra
21noncomputable section
23open ProCGroups
24open ProCGroups.ProC
25open ProCGroups.InverseSystems
27universe u v w
29variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31section InClass
33/-- The `C`-indexed open-normal quotient tower for a completed group algebra. The order is
34chosen so that larger indices give finer quotients. -/
35abbrev CompletedGroupAlgebraIndexInClass (C : ProCGroups.FiniteGroupClass.{v}) :=
36 OrderDual (OpenNormalSubgroupInClass C G)
38/-- The finite quotient `G/U` at one `C`-indexed stage. -/
39abbrev CompletedGroupAlgebraQuotientInClass (C : ProCGroups.FiniteGroupClass.{v})
40 (U : CompletedGroupAlgebraIndexInClass G C) : Type v :=
41 (openNormalSubgroupInClassSystem C G).X U
43/-- Quotients appearing in a finite-only class are finite. -/
45 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
46 (U : CompletedGroupAlgebraIndexInClass G C) :
47 Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
48 hC (OrderDual.ofDual U).2
50/-- The terminal `C`-indexed completed-group-algebra quotient, corresponding to `G/G`. -/
52 (C : ProCGroups.FiniteGroupClass.{v})
54 CompletedGroupAlgebraIndexInClass G C :=
55 OrderDual.toDual (OpenNormalSubgroupInClass.top (C := C) (G := G))
57omit [IsTopologicalGroup G] in
58/-- The terminal in-class completed-group-algebra index is below every in-class index. -/
60 (C : ProCGroups.FiniteGroupClass.{v})
62 (U : CompletedGroupAlgebraIndexInClass G C) :
63 terminalCompletedGroupAlgebraIndexInClass (G := G) C ≤ U := by
64 change ((OrderDual.ofDual U).1 : Subgroup G) ≤ (⊤ : Subgroup G)
65 exact le_top
67variable (R : Type u) [CommRing R]
69end InClass
71end