CompletedGroupAlgebra/OpenFiniteQuotientTopology/CanonicalMaps.lean
1import CompletedGroupAlgebra.Basic.ClassComparison
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/OpenFiniteQuotientTopology/CanonicalMaps.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 quotient map from the abstract group algebra `R[G]` to one `C`-indexed finite stage. -/
34def completedGroupAlgebraStageMapInClass
35 (C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]
36 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
37 (U : CompletedGroupAlgebraIndexInClass G C) :
38 MonoidAlgebra R G →+* CompletedGroupAlgebraStageInClass C R G U :=
39 MonoidAlgebra.mapDomainRingHom R
40 (openNormalSubgroupInClassProj (C := C) (G := G) U)
42omit [TopologicalSpace R] [IsTopologicalRing R] in
43@[simp]
44theorem completedGroupAlgebraStageMapInClass_of
45 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
46 (g : G) :
47 completedGroupAlgebraStageMapInClass C R G U (MonoidAlgebra.of R G g) =
48 MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1 := by
49 classical
50 simp only [completedGroupAlgebraStageMapInClass, MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk,
51 OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
52 rfl
54omit [TopologicalSpace R] [IsTopologicalRing R] in
56 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
57 (g : G) (r : R) :
58 completedGroupAlgebraStageMapInClass C R G U (MonoidAlgebra.single g r) =
59 MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) r := by
60 classical
61 simp only [completedGroupAlgebraStageMapInClass, MonoidAlgebra.single, MonoidAlgebra.mapDomainRingHom_apply,
62 Finsupp.mapDomain_single]
63 rfl
65omit [TopologicalSpace R] [IsTopologicalRing R] in
67 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
68 (r : R) (x : MonoidAlgebra R G) :
69 completedGroupAlgebraStageMapInClass C R G U (r • x) =
70 r • completedGroupAlgebraStageMapInClass C R G U x := by
72 congr 1
73 simp only [completedGroupAlgebraStageMapInClass, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,
74 RingHom.coe_id, Function.comp_apply, id_eq, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, map_one]
76omit [TopologicalSpace R] [IsTopologicalRing R] in
78 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
79 (r : R) :
80 completedGroupAlgebraStageMapInClass C R G U (algebraMap R (MonoidAlgebra R G) r) =
81 algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r := by
82 simp only [completedGroupAlgebraStageMapInClass, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,
83 RingHom.coe_id, Function.comp_apply, id_eq, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, map_one]
85omit [TopologicalSpace R] [IsTopologicalRing R] in
87 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C) :
88 Function.Surjective (completedGroupAlgebraStageMapInClass C R G U) := by
89 classical
90 intro x
91 induction x using Finsupp.induction with
94 | single_add q r x _ _ ih =>
95 rcases openNormalSubgroupInClassProj_surjective (C := C) (G := G) U q with ⟨g, hg⟩
96 rcases ih with ⟨y, hy⟩
97 refine ⟨(MonoidAlgebra.single g r : MonoidAlgebra R G) + y, ?_⟩
98 rw [map_add, completedGroupAlgebraStageMapInClass_single, hy, hg]
100omit [TopologicalSpace R] [IsTopologicalRing R] in
101@[simp]
102theorem completedGroupAlgebraStageMapInClass_compatible
103 (C : ProCGroups.FiniteGroupClass.{v})
104 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
105 (completedGroupAlgebraTransitionInClass C R G hUV).comp
106 (completedGroupAlgebraStageMapInClass C R G V) =
107 completedGroupAlgebraStageMapInClass C R G U := by
108 rw [completedGroupAlgebraTransitionInClass, completedGroupAlgebraStageMapInClass,
109 completedGroupAlgebraStageMapInClass, ← MonoidAlgebra.mapDomainRingHom_comp]
110 congr 1
112/-- The `C`-indexed finite-stage quotient maps form a compatible family. -/
114 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
115 (completedGroupAlgebraSystemInClass C hC R G).CompatibleMaps
116 (fun U => completedGroupAlgebraStageMapInClass C R G U) := by
117 intro U V hUV
118 funext x
119 exact congrFun
120 (congrArg DFunLike.coe
121 (completedGroupAlgebraStageMapInClass_compatible (R := R) (G := G) C hUV))
122 x
124/-- The canonical map `R[G] -> [[R G]]_C`, obtained from all `C`-indexed quotient maps. -/
126 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
127 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
128 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
129 (x : MonoidAlgebra R G) : CompletedGroupAlgebraInClass C hC R G :=
130 ⟨fun U => completedGroupAlgebraStageMapInClass C R G U x, by
131 intro U V hUV
132 exact congrFun
133 (congrArg DFunLike.coe
134 (completedGroupAlgebraStageMapInClass_compatible (R := R) (G := G) C hUV))
135 x⟩
137@[simp]
139 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
140 (U : CompletedGroupAlgebraIndexInClass G C) (x : MonoidAlgebra R G) :
141 completedGroupAlgebraProjectionInClass C hC R G U
142 (toCompletedGroupAlgebraInClass C hC R G x) =
143 completedGroupAlgebraStageMapInClass C R G U x :=
144 rfl
146@[simp]
148 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
149 (r : R) (x : MonoidAlgebra R G) :
150 toCompletedGroupAlgebraInClass C hC R G (r • x) =
151 r • toCompletedGroupAlgebraInClass C hC R G x := by
152 apply (completedGroupAlgebraSystemInClass C hC R G).ext
153 intro U
154 change completedGroupAlgebraStageMapInClass C R G U (r • x) =
155 r • completedGroupAlgebraStageMapInClass C R G U x
156 exact completedGroupAlgebraStageMapInClass_smul (R := R) (G := G) C U r x
158/-- The canonical map `R[G] -> [[R G]]_C`, as a ring homomorphism. -/
160 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
161 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
162 [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
163 MonoidAlgebra R G →+* CompletedGroupAlgebraInClass C hC R G where
164 toFun := toCompletedGroupAlgebraInClass C hC R G
165 map_zero' := by
166 apply (completedGroupAlgebraSystemInClass C hC R G).ext
167 intro U
169 map_one' := by
170 apply (completedGroupAlgebraSystemInClass C hC R G).ext
171 intro U
173 map_add' x y := by
174 apply (completedGroupAlgebraSystemInClass C hC R G).ext
175 intro U
177 map_mul' x y := by
178 apply (completedGroupAlgebraSystemInClass C hC R G).ext
179 intro U
182@[simp]
184 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
185 (x : MonoidAlgebra R G) :
186 toCompletedGroupAlgebraInClassRingHom C hC R G x =
187 toCompletedGroupAlgebraInClass C hC R G x :=
188 rfl
190/-- The canonical map `R[G] -> [[R G]]_C`, as an algebra homomorphism. -/
192 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
193 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
194 [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
195 MonoidAlgebra R G →ₐ[R] CompletedGroupAlgebraInClass C hC R G where
196 toRingHom := toCompletedGroupAlgebraInClassRingHom C hC R G
197 commutes' := by
198 intro r
199 apply (completedGroupAlgebraSystemInClass C hC R G).ext
200 intro U
201 change completedGroupAlgebraStageMapInClass C R G U
202 (algebraMap R (MonoidAlgebra R G) r) =
203 algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r
204 exact completedGroupAlgebraStageMapInClass_algebraMap (R := R) (G := G) C U r
206@[simp]
208 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
209 (x : MonoidAlgebra R G) :
210 toCompletedGroupAlgebraInClassAlgHom C hC R G x =
211 toCompletedGroupAlgebraInClass C hC R G x :=
212 rfl
214/-- The canonical map `R[G] -> [[R G]]_C`, as a linear map. -/
216 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
217 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
218 [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
219 MonoidAlgebra R G →ₗ[R] CompletedGroupAlgebraInClass C hC R G where
220 toFun := toCompletedGroupAlgebraInClass C hC R G
221 map_add' := by
222 intro x y
223 exact map_add (toCompletedGroupAlgebraInClassRingHom C hC R G) x y
224 map_smul' := toCompletedGroupAlgebraInClass_smul (R := R) (G := G) C hC
226@[simp]
228 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
229 (x : MonoidAlgebra R G) :
230 toCompletedGroupAlgebraInClassLinearMap C hC R G x =
231 toCompletedGroupAlgebraInClass C hC R G x :=
232 rfl
234@[simp]
236 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
237 (U : CompletedGroupAlgebraIndexInClass G C) :
238 (completedGroupAlgebraProjectionRingHomInClass C hC R G U).comp
239 (toCompletedGroupAlgebraInClassRingHom C hC R G) =
240 completedGroupAlgebraStageMapInClass C R G U := by
241 apply RingHom.ext
242 intro x
243 rfl
245/-- The abstract group algebra is dense in the `C`-indexed completed group algebra when `G` is
246pro-`C` and `C` is a formation. -/
248 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
249 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
250 DenseRange (toCompletedGroupAlgebraInClass C hC R G) := by
251 let S := completedGroupAlgebraSystemInClass C hC R G
252 letI : Nonempty (OpenNormalSubgroupInClass C G) :=
253 IsProCGroup.openNormalSubgroupInClass_nonempty hG
254 letI : Nonempty (CompletedGroupAlgebraIndexInClass G C) := inferInstance
255 have hdir :
256 Directed (α := CompletedGroupAlgebraIndexInClass G C) (· ≤ ·) fun U => U :=
257 directed_openNormalSubgroupInClass (C := C) (G := G) hForm
258 have hdense :
259 DenseRange
260 (S.inverseLimitLift
261 (fun U : CompletedGroupAlgebraIndexInClass G C =>
262 completedGroupAlgebraStageMapInClass C R G U)
263 (completedGroupAlgebraStageMapInClass_compatibleMaps (R := R) (G := G) C hC)) :=
264 S.denseRange_lift
265 (fun U : CompletedGroupAlgebraIndexInClass G C =>
266 completedGroupAlgebraStageMapInClass C R G U)
267 (completedGroupAlgebraStageMapInClass_compatibleMaps (R := R) (G := G) C hC)
268 (fun U => completedGroupAlgebraStageMapInClass_surjective (R := R) (G := G) C U)
269 hdir
270 simpa [S, toCompletedGroupAlgebraInClass] using hdense
272@[simp]
274 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
275 (completedGroupAlgebraTransition R G hUV).comp
276 (completedGroupAlgebraProjectionRingHom R G V) =
277 completedGroupAlgebraProjectionRingHom R G U := by
278 apply RingHom.ext
279 intro x
280 exact completedGroupAlgebraProjection_compatible (R := R) (G := G) x hUV
282/-- The quotient map from the abstract group algebra `R[G]` to one finite stage `R[G/U]`. -/
283def completedGroupAlgebraStageMap (R : Type u) (G : Type v) [CommRing R] [Group G]
284 [TopologicalSpace G] [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
285 MonoidAlgebra R G →+* CompletedGroupAlgebraStage R G U :=
286 MonoidAlgebra.mapDomainRingHom R
288 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U)
290omit [TopologicalSpace R] [IsTopologicalRing R] in
291@[simp]
293 (U : CompletedGroupAlgebraIndex G) (g : G) :
294 completedGroupAlgebraStageMap R G U (MonoidAlgebra.of R G g) =
295 MonoidAlgebra.single (openNormalSubgroupInClassProj
296 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) 1 := by
297 classical
298 simp only [completedGroupAlgebraStageMap, MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk,
299 OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
300 rfl
302omit [TopologicalSpace R] [IsTopologicalRing R] in
304 (U : CompletedGroupAlgebraIndex G) (g : G) (r : R) :
305 completedGroupAlgebraStageMap R G U (MonoidAlgebra.single g r) =
306 MonoidAlgebra.single (openNormalSubgroupInClassProj
307 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) r := by
308 classical
309 simp only [completedGroupAlgebraStageMap, MonoidAlgebra.single, MonoidAlgebra.mapDomainRingHom_apply,
310 Finsupp.mapDomain_single]
311 rfl
313omit [TopologicalSpace R] [IsTopologicalRing R] in
315 (U : CompletedGroupAlgebraIndex G) (r : R) (x : MonoidAlgebra R G) :
316 completedGroupAlgebraStageMap R G U (r • x) =
317 r • completedGroupAlgebraStageMap R G U x := by
319 congr 1
320 simp only [completedGroupAlgebraStageMap, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,
321 RingHom.coe_id, Function.comp_apply, id_eq, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, map_one]
323omit [TopologicalSpace R] [IsTopologicalRing R] in
325 (U : CompletedGroupAlgebraIndex G) (r : R) :
326 completedGroupAlgebraStageMap R G U (algebraMap R (MonoidAlgebra R G) r) =
327 algebraMap R (CompletedGroupAlgebraStage R G U) r := by
328 simp only [completedGroupAlgebraStageMap, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,
329 RingHom.coe_id, Function.comp_apply, id_eq, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, map_one]
331omit [TopologicalSpace R] [IsTopologicalRing R] in
332theorem completedGroupAlgebraStageMap_surjective (U : CompletedGroupAlgebraIndex G) :
333 Function.Surjective (completedGroupAlgebraStageMap R G U) := by
334 classical
335 intro x
336 induction x using Finsupp.induction with
338 exact ⟨0, map_zero (completedGroupAlgebraStageMap R G U)⟩
339 | single_add q r x _ _ ih =>
341 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U q with
342 ⟨g, hg⟩
343 rcases ih with ⟨y, hy⟩
344 refine ⟨(MonoidAlgebra.single g r : MonoidAlgebra R G) + y, ?_⟩
345 rw [map_add, completedGroupAlgebraStageMap_single, hy, hg]
347omit [TopologicalSpace R] [IsTopologicalRing R] in
348@[simp]
350 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
351 (completedGroupAlgebraTransition R G hUV).comp (completedGroupAlgebraStageMap R G V) =
352 completedGroupAlgebraStageMap R G U := by
354 completedGroupAlgebraStageMap, ← MonoidAlgebra.mapDomainRingHom_comp]
355 congr 1
357/-- The finite-stage quotient maps form a compatible family into the completed group algebra
358system. -/
361 (fun U => completedGroupAlgebraStageMap R G U) := by
362 intro U V hUV
363 funext x
364 exact congrFun
365 (congrArg DFunLike.coe
366 (completedGroupAlgebraStageMap_compatible (R := R) (G := G) (U := U) (V := V) hUV))
367 x
369/-- The canonical map `R[G] -> [[R G]]`, obtained from all quotient maps `R[G] -> R[G/U]`. -/
370def toCompletedGroupAlgebra (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
371 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
372 (x : MonoidAlgebra R G) : Carrier R G :=
373 ⟨fun U => completedGroupAlgebraStageMap R G U x, by
374 intro U V hUV
375 exact congrFun
376 (congrArg DFunLike.coe
377 (completedGroupAlgebraStageMap_compatible (R := R) (G := G) (U := U) (V := V) hUV))
378 x⟩
380@[simp]
382 (U : CompletedGroupAlgebraIndex G) (x : MonoidAlgebra R G) :
383 completedGroupAlgebraProjection R G U (toCompletedGroupAlgebra R G x) =
384 completedGroupAlgebraStageMap R G U x := rfl
386@[simp]
387theorem toCompletedGroupAlgebra_smul (r : R) (x : MonoidAlgebra R G) :
388 toCompletedGroupAlgebra R G (r • x) =
389 r • toCompletedGroupAlgebra R G x := by
390 apply (completedGroupAlgebraSystem R G).ext
391 intro U
392 change completedGroupAlgebraProjection R G U (toCompletedGroupAlgebra R G (r • x)) =
393 completedGroupAlgebraProjection R G U (r • toCompletedGroupAlgebra R G x)
399/-- The canonical map `R[G] -> [[R G]]` as a ring homomorphism. -/
400def toCompletedGroupAlgebraRingHom (R : Type u) (G : Type v) [CommRing R]
401 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
402 [IsTopologicalGroup G] :
403 MonoidAlgebra R G →+* Carrier R G where
404 toFun := toCompletedGroupAlgebra R G
405 map_zero' := by
406 apply (completedGroupAlgebraSystem R G).ext
407 intro U
408 exact map_zero (completedGroupAlgebraStageMap R G U)
409 map_one' := by
410 apply (completedGroupAlgebraSystem R G).ext
411 intro U
412 exact map_one (completedGroupAlgebraStageMap R G U)
413 map_add' x y := by
414 apply (completedGroupAlgebraSystem R G).ext
415 intro U
416 exact map_add (completedGroupAlgebraStageMap R G U) x y
417 map_mul' x y := by
418 apply (completedGroupAlgebraSystem R G).ext
419 intro U
420 exact map_mul (completedGroupAlgebraStageMap R G U) x y
422@[simp]
424 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
425 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC).comp
426 (toCompletedGroupAlgebraRingHom R G) =
427 toCompletedGroupAlgebraInClassRingHom C hC R G := by
428 apply RingHom.ext
429 intro x
430 apply (completedGroupAlgebraSystemInClass C hC R G).ext
431 intro U
432 rfl
434@[simp]
436 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
437 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
438 (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG).comp
439 (toCompletedGroupAlgebraInClassRingHom C hC R G) =
440 toCompletedGroupAlgebraRingHom R G := by
441 rw [← completedGroupAlgebraToInClass_comp_toCompletedGroupAlgebra (R := R) (G := G) C hC,
442 ← RingHom.comp_assoc, completedGroupAlgebraFromInClassRingHom_comp_toInClassRingHom]
443 rfl
445/-- The canonical map `R[G] -> [[R G]]` as an `R`-algebra homomorphism. -/
446def toCompletedGroupAlgebraAlgHom (R : Type u) (G : Type v) [CommRing R]
447 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
448 [IsTopologicalGroup G] :
449 MonoidAlgebra R G →ₐ[R] Carrier R G where
450 toRingHom := toCompletedGroupAlgebraRingHom R G
451 commutes' := by
452 intro r
453 apply (completedGroupAlgebraSystem R G).ext
454 intro U
455 change completedGroupAlgebraStageMap R G U (algebraMap R (MonoidAlgebra R G) r) =
456 algebraMap R (CompletedGroupAlgebraStage R G U) r
457 exact completedGroupAlgebraStageMap_algebraMap (R := R) (G := G) U r
459/-- The canonical map `R[G] -> [[R G]]` as an `R`-linear map. -/
460def toCompletedGroupAlgebraLinearMap (R : Type u) (G : Type v) [CommRing R]
461 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
462 [IsTopologicalGroup G] :
463 MonoidAlgebra R G →ₗ[R] Carrier R G where
464 toFun := toCompletedGroupAlgebra R G
465 map_add' := by
466 intro x y
467 exact map_add (toCompletedGroupAlgebraRingHom R G) x y
468 map_smul' := toCompletedGroupAlgebra_smul (R := R) (G := G)
470@[simp]
472 (U : CompletedGroupAlgebraIndex G) :
473 (completedGroupAlgebraProjectionRingHom R G U).comp
474 (toCompletedGroupAlgebraRingHom R G) =
475 completedGroupAlgebraStageMap R G U := by
476 apply RingHom.ext
477 intro x
478 exact completedGroupAlgebraProjection_toCompletedGroupAlgebra (R := R) (G := G) U x
480omit G [Group G] [TopologicalSpace G] [IsTopologicalGroup G] in
481end