Source: ProCGroups.CompletedGroupAlgebra.Basic.InClass.Topology
1import ProCGroups.CompletedGroupAlgebra.Basic.InClass.Projection
3/-!
4# Completed Group Algebra / Basic / Within a Class / Topology
6This module transports finite-stage topological structures through the named \(C\)-indexed
7inverse-limit carrier and records its compactness and separation properties.
8-/
10open scoped Topology
12namespace CompletedGroupAlgebra
14noncomputable section
16open ProCGroups
17open ProCGroups.ProC
18open ProCGroups.InverseSystems
20universe u v w
22variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
23variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
25local instance
26 (C : ProCGroups.FiniteGroupClass.{v})
27 (U : CompletedGroupAlgebraIndexInClass G C) :
28 Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
29 change Ring (CompletedGroupAlgebraStageInClass C R G U)
30 infer_instance
32local instance
33 (C : ProCGroups.FiniteGroupClass.{v})
34 (U : CompletedGroupAlgebraIndexInClass G C) :
35 Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
36 change Module R (CompletedGroupAlgebraStageInClass C R G U)
37 infer_instance
39/-- Each \(C\)-indexed finite stage is a topological ring. -/
40theorem completedGroupAlgebraStageInClass_isTopologicalRing
41 (C : ProCGroups.FiniteGroupClass.{v})
42 (U : CompletedGroupAlgebraIndexInClass G C) :
43 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
44 finite_completedGroupAlgebraQuotientInClass G C U
45 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
46 (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
47 IsTopologicalRing (CompletedGroupAlgebraStageInClass C R G U) := by
48 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
49 finite_completedGroupAlgebraQuotientInClass G C U
50 letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
51 (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
52 dsimp [completedGroupAlgebraSystemInClass, CompletedGroupAlgebraStageInClass]
53 exact finiteGroupAlgebra_isTopologicalRing R (CompletedGroupAlgebraQuotientInClass G C U)
55/--
56The inverse system of finite-stage group algebras inherits a ring structure from the compatible
57finite-stage rings.
58-/
59instance instIsTopologicalRingCompletedGroupAlgebraSystemInClassX
60 (C : ProCGroups.FiniteGroupClass.{v})
61 (U : CompletedGroupAlgebraIndexInClass G C) :
62 IsTopologicalRing ((completedGroupAlgebraSystemInClass C R G).X U) :=
63 completedGroupAlgebraStageInClass_isTopologicalRing (R := R) (G := G) C U
65/--
66The \(C\)-indexed completed group algebra inherits a ring structure from the compatible
67finite-stage rings.
68-/
69instance instIsTopologicalRingCompletedGroupAlgebraInClass
70 (C : ProCGroups.FiniteGroupClass.{v}) :
71 IsTopologicalRing (CompletedGroupAlgebraInClass C R G) := by
72 change IsTopologicalRing (completedGroupAlgebraSystemInClass C R G).inverseLimit
73 infer_instance
75/-- Scalar multiplication is continuous for the relevant inverse-limit topology. -/
76instance instContinuousSMulCompletedGroupAlgebraInClass
77 (C : ProCGroups.FiniteGroupClass.{v}) :
78 ContinuousSMul R (CompletedGroupAlgebraInClass C R G) := by
79 letI : ∀ U : CompletedGroupAlgebraIndexInClass G C,
80 ContinuousSMul R ((completedGroupAlgebraSystemInClass C R G).X U) :=
81 fun U => by
82 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
83 finite_completedGroupAlgebraQuotientInClass G C U
84 dsimp [completedGroupAlgebraSystemInClass, CompletedGroupAlgebraStageInClass]
85 exact finiteGroupAlgebra_continuousSMul R
86 (CompletedGroupAlgebraQuotientInClass G C U)
87 exact inferInstanceAs
88 (ContinuousSMul R (completedGroupAlgebraSystemInClass C R G).inverseLimit)
90/-- The coefficient-ring map into the \(C\)-indexed completed group algebra is continuous. -/
91theorem continuous_completedGroupAlgebraAlgebraMapInClass
92 (C : ProCGroups.FiniteGroupClass.{v}) :
93 Continuous (algebraMap R (CompletedGroupAlgebraInClass C R G)) := by
94 let S := completedGroupAlgebraSystemInClass C R G
95 letI : ∀ U, TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
96 fun U => (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
97 let π : ∀ U : CompletedGroupAlgebraIndexInClass G C,
98 R → CompletedGroupAlgebraStageInClass C R G U :=
99 fun U r => algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r
100 have hπ : ∀ U, Continuous (π U) := by
101 intro U
102 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
103 finite_completedGroupAlgebraQuotientInClass G C U
104 exact finiteGroupAlgebra_algebraMap_continuous R
105 (CompletedGroupAlgebraQuotientInClass G C U)
106 have hcompat : S.CompatibleMaps π := by
107 intro U V hUV
108 funext r
109 exact completedGroupAlgebraTransitionInClass_algebraMap
110 (R := R) (G := G) C hUV r
111 change Continuous (S.inverseLimitLift π hcompat)
112 exact S.continuous_inverseLimitLift π hπ hcompat
114/-- The \(C\)-indexed completed group algebra is compact for compact Hausdorff coefficients. -/
115theorem completedGroupAlgebraInClass_compactSpace
116 (C : ProCGroups.FiniteGroupClass.{v})
117 [CompactSpace R] [T2Space R] :
118 CompactSpace (CompletedGroupAlgebraInClass C R G) := by
119 let S := completedGroupAlgebraSystemInClass C R G
120 letI : ∀ U : CompletedGroupAlgebraIndexInClass G C, CompactSpace (S.X U) := fun U =>
121 by
122 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
123 finite_completedGroupAlgebraQuotientInClass G C U
124 dsimp [S, completedGroupAlgebraSystemInClass, CompletedGroupAlgebraStageInClass]
125 exact finiteGroupAlgebra_compactSpace R
126 (CompletedGroupAlgebraQuotientInClass G C U)
127 letI : ∀ U : CompletedGroupAlgebraIndexInClass G C, T2Space (S.X U) := fun U =>
128 by
129 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
130 finite_completedGroupAlgebraQuotientInClass G C U
131 dsimp [S, completedGroupAlgebraSystemInClass, CompletedGroupAlgebraStageInClass]
132 exact finiteGroupAlgebra_t2Space R
133 (CompletedGroupAlgebraQuotientInClass G C U)
134 change CompactSpace S.inverseLimit
135 infer_instance
137/-- The \(C\)-indexed completed group algebra is Hausdorff for Hausdorff coefficients. -/
138theorem completedGroupAlgebraInClass_t2Space
139 (C : ProCGroups.FiniteGroupClass.{v})
140 [T2Space R] :
141 T2Space (CompletedGroupAlgebraInClass C R G) := by
142 let S := completedGroupAlgebraSystemInClass C R G
143 letI : ∀ U : CompletedGroupAlgebraIndexInClass G C, T2Space (S.X U) := fun U =>
144 by
145 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
146 finite_completedGroupAlgebraQuotientInClass G C U
147 dsimp [S, completedGroupAlgebraSystemInClass, CompletedGroupAlgebraStageInClass]
148 exact finiteGroupAlgebra_t2Space R
149 (CompletedGroupAlgebraQuotientInClass G C U)
150 exact S.t2Space_inverseLimit
152/--
153The \(C\)-indexed completed group algebra is totally disconnected for totally disconnected
154coefficients.
155-/
156theorem completedGroupAlgebraInClass_totallyDisconnectedSpace
157 (C : ProCGroups.FiniteGroupClass.{v})
158 [TotallyDisconnectedSpace R] :
159 TotallyDisconnectedSpace (CompletedGroupAlgebraInClass C R G) := by
160 let S := completedGroupAlgebraSystemInClass C R G
161 letI : ∀ U : CompletedGroupAlgebraIndexInClass G C, TotallyDisconnectedSpace (S.X U) :=
162 fun U =>
163 by
164 letI : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
165 finite_completedGroupAlgebraQuotientInClass G C U
166 dsimp [S, completedGroupAlgebraSystemInClass, CompletedGroupAlgebraStageInClass]
167 exact finiteGroupAlgebra_totallyDisconnectedSpace R
168 (CompletedGroupAlgebraQuotientInClass G C U)
169 exact S.totallyDisconnectedSpace_inverseLimit
172end
174end CompletedGroupAlgebra