CompletedGroupAlgebra/Basic/InClass/Topology.lean
1import CompletedGroupAlgebra.Basic.InClass.Projection
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/Basic/InClass/Topology.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]
30variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
33/-- Each `C`-indexed finite stage is a topological ring. -/
35 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
36 (U : CompletedGroupAlgebraIndexInClass G C) :
37 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
39 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
40 (completedGroupAlgebraSystemInClass C hC R G).topologicalSpace U
41 IsTopologicalRing (CompletedGroupAlgebraStageInClass C R G U) := by
42 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
44 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
45 (completedGroupAlgebraSystemInClass C hC R G).topologicalSpace U
46 dsimp [completedGroupAlgebraSystemInClass, CompletedGroupAlgebraStageInClass]
47 exact finiteGroupAlgebra_isTopologicalRing R (CompletedGroupAlgebraQuotientInClass G C U)
50 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
51 (U : CompletedGroupAlgebraIndexInClass G C) :
52 IsTopologicalRing ((completedGroupAlgebraSystemInClass C hC R G).X U) :=
53 completedGroupAlgebraStageInClass_isTopologicalRing (R := R) (G := G) C hC U
56 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
57 IsTopologicalRing (CompletedGroupAlgebraInClass C hC R G) := by
58 change IsTopologicalRing (completedGroupAlgebraSystemInClass C hC R G).inverseLimit
59 infer_instance
62 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
63 ContinuousSMul R (CompletedGroupAlgebraInClass C hC R G) where
64 continuous_smul := by
65 let A := CompletedGroupAlgebraInClass C hC R G
66 let S := completedGroupAlgebraSystemInClass C hC R G
67 letI : ∀ U : CompletedGroupAlgebraIndexInClass G C,
68 TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
69 fun U => S.topologicalSpace U
70 have hval : Continuous fun p : R × A =>
71 fun U : CompletedGroupAlgebraIndexInClass G C =>
72 (show CompletedGroupAlgebraStageInClass C R G U from (p.1 • p.2).1 U) := by
73 change Continuous fun p : R × A =>
74 fun U : CompletedGroupAlgebraIndexInClass G C =>
75 p.1 • completedGroupAlgebraProjectionInClass C hC R G U p.2
76 apply continuous_pi
77 intro U
78 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
80 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
81 S.topologicalSpace U
82 letI : ContinuousSMul R (CompletedGroupAlgebraStageInClass C R G U) :=
83 finiteGroupAlgebra_continuousSMul R (CompletedGroupAlgebraQuotientInClass G C U)
84 exact continuous_fst.smul ((S.continuous_projection U).comp continuous_snd)
85 exact Continuous.subtype_mk hval fun p => (p.1 • p.2).2
87/-- The coefficient-ring map into the `C`-indexed completed group algebra is continuous. -/
89 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
90 Continuous (algebraMap R (CompletedGroupAlgebraInClass C hC R G)) := by
91 let S := completedGroupAlgebraSystemInClass C hC R G
92 letI : ∀ U : CompletedGroupAlgebraIndexInClass G C,
93 TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
94 fun U => S.topologicalSpace U
95 have hval : Continuous fun r : R =>
96 fun U : CompletedGroupAlgebraIndexInClass G C =>
97 (show CompletedGroupAlgebraStageInClass C R G U from
98 (algebraMap R (CompletedGroupAlgebraInClass C hC R G) r).1 U) := by
99 change Continuous fun r : R =>
100 fun U : CompletedGroupAlgebraIndexInClass G C =>
101 algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r
102 apply continuous_pi
103 intro U
104 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
106 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
107 S.topologicalSpace U
108 exact finiteGroupAlgebra_algebraMap_continuous R (CompletedGroupAlgebraQuotientInClass G C U)
109 exact Continuous.subtype_mk hval fun r =>
110 (algebraMap R (CompletedGroupAlgebraInClass C hC R G) r).2
112/-- Each `C`-indexed finite stage is a profinite ring when the coefficient ring is profinite. -/
114 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
115 (hR : IsProfiniteRing R) (U : CompletedGroupAlgebraIndexInClass G C) :
116 IsProfiniteRing ((completedGroupAlgebraSystemInClass C hC R G).X U) := by
117 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
119 dsimp [completedGroupAlgebraSystemInClass, CompletedGroupAlgebraStageInClass]
120 exact finiteGroupAlgebra_isProfiniteRing R (CompletedGroupAlgebraQuotientInClass G C U) hR
122/-- The `C`-indexed completed group algebra is compact when the coefficient ring is profinite. -/
124 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
125 (hR : IsProfiniteRing R) :
126 CompactSpace (CompletedGroupAlgebraInClass C hC R G) := by
127 let S := completedGroupAlgebraSystemInClass C hC R G
128 letI : ∀ U : CompletedGroupAlgebraIndexInClass G C, CompactSpace (S.X U) := fun U =>
129 (completedGroupAlgebraStageInClass_isProfiniteRing (R := R) (G := G) C hC hR U).2.1
130 letI : ∀ U : CompletedGroupAlgebraIndexInClass G C, T2Space (S.X U) := fun U =>
131 (completedGroupAlgebraStageInClass_isProfiniteRing (R := R) (G := G) C hC hR U).2.2.1
132 change CompactSpace S.inverseLimit
133 infer_instance
135/-- The `C`-indexed completed group algebra is Hausdorff when the coefficient ring is profinite. -/
137 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
138 (hR : IsProfiniteRing R) :
139 T2Space (CompletedGroupAlgebraInClass C hC R G) := by
140 let S := completedGroupAlgebraSystemInClass C hC R G
141 letI : ∀ U : CompletedGroupAlgebraIndexInClass G C, T2Space (S.X U) := fun U =>
142 (completedGroupAlgebraStageInClass_isProfiniteRing (R := R) (G := G) C hC hR U).2.2.1
143 exact S.t2Space_inverseLimit
145/-- The `C`-indexed completed group algebra is totally disconnected for profinite coefficients. -/
147 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
148 (hR : IsProfiniteRing R) :
149 TotallyDisconnectedSpace (CompletedGroupAlgebraInClass C hC R G) := by
150 let S := completedGroupAlgebraSystemInClass C hC R G
151 letI : ∀ U : CompletedGroupAlgebraIndexInClass G C, TotallyDisconnectedSpace (S.X U) :=
152 fun U =>
153 (completedGroupAlgebraStageInClass_isProfiniteRing (R := R) (G := G) C hC hR U).2.2.2
154 exact S.totallyDisconnectedSpace_inverseLimit
156/-- The `C`-indexed completed group algebra is profinite when the coefficient ring is profinite. -/
158 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
159 (hR : IsProfiniteRing R) :
160 IsProfiniteRing (CompletedGroupAlgebraInClass C hC R G) := by
161 letI : IsTopologicalRing (CompletedGroupAlgebraInClass C hC R G) :=
162 instIsTopologicalRingCompletedGroupAlgebraInClass (R := R) (G := G) C hC
163 letI : CompactSpace (CompletedGroupAlgebraInClass C hC R G) :=
164 completedGroupAlgebraInClass_compactSpace (R := R) (G := G) C hC hR
165 letI : T2Space (CompletedGroupAlgebraInClass C hC R G) :=
166 completedGroupAlgebraInClass_t2Space (R := R) (G := G) C hC hR
167 letI : TotallyDisconnectedSpace (CompletedGroupAlgebraInClass C hC R G) :=
168 completedGroupAlgebraInClass_totallyDisconnectedSpace (R := R) (G := G) C hC hR
169 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩
171/-- The `C`-indexed completed group algebra is a profinite module over its coefficient ring. -/
173 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
174 (hR : IsProfiniteRing R) :
175 IsProfiniteModule R (CompletedGroupAlgebraInClass C hC R G) := by
176 letI : IsTopologicalRing R := hR.1
177 letI : IsTopologicalRing (CompletedGroupAlgebraInClass C hC R G) :=
178 instIsTopologicalRingCompletedGroupAlgebraInClass (R := R) (G := G) C hC
179 letI : IsTopologicalAddGroup (CompletedGroupAlgebraInClass C hC R G) := inferInstance
180 letI : ContinuousSMul R (CompletedGroupAlgebraInClass C hC R G) :=
181 instContinuousSMulCompletedGroupAlgebraInClass (R := R) (G := G) C hC
182 letI : CompactSpace (CompletedGroupAlgebraInClass C hC R G) :=
183 completedGroupAlgebraInClass_compactSpace (R := R) (G := G) C hC hR
184 letI : T2Space (CompletedGroupAlgebraInClass C hC R G) :=
185 completedGroupAlgebraInClass_t2Space (R := R) (G := G) C hC hR
186 letI : TotallyDisconnectedSpace (CompletedGroupAlgebraInClass C hC R G) :=
187 completedGroupAlgebraInClass_totallyDisconnectedSpace (R := R) (G := G) C hC hR
188 exact ⟨hR, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance⟩
191end