CompletedGroupAlgebra/OpenFiniteQuotientTopology/OpenFiniteComparison.lean
1import CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.CanonicalMap
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/OpenFiniteQuotientTopology/OpenFiniteComparison.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Completed group algebras
14The 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.
15-/
16open scoped Topology
18namespace CompletedGroupAlgebra
20noncomputable section
22open ProCGroups
23open ProCGroups.ProC
24open ProCGroups.InverseSystems
25open ProCGroups.Completion
27universe u v w
29variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
30variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
33/-- The canonical map from the fixed-coefficient completed group algebra `[[R G]]` to the
34two-parameter limit `lim_{I,U}(R/I)[G/U]`. -/
36 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
37 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
38 (x : Carrier R G) :
40 ⟨fun K => completedGroupAlgebraOpenFiniteQuotientProjection R G K x, by
41 intro K L hKL
42 exact congrFun
43 (congrArg DFunLike.coe
45 x⟩
47@[simp]
49 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
50 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
51 (K : CompletedGroupAlgebraOpenQuotientIndex R G) (x : Carrier R G) :
55 rfl
57@[simp]
59 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
60 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
61 (x : MonoidAlgebra R G) :
63 toCompletedGroupAlgebraOpenFiniteQuotientLimit R G x := by
64 apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
65 intro K
66 rfl
68/-- The canonical map `[[R G]] -> lim_{I,U}(R/I)[G/U]`, as a ring homomorphism. -/
70 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
71 [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
72 Carrier R G →+* CompletedGroupAlgebraOpenFiniteQuotientLimit R G where
73 toFun := completedGroupAlgebraToOpenFiniteQuotientLimit R G
74 map_zero' := by
75 apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
76 intro K
77 exact map_zero (completedGroupAlgebraOpenFiniteQuotientProjection R G K)
78 map_one' := by
79 apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
80 intro K
81 exact map_one (completedGroupAlgebraOpenFiniteQuotientProjection R G K)
82 map_add' x y := by
83 apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
84 intro K
85 exact map_add (completedGroupAlgebraOpenFiniteQuotientProjection R G K) x y
86 map_mul' x y := by
87 apply (completedGroupAlgebraOpenFiniteQuotientSystem R G).ext
88 intro K
89 exact map_mul (completedGroupAlgebraOpenFiniteQuotientProjection R G K) x y
91@[simp]
93 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
96 completedGroupAlgebraOpenFiniteQuotientProjection R G K := by
97 apply RingHom.ext
98 intro x
99 rfl
101@[simp]
104 (toCompletedGroupAlgebraRingHom R G) =
106 apply RingHom.ext
107 intro x
108 exact completedGroupAlgebraToOpenFiniteQuotientLimit_toCompletedGroupAlgebra (R := R) (G := G) x
110/-- The comparison map `[[RG]] -> lim_{I,U}(R/I)[G/U]` is continuous. -/
112 Continuous (completedGroupAlgebraToOpenFiniteQuotientLimit R G) := by
113 let A := Carrier R G
114 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
115 TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
116 fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
117 have hval : Continuous fun x : A =>
119 (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
120 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
121 change Continuous fun x : A =>
122 fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>
124 apply continuous_pi
125 intro K
126 exact continuous_completedGroupAlgebraOpenFiniteQuotientProjection (R := R) (G := G) K
127 exact Continuous.subtype_mk hval fun x =>
131 [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
132 DenseRange (completedGroupAlgebraToOpenFiniteQuotientLimit R G) := by
133 have hdense :
134 DenseRange
136 (toCompletedGroupAlgebra R G)) := by
137 simpa [Function.comp] using
138 denseRange_toCompletedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G)
139 exact DenseRange.of_comp hdense
141/-- The comparison map to the two-parameter kernel-neighborhood limit is injective when the
142coefficient ring is profinite. This is the completed-stage form of the kernel-intersection
143assertion in Lemma 5.3.5(a). -/
145 (hR : IsProfiniteRing R) :
146 Function.Injective (completedGroupAlgebraToOpenFiniteQuotientLimit R G) := by
147 intro x y hxy
148 apply (completedGroupAlgebraSystem R G).ext
149 intro U
150 apply Finsupp.ext
151 intro q
152 have hzero : ((completedGroupAlgebraProjection R G U x -
153 completedGroupAlgebraProjection R G U y) q) = 0 := by
154 apply profiniteRing_eq_zero_of_forall_openIdeal_quotient_eq_zero (R := R) hR
155 intro Iopen
156 let K : CompletedGroupAlgebraOpenQuotientIndex R G := (OrderDual.toDual Iopen, U)
157 have hcoord := congrArg
158 (fun z : CompletedGroupAlgebraOpenFiniteQuotientLimit R G =>
160 change completedGroupAlgebraStageCoeffQuotientMap R G Iopen.1 U
161 (completedGroupAlgebraProjection R G U x) =
162 completedGroupAlgebraStageCoeffQuotientMap R G Iopen.1 U
163 (completedGroupAlgebraProjection R G U y) at hcoord
164 have hdiff : completedGroupAlgebraStageCoeffQuotientMap R G Iopen.1 U
165 (completedGroupAlgebraProjection R G U x -
166 completedGroupAlgebraProjection R G U y) = 0 := by
167 rw [map_sub, hcoord, sub_self]
168 have hq := congrArg
169 (fun z : CompletedGroupAlgebraCoeffQuotientStage R G Iopen.1 U => z q) hdiff
171 MonoidAlgebra.mapRangeRingHom_apply] using hq
172 have hsub : (completedGroupAlgebraProjection R G U x) q -
173 (completedGroupAlgebraProjection R G U y) q = 0 := by
174 simpa using hzero
175 exact sub_eq_zero.mp hsub
177/-- The comparison map to the two-parameter kernel-neighborhood limit is onto for profinite
178coefficients: its dense image is compact, hence closed, in the Hausdorff two-parameter limit. -/
180 (hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
181 Function.Surjective (completedGroupAlgebraToOpenFiniteQuotientLimit R G) := by
182 letI : CompactSpace (Carrier R G) :=
183 completedGroupAlgebra_compactSpace (R := R) (G := G) hR
184 letI : T2Space (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
185 completedGroupAlgebraOpenFiniteQuotientLimit_t2Space (R := R) (G := G) hR
186 have hclosed : IsClosed (Set.range (completedGroupAlgebraToOpenFiniteQuotientLimit R G)) := by
187 exact (isCompact_range
188 (continuous_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G))).isClosed
189 have hdense :
190 closure (Set.range (completedGroupAlgebraToOpenFiniteQuotientLimit R G)) = Set.univ :=
191 (denseRange_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G)).closure_range
192 have hrange : Set.range (completedGroupAlgebraToOpenFiniteQuotientLimit R G) = Set.univ := by
193 rwa [hclosed.closure_eq] at hdense
194 intro y
195 have hy : y ∈ Set.range (completedGroupAlgebraToOpenFiniteQuotientLimit R G) := by
196 rw [hrange]
197 exact Set.mem_univ y
198 simpa using hy
200/-- The comparison map `[[RG]] -> lim_{I,U}(R/I)[G/U]` is a bijection under the profinite
201coefficient hypothesis. -/
203 (hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
204 Function.Bijective (completedGroupAlgebraToOpenFiniteQuotientLimit R G) :=
205 ⟨injective_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G) hR,
206 surjective_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G) hR⟩
208/-- RZ §5.3 comparison: the fixed-coefficient inverse-limit model `[[RG]]` is ring-isomorphic to
209the two-parameter kernel-neighborhood limit `lim_{I,U}(R/I)[G/U]` for profinite coefficient rings. -/
211 (hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
212 Carrier R G ≃+* CompletedGroupAlgebraOpenFiniteQuotientLimit R G :=
213 RingEquiv.ofBijective (completedGroupAlgebraToOpenFiniteQuotientLimitRingHom R G)
214 (bijective_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G) hR)
216@[simp]
218 (hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)]
219 (x : Carrier R G) :
220 completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv (R := R) (G := G) hR x =
222 rfl
224/-- The same comparison as a homeomorphism of the underlying profinite spaces. -/
226 (hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
227 Carrier R G ≃ₜ CompletedGroupAlgebraOpenFiniteQuotientLimit R G := by
228 letI : CompactSpace (Carrier R G) :=
229 completedGroupAlgebra_compactSpace (R := R) (G := G) hR
230 letI : T2Space (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
231 completedGroupAlgebraOpenFiniteQuotientLimit_t2Space (R := R) (G := G) hR
232 let e : Carrier R G ≃ CompletedGroupAlgebraOpenFiniteQuotientLimit R G :=
233 (completedGroupAlgebraOpenFiniteQuotientLimitRingEquiv (R := R) (G := G) hR).toEquiv
234 exact Continuous.homeoOfEquivCompactToT2 (f := e) (by
235 change Continuous (completedGroupAlgebraToOpenFiniteQuotientLimit R G)
236 exact continuous_completedGroupAlgebraToOpenFiniteQuotientLimit (R := R) (G := G))
238/-- Lemma 5.3.5(c), fixed-coefficient inverse-limit form: the abstract group algebra maps
239dense into the completed group algebra. -/
240theorem denseRange_toCompletedGroupAlgebra (hG : ProCGroups.IsProfiniteGroup G) :
241 DenseRange (toCompletedGroupAlgebra R G) := by
242 let S := completedGroupAlgebraSystem R G
243 letI : TopologicalSpace (MonoidAlgebra R G) := ⊥
244 have hProC : IsProCGroup ProCGroups.FiniteGroupClass.allFinite G :=
245 (isProC_allFinite_iff_isProfiniteGroup (G := G)).2 hG
246 letI : Nonempty (OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G) :=
247 IsProCGroup.openNormalSubgroupInClass_nonempty hProC
248 letI : Nonempty (CompletedGroupAlgebraIndex G) := inferInstance
249 have hdir : Directed (α := CompletedGroupAlgebraIndex G) (· ≤ ·) fun U => U :=
251 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) ProCGroups.FiniteGroupClass.allFinite_formation
252 have hdense :
253 DenseRange
254 (S.inverseLimitLift (fun U : CompletedGroupAlgebraIndex G => completedGroupAlgebraStageMap R G U)
255 (completedGroupAlgebraStageMap_compatibleMaps (R := R) (G := G))) :=
256 S.denseRange_lift
257 (fun U : CompletedGroupAlgebraIndex G => completedGroupAlgebraStageMap R G U)
258 (completedGroupAlgebraStageMap_compatibleMaps (R := R) (G := G))
259 (fun U => completedGroupAlgebraStageMap_surjective (R := R) (G := G) U)
260 hdir
261 simpa [S, toCompletedGroupAlgebra] using hdense
263theorem denseRange_toCompletedGroupAlgebraRingHom (hG : ProCGroups.IsProfiniteGroup G) :
264 DenseRange (toCompletedGroupAlgebraRingHom R G) := by
265 simpa [toCompletedGroupAlgebraRingHom] using
266 denseRange_toCompletedGroupAlgebra (R := R) (G := G) hG
268/-- The completion topology on the abstract group algebra, induced by the canonical map into
269`[[R G]]`; below it is identified with the kernel-neighborhood topology generated by the maps
270`R[G] -> (R/I)[G/U]`. -/
271def completedGroupAlgebraNaturalTopology (R : Type u) (G : Type v) [CommRing R]
272 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
273 [IsTopologicalGroup G] :
274 TopologicalSpace (MonoidAlgebra R G) :=
275 TopologicalSpace.induced (toCompletedGroupAlgebra R G) inferInstance
278 letI : TopologicalSpace (MonoidAlgebra R G) :=
280 Continuous (toCompletedGroupAlgebraRingHom R G) := by
281 letI : TopologicalSpace (MonoidAlgebra R G) :=
283 change Continuous (toCompletedGroupAlgebra R G)
284 exact (continuous_induced_dom : Continuous (toCompletedGroupAlgebra R G))
286/-- The canonical map as a continuous `R`-linear map for the topology induced from `[[RG]]`. -/
288 letI : TopologicalSpace (MonoidAlgebra R G) :=
290 MonoidAlgebra R G →L[R] Carrier R G := by
291 letI : TopologicalSpace (MonoidAlgebra R G) :=
293 exact
294 { toLinearMap := toCompletedGroupAlgebraLinearMap R G
295 cont := continuous_toCompletedGroupAlgebraRingHom_naturalTopology (R := R) (G := G) }
297omit [IsTopologicalRing R] in
298/-- The kernel-neighborhood topology is exactly the topology induced by the canonical map from
299`R[G]` to the two-parameter kernel-neighborhood limit. -/
302 TopologicalSpace.induced (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G) inferInstance := by
303 let S := completedGroupAlgebraOpenFiniteQuotientSystem R G
304 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
305 TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
306 fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
307 change TopologicalSpace.induced (groupAlgebraOpenFiniteQuotientProductMap R G) inferInstance =
308 TopologicalSpace.induced (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G)
309 (TopologicalSpace.induced (fun z : S.inverseLimit => z.1) inferInstance)
310 rw [induced_compose]
311 rfl
313/-- Under the profinite coefficient hypothesis, the topology on `R[G]` induced from `[[RG]]`
314agrees with the topology induced by the two-parameter kernel-neighborhood limit. -/
316 (hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
318 TopologicalSpace.induced (toCompletedGroupAlgebraOpenFiniteQuotientLimit R G) inferInstance := by
319 let e := completedGroupAlgebraOpenFiniteQuotientLimitHomeomorph (R := R) (G := G) hR
320 have hcomp : e ∘ toCompletedGroupAlgebra R G =
322 funext x
324 (R := R) (G := G) x
326 rw [e.isInducing.eq_induced]
327 rw [induced_compose]
328 rw [hcomp]
330/-- RZ §5.3 natural topology comparison: the topology on the abstract group algebra induced from
331`[[RG]]` is the kernel-neighborhood topology generated by the maps `R[G] -> (R/I)[G/U]`. -/
333 (hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
337 (R := R) (G := G) hR,
338 groupAlgebraOpenFiniteQuotientKernelTopology_eq_induced_toLimit (R := R) (G := G)]
340/-- The canonical map `R[G] -> [[RG]]` is continuous for the kernel-neighborhood topology on
341`R[G]`. -/
343 (hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
344 letI : TopologicalSpace (MonoidAlgebra R G) :=
346 Continuous (toCompletedGroupAlgebraRingHom R G) := by
347 let τnat := completedGroupAlgebraNaturalTopology R G
348 let τker := groupAlgebraOpenFiniteQuotientKernelTopology R G
349 have hτ : τnat = τker :=
351 (R := R) (G := G) hR
352 change @Continuous (MonoidAlgebra R G) (Carrier R G)
353 τker inferInstance (toCompletedGroupAlgebraRingHom R G)
354 rw [← hτ]
355 exact continuous_toCompletedGroupAlgebraRingHom_naturalTopology (R := R) (G := G)
357/-- The canonical map as a continuous `R`-linear map for the kernel-neighborhood topology. -/
359 (hR : IsProfiniteRing R) [Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G)] :
360 letI : TopologicalSpace (MonoidAlgebra R G) :=
362 MonoidAlgebra R G →L[R] Carrier R G := by
363 letI : TopologicalSpace (MonoidAlgebra R G) :=
365 exact
366 { toLinearMap := toCompletedGroupAlgebraLinearMap R G
368 (R := R) (G := G) hR }
370/-- Lemma 5.3.5(b/c), kernel-topology data form: for profinite `R` and profinite `G`, the
371concrete inverse-limit `[[RG]]` is profinite and receives a dense continuous map from `R[G]`
372when `R[G]` carries the kernel-neighborhood topology. -/
374 (hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :
375 letI : TopologicalSpace (MonoidAlgebra R G) :=
377 IsProfiniteRing (Carrier R G) ∧
378 DenseRange (toCompletedGroupAlgebraRingHom R G) ∧
379 Continuous (toCompletedGroupAlgebraRingHom R G) := by
380 have hProC : IsProCGroup ProCGroups.FiniteGroupClass.allFinite G :=
381 (isProC_allFinite_iff_isProfiniteGroup (G := G)).2 hG
382 letI : Nonempty (OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G) :=
383 IsProCGroup.openNormalSubgroupInClass_nonempty hProC
384 letI : Nonempty (CompletedGroupAlgebraIndex G) := inferInstance
385 letI : Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G) := inferInstance
386 letI : TopologicalSpace (MonoidAlgebra R G) :=
388 exact ⟨completedGroupAlgebra_isProfiniteRing (R := R) (G := G) hR,
389 denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG,
390 continuous_toCompletedGroupAlgebraRingHom_kernelTopology (R := R) (G := G) hR⟩
392/-- Linear-module form of the kernel-topology completion data for Lemma 5.3.5. -/
394 (hR : IsProfiniteRing R) (hG : ProCGroups.IsProfiniteGroup G) :
395 letI : TopologicalSpace (MonoidAlgebra R G) :=
397 IsProfiniteModule R (Carrier R G) ∧
398 DenseRange (toCompletedGroupAlgebraLinearMap R G) ∧
399 Continuous (toCompletedGroupAlgebraLinearMap R G) := by
400 have hProC : IsProCGroup ProCGroups.FiniteGroupClass.allFinite G :=
401 (isProC_allFinite_iff_isProfiniteGroup (G := G)).2 hG
402 letI : Nonempty (OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G) :=
403 IsProCGroup.openNormalSubgroupInClass_nonempty hProC
404 letI : Nonempty (CompletedGroupAlgebraIndex G) := inferInstance
405 letI : Nonempty (CompletedGroupAlgebraOpenQuotientIndex R G) := inferInstance
406 letI : TopologicalSpace (MonoidAlgebra R G) :=
408 refine ⟨completedGroupAlgebra_isProfiniteModule (R := R) (G := G) hR, ?_, ?_⟩
409 · change DenseRange (toCompletedGroupAlgebra R G)
410 simpa [toCompletedGroupAlgebraRingHom] using
411 denseRange_toCompletedGroupAlgebraRingHom (R := R) (G := G) hG
412 · change Continuous (toCompletedGroupAlgebra R G)
413 exact continuous_toCompletedGroupAlgebraRingHom_kernelTopology (R := R) (G := G) hR
414end