Yamaguchi Lean 4 Library
Source: ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.CanonicalMaps
ProCGroups/CompletedGroupAlgebra/OpenFiniteQuotientTopology/CanonicalMaps/Source

Source: ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.CanonicalMaps

1import ProCGroups.CompletedGroupAlgebra.Basic.ClassComparison
3/-!
4# Completed Group Algebra / Open Finite Quotient Topology / Canonical Maps
6This module constructs the canonical dense maps from the abstract group algebra to the
7\(C\)-indexed and all-finite named completions, together with their bundled ring, algebra, and
8linear forms and finite-stage characterizations.
9-/
11open scoped Topology
13namespace CompletedGroupAlgebra
15noncomputable section
17open ProCGroups
18open ProCGroups.ProC
19open ProCGroups.InverseSystems
20open ProCGroups.Completion
22universe u v w
24variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
25variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
26variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
28/-- The quotient map from the abstract group algebra \(R[G]\) to one \(C\)-indexed finite stage. -/
29def completedGroupAlgebraStageMapInClass
30 (C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]
31 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
32 (U : CompletedGroupAlgebraIndexInClass G C) :
33 MonoidAlgebra R G →+* CompletedGroupAlgebraStageInClass C R G U :=
34 MonoidAlgebra.mapDomainRingHom R
35 (openNormalSubgroupInClassProj (C := C) (G := G) U)
37omit [TopologicalSpace R] [IsTopologicalRing R] in
38/--
39At a \(C\)-indexed stage \(U\), the quotient map sends the group-like element of \(g\) to the
40singleton at the image of \(g\) in \(G/U\), with coefficient \(1\).
41-/
42@[simp]
43theorem completedGroupAlgebraStageMapInClass_of
44 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
45 (g : G) :
46 completedGroupAlgebraStageMapInClass C R G U (MonoidAlgebra.of R G g) =
47 MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1 := by
48 change
49 MonoidAlgebra.mapDomain
50 (openNormalSubgroupInClassProj (C := C) (G := G) U)
51 (MonoidAlgebra.single g 1) =
52 MonoidAlgebra.single
53 (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1
54 exact MonoidAlgebra.mapDomain_single
56omit [TopologicalSpace R] [IsTopologicalRing R] in
57/--
58At a \(C\)-indexed stage \(U\), the quotient map sends the singleton at \(g\) with coefficient
59\(r\) to the singleton at the image of \(g\) in \(G/U\), with coefficient \(r\).
60-/
61theorem completedGroupAlgebraStageMapInClass_single
62 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
63 (g : G) (r : R) :
64 completedGroupAlgebraStageMapInClass C R G U (MonoidAlgebra.single g r) =
65 MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) r := by
66 change
67 MonoidAlgebra.mapDomain
68 (openNormalSubgroupInClassProj (C := C) (G := G) U)
69 (MonoidAlgebra.single g r) =
70 MonoidAlgebra.single
71 (openNormalSubgroupInClassProj (C := C) (G := G) U g) r
72 exact MonoidAlgebra.mapDomain_single
74omit [TopologicalSpace R] [IsTopologicalRing R] in
75/-- The \(C\)-indexed quotient-stage map preserves scalar multiplication by elements of \(R\). -/
76theorem completedGroupAlgebraStageMapInClass_smul
77 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
78 (r : R) (x : MonoidAlgebra R G) :
79 completedGroupAlgebraStageMapInClass C R G U (r • x) =
80 r • completedGroupAlgebraStageMapInClass C R G U x := by
81 rw [Algebra.smul_def, Algebra.smul_def, map_mul]
82 congr 1
83 change
84 MonoidAlgebra.mapDomain
85 (openNormalSubgroupInClassProj (C := C) (G := G) U)
86 (MonoidAlgebra.single 1 r) =
87 MonoidAlgebra.single 1 r
88 rw [MonoidAlgebra.mapDomain_single,
89 (openNormalSubgroupInClassProj (C := C) (G := G) U).map_one]
91omit [TopologicalSpace R] [IsTopologicalRing R] in
92/--
93The \(C\)-indexed quotient-stage map commutes with the canonical embeddings of scalars from
94\(R\).
95-/
96theorem completedGroupAlgebraStageMapInClass_algebraMap
97 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
98 (r : R) :
99 completedGroupAlgebraStageMapInClass C R G U (algebraMap R (MonoidAlgebra R G) r) =
100 algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r := by
101 change
102 MonoidAlgebra.mapDomain
103 (openNormalSubgroupInClassProj (C := C) (G := G) U)
104 (MonoidAlgebra.single 1 r) =
105 MonoidAlgebra.single 1 r
106 rw [MonoidAlgebra.mapDomain_single,
107 (openNormalSubgroupInClassProj (C := C) (G := G) U).map_one]
109omit [TopologicalSpace R] [IsTopologicalRing R] in
110/-- The quotient map \(R[G]\to R[G/U]\) is surjective for every \(C\)-indexed stage \(U\). -/
111theorem completedGroupAlgebraStageMapInClass_surjective
112 (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C) :
113 Function.Surjective (completedGroupAlgebraStageMapInClass C R G U) := by
114 classical
115 intro x
116 obtain ⟨y, hy⟩ :=
117 Finsupp.mapDomain_surjective (M := R)
118 (openNormalSubgroupInClassProj_surjective (C := C) (G := G) U) x.coeff
119 refine ⟨MonoidAlgebra.ofCoeff y, ?_⟩
120 apply MonoidAlgebra.coeff_injective
121 exact hy
123omit [TopologicalSpace R] [IsTopologicalRing R] in
124/--
125The class-restricted completed group-algebra stage map is compatible with transition maps and
126coordinate projections for the completed group algebra.
127-/
128@[simp]
129theorem completedGroupAlgebraStageMapInClass_compatible
130 (C : ProCGroups.FiniteGroupClass.{v})
131 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
132 (completedGroupAlgebraTransitionInClass C R G hUV).comp
133 (completedGroupAlgebraStageMapInClass C R G V) =
134 completedGroupAlgebraStageMapInClass C R G U := by
135 rw [completedGroupAlgebraTransitionInClass, completedGroupAlgebraStageMapInClass,
136 completedGroupAlgebraStageMapInClass, ← MonoidAlgebra.mapDomainRingHom_comp]
137 congr 1
139/-- The \(C\)-indexed finite-stage quotient maps form a compatible family. -/
140theorem completedGroupAlgebraStageMapInClass_compatibleMaps
141 (C : ProCGroups.FiniteGroupClass.{v}) :
142 (completedGroupAlgebraSystemInClass C R G).CompatibleMaps
143 (fun U => completedGroupAlgebraStageMapInClass C R G U) := by
144 intro U V hUV
145 funext x
146 exact congrFun
147 (congrArg DFunLike.coe
148 (completedGroupAlgebraStageMapInClass_compatible (R := R) (G := G) C hUV))
149 x
151/--
152The canonical map \(R[G] \to \widehat{R[G]}_C\), obtained from all \(C\)-indexed quotient maps.
153-/
154def toCompletedGroupAlgebraInClass
155 (C : ProCGroups.FiniteGroupClass.{v})
156 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
157 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
158 (x : MonoidAlgebra R G) : CompletedGroupAlgebraInClass C R G :=
159 (completedGroupAlgebraInClassCompatibleFamilyEquiv
160 (R := R) (G := G) C).symm
161 ((completedGroupAlgebraSystemInClass C R G).inverseLimitLift
162 (fun U => completedGroupAlgebraStageMapInClass C R G U)
163 (completedGroupAlgebraStageMapInClass_compatibleMaps
164 (R := R) (G := G) C) x)
166/--
167The \(U\)-coordinate of the canonical dense element in the \(C\)-indexed completion is the
168\(C\)-indexed stage map at \(U\).
169-/
170@[simp]
171theorem completedGroupAlgebraProjectionInClass_toCompletedGroupAlgebraInClass
172 (C : ProCGroups.FiniteGroupClass.{v})
173 (U : CompletedGroupAlgebraIndexInClass G C) (x : MonoidAlgebra R G) :
174 completedGroupAlgebraProjectionInClass C R G U
175 (toCompletedGroupAlgebraInClass C R G x) =
176 completedGroupAlgebraStageMapInClass C R G U x :=
177 rfl
179/--
180The canonical map from \(R[G]\) into the \(C\)-indexed completed group algebra preserves scalar
181multiplication by \(R\).
182-/
183@[simp]
184theorem toCompletedGroupAlgebraInClass_smul
185 (C : ProCGroups.FiniteGroupClass.{v})
186 (r : R) (x : MonoidAlgebra R G) :
187 toCompletedGroupAlgebraInClass C R G (r • x) =
188 r • toCompletedGroupAlgebraInClass C R G x := by
189 apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
190 intro U
191 change completedGroupAlgebraStageMapInClass C R G U (r • x) =
192 r • completedGroupAlgebraStageMapInClass C R G U x
193 exact completedGroupAlgebraStageMapInClass_smul (R := R) (G := G) C U r x
195/-- The canonical map \(R[G] \to \widehat{R[G]}_C\) is bundled as a ring homomorphism. -/
196def toCompletedGroupAlgebraInClassRingHom
197 (C : ProCGroups.FiniteGroupClass.{v})
198 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
199 [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
200 MonoidAlgebra R G →+* CompletedGroupAlgebraInClass C R G where
201 toFun := toCompletedGroupAlgebraInClass C R G
202 map_zero' := by
203 apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
204 intro U
205 exact map_zero (completedGroupAlgebraStageMapInClass C R G U)
206 map_one' := by
207 apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
208 intro U
209 exact map_one (completedGroupAlgebraStageMapInClass C R G U)
210 map_add' x y := by
211 apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
212 intro U
213 exact map_add (completedGroupAlgebraStageMapInClass C R G U) x y
214 map_mul' x y := by
215 apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
216 intro U
217 exact map_mul (completedGroupAlgebraStageMapInClass C R G U) x y
219/--
220The bundled ring homomorphism has the same underlying function as the coordinatewise
221construction.
222-/
223@[simp]
224theorem toCompletedGroupAlgebraInClassRingHom_apply
225 (C : ProCGroups.FiniteGroupClass.{v})
226 (x : MonoidAlgebra R G) :
227 toCompletedGroupAlgebraInClassRingHom C R G x =
228 toCompletedGroupAlgebraInClass C R G x :=
229 rfl
231/-- The canonical map \(R[G] \to \widehat{R[G]}_C\), as an algebra homomorphism. -/
232def toCompletedGroupAlgebraInClassAlgHom
233 (C : ProCGroups.FiniteGroupClass.{v})
234 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
235 [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
236 MonoidAlgebra R G →ₐ[R] CompletedGroupAlgebraInClass C R G where
237 toRingHom := toCompletedGroupAlgebraInClassRingHom C R G
238 commutes' := by
239 intro r
240 apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
241 intro U
242 change completedGroupAlgebraStageMapInClass C R G U
243 (algebraMap R (MonoidAlgebra R G) r) =
244 algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r
245 exact completedGroupAlgebraStageMapInClass_algebraMap (R := R) (G := G) C U r
247/--
248Evaluating the canonical \(C\)-indexed algebra homomorphism gives the coordinatewise dense map
249`toCompletedGroupAlgebraInClass`.
250-/
251@[simp]
252theorem toCompletedGroupAlgebraInClassAlgHom_apply
253 (C : ProCGroups.FiniteGroupClass.{v})
254 (x : MonoidAlgebra R G) :
255 toCompletedGroupAlgebraInClassAlgHom C R G x =
256 toCompletedGroupAlgebraInClass C R G x :=
257 rfl
259/-- The canonical map \(R[G] \to \widehat{R[G]}_C\), as a linear map. -/
260def toCompletedGroupAlgebraInClassLinearMap
261 (C : ProCGroups.FiniteGroupClass.{v})
262 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
263 [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
264 MonoidAlgebra R G →ₗ[R] CompletedGroupAlgebraInClass C R G where
265 toFun := toCompletedGroupAlgebraInClass C R G
266 map_add' := by
267 intro x y
268 exact map_add (toCompletedGroupAlgebraInClassRingHom C R G) x y
269 map_smul' := toCompletedGroupAlgebraInClass_smul (R := R) (G := G) C
271/-- The bundled linear map has the same underlying function as the coordinatewise construction. -/
272@[simp]
273theorem toCompletedGroupAlgebraInClassLinearMap_apply
274 (C : ProCGroups.FiniteGroupClass.{v})
275 (x : MonoidAlgebra R G) :
276 toCompletedGroupAlgebraInClassLinearMap C R G x =
277 toCompletedGroupAlgebraInClass C R G x :=
278 rfl
280/--
281Composing the \(U\)-coordinate projection from the \(C\)-indexed completion with its canonical
282dense ring homomorphism gives the \(C\)-indexed stage map at \(U\).
283-/
284@[simp]
285theorem completedGAProjectionInClass_comp_toCompletedGAInClass
286 (C : ProCGroups.FiniteGroupClass.{v})
287 (U : CompletedGroupAlgebraIndexInClass G C) :
288 (completedGroupAlgebraProjectionInClass C R G U).comp
289 (toCompletedGroupAlgebraInClassRingHom C R G) =
290 completedGroupAlgebraStageMapInClass C R G U := by
291 apply RingHom.ext
292 intro x
293 rfl
295/--
296The abstract group algebra is dense in the \(C\)-indexed completed group algebra when \(G\) is
297pro-\(C\) and \(C\) is a formation.
298-/
299theorem denseRange_toCompletedGroupAlgebraInClass
300 (C : ProCGroups.FiniteGroupClass.{v})
301 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
302 DenseRange (toCompletedGroupAlgebraInClass C R G) := by
303 let S := completedGroupAlgebraSystemInClass C R G
304 letI : Nonempty (OpenNormalSubgroupInClass C G) :=
305 HasOpenNormalBasisInClass.openNormalSubgroupInClass_nonempty hG
306 letI : Nonempty (CompletedGroupAlgebraIndexInClass G C) := inferInstance
307 have hdir :
308 Directed (α := CompletedGroupAlgebraIndexInClass G C) (· ≤ ·) fun U => U :=
309 directed_openNormalSubgroupInClass (C := C) (G := G) hForm
310 have hdense :
311 DenseRange
312 (S.inverseLimitLift
313 (fun U : CompletedGroupAlgebraIndexInClass G C =>
314 completedGroupAlgebraStageMapInClass C R G U)
315 (completedGroupAlgebraStageMapInClass_compatibleMaps (R := R) (G := G) C )) :=
316 S.denseRange_lift
317 (fun U : CompletedGroupAlgebraIndexInClass G C =>
318 completedGroupAlgebraStageMapInClass C R G U)
319 (completedGroupAlgebraStageMapInClass_compatibleMaps (R := R) (G := G) C )
320 (fun U => completedGroupAlgebraStageMapInClass_surjective (R := R) (G := G) C U)
321 hdir
322 change DenseRange
323 (S.inverseLimitLift
324 (fun U : CompletedGroupAlgebraIndexInClass G C =>
325 completedGroupAlgebraStageMapInClass C R G U)
326 (completedGroupAlgebraStageMapInClass_compatibleMaps (R := R) (G := G) C))
327 exact hdense
329/--
330Projecting to a finer stage \(V\) and then applying the transition to \(U\) agrees with projecting
331directly to \(U\).
332-/
333@[simp]
334theorem completedGroupAlgebraTransition_comp_projection
335 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
336 (completedGroupAlgebraTransition R G hUV).comp
337 (completedGroupAlgebraProjection R G V) =
338 completedGroupAlgebraProjection R G U := by
339 apply RingHom.ext
340 intro x
341 exact completedGroupAlgebraProjection_compatible (R := R) (G := G) x hUV
343/-- The quotient map from the abstract group algebra \(R[G]\) to one finite stage \(R[G/U]\). -/
344def completedGroupAlgebraStageMap (R : Type u) (G : Type v) [CommRing R] [Group G]
345 [TopologicalSpace G] [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
346 MonoidAlgebra R G →+* CompletedGroupAlgebraStage R G U :=
347 MonoidAlgebra.mapDomainRingHom R
348 (openNormalSubgroupInClassProj
351omit [TopologicalSpace R] [IsTopologicalRing R] in
352/--
353At an all-finite stage \(U\), the quotient map sends the group-like element of \(g\) to the
354singleton at the image of \(g\) in \(G/U\), with coefficient \(1\).
355-/
356@[simp]
357theorem completedGroupAlgebraStageMap_of
358 (U : CompletedGroupAlgebraIndex G) (g : G) :
359 completedGroupAlgebraStageMap R G U (MonoidAlgebra.of R G g) =
360 MonoidAlgebra.single (openNormalSubgroupInClassProj
361 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) 1 := by
362 change
363 MonoidAlgebra.mapDomain
364 (openNormalSubgroupInClassProj
366 (MonoidAlgebra.single g 1) =
367 MonoidAlgebra.single
368 (openNormalSubgroupInClassProj
370 exact MonoidAlgebra.mapDomain_single
372omit [TopologicalSpace R] [IsTopologicalRing R] in
373/--
374At an all-finite stage \(U\), the quotient map sends the singleton at \(g\) with coefficient \(r\)
375to the singleton at the image of \(g\) in \(G/U\), with coefficient \(r\).
376-/
377theorem completedGroupAlgebraStageMap_single
378 (U : CompletedGroupAlgebraIndex G) (g : G) (r : R) :
379 completedGroupAlgebraStageMap R G U (MonoidAlgebra.single g r) =
380 MonoidAlgebra.single (openNormalSubgroupInClassProj
381 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) r := by
382 change
383 MonoidAlgebra.mapDomain
384 (openNormalSubgroupInClassProj
386 (MonoidAlgebra.single g r) =
387 MonoidAlgebra.single
388 (openNormalSubgroupInClassProj
390 exact MonoidAlgebra.mapDomain_single
392omit [TopologicalSpace R] [IsTopologicalRing R] in
393/-- The all-finite quotient-stage map preserves scalar multiplication by elements of \(R\). -/
394theorem completedGroupAlgebraStageMap_smul
395 (U : CompletedGroupAlgebraIndex G) (r : R) (x : MonoidAlgebra R G) :
396 completedGroupAlgebraStageMap R G U (r • x) =
397 r • completedGroupAlgebraStageMap R G U x := by
398 rw [Algebra.smul_def, Algebra.smul_def, map_mul]
399 congr 1
400 change
401 MonoidAlgebra.mapDomain
402 (openNormalSubgroupInClassProj
404 (MonoidAlgebra.single 1 r) =
405 MonoidAlgebra.single 1 r
406 rw [MonoidAlgebra.mapDomain_single,
407 (openNormalSubgroupInClassProj
408 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U).map_one]
410omit [TopologicalSpace R] [IsTopologicalRing R] in
411/--
412The all-finite quotient-stage map commutes with the canonical embeddings of scalars from \(R\).
413-/
414theorem completedGroupAlgebraStageMap_algebraMap
415 (U : CompletedGroupAlgebraIndex G) (r : R) :
416 completedGroupAlgebraStageMap R G U (algebraMap R (MonoidAlgebra R G) r) =
417 algebraMap R (CompletedGroupAlgebraStage R G U) r := by
418 change
419 MonoidAlgebra.mapDomain
420 (openNormalSubgroupInClassProj
422 (MonoidAlgebra.single 1 r) =
423 MonoidAlgebra.single 1 r
424 rw [MonoidAlgebra.mapDomain_single,
425 (openNormalSubgroupInClassProj
426 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U).map_one]
428omit [TopologicalSpace R] [IsTopologicalRing R] in
429/-- The quotient map \(R[G]\to R[G/U]\) is surjective for every all-finite stage \(U\). -/
430theorem completedGroupAlgebraStageMap_surjective (U : CompletedGroupAlgebraIndex G) :
431 Function.Surjective (completedGroupAlgebraStageMap R G U) := by
432 classical
433 intro x
434 obtain ⟨y, hy⟩ :=
435 Finsupp.mapDomain_surjective (M := R)
436 (openNormalSubgroupInClassProj_surjective
437 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U) x.coeff
438 refine ⟨MonoidAlgebra.ofCoeff y, ?_⟩
439 apply MonoidAlgebra.coeff_injective
440 exact hy
442omit [TopologicalSpace R] [IsTopologicalRing R] in
443/--
444The completed group-algebra stage map is compatible with transition maps and coordinate
445projections for the completed group algebra.
446-/
447@[simp]
448theorem completedGroupAlgebraStageMap_compatible
449 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
450 (completedGroupAlgebraTransition R G hUV).comp (completedGroupAlgebraStageMap R G V) =
451 completedGroupAlgebraStageMap R G U := by
452 rw [completedGroupAlgebraTransition, completedGroupAlgebraStageMap,
453 completedGroupAlgebraStageMap, ← MonoidAlgebra.mapDomainRingHom_comp]
454 congr 1
456/--
457The finite-stage quotient maps form a compatible family into the completed group algebra system.
458-/
459theorem completedGroupAlgebraStageMap_compatibleMaps :
460 (completedGroupAlgebraSystem R G).CompatibleMaps
461 (fun U => completedGroupAlgebraStageMap R G U) := by
462 intro U V hUV
463 funext x
464 exact congrFun
465 (congrArg DFunLike.coe
466 (completedGroupAlgebraStageMap_compatible (R := R) (G := G) (U := U) (V := V) hUV))
467 x
469/--
470The canonical map \(R[G] \to \widehat{R[G]}\), obtained from all quotient maps \(R[G]\to
471R[G/U]\).
472-/
473def toCompletedGroupAlgebra (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
474 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
475 (x : MonoidAlgebra R G) : CompletedGroupAlgebraCarrier R G :=
476 (completedGroupAlgebraCompatibleFamilyEquiv (R := R) (G := G)).symm
477 ((completedGroupAlgebraSystem R G).inverseLimitLift
478 (fun U => completedGroupAlgebraStageMap R G U)
479 (completedGroupAlgebraStageMap_compatibleMaps (R := R) (G := G)) x)
481/--
482The \(U\)-coordinate of the canonical dense element in the all-finite completion is the
483all-finite stage map at \(U\).
484-/
485@[simp]
486theorem completedGroupAlgebraProjection_toCompletedGroupAlgebra
487 (U : CompletedGroupAlgebraIndex G) (x : MonoidAlgebra R G) :
488 completedGroupAlgebraProjection R G U (toCompletedGroupAlgebra R G x) =
489 completedGroupAlgebraStageMap R G U x := rfl
491/--
492The canonical map from \(R[G]\) into the all-finite completed group algebra preserves scalar
493multiplication by \(R\).
494-/
495@[simp]
496theorem toCompletedGroupAlgebra_smul (r : R) (x : MonoidAlgebra R G) :
497 toCompletedGroupAlgebra R G (r • x) =
498 r • toCompletedGroupAlgebra R G x := by
499 apply completedGroupAlgebra_ext (R := R) (G := G)
500 intro U
501 calc
502 completedGroupAlgebraProjection R G U
503 (toCompletedGroupAlgebra R G (r • x)) =
504 completedGroupAlgebraStageMap R G U (r • x) :=
505 completedGroupAlgebraProjection_toCompletedGroupAlgebra
506 (R := R) (G := G) U (r • x)
507 _ = r • completedGroupAlgebraStageMap R G U x :=
508 completedGroupAlgebraStageMap_smul (R := R) (G := G) U r x
509 _ = r • completedGroupAlgebraProjection R G U
510 (toCompletedGroupAlgebra R G x) := by
511 rw [completedGroupAlgebraProjection_toCompletedGroupAlgebra]
512 _ = completedGroupAlgebraProjection R G U
513 (r • toCompletedGroupAlgebra R G x) :=
514 ((completedGroupAlgebraProjectionAlgHom R G U).toLinearMap.map_smul
515 r (toCompletedGroupAlgebra R G x)).symm
517/-- The canonical map \(R[G] \to \widehat{R[G]}\) is bundled as a ring homomorphism. -/
518def toCompletedGroupAlgebraRingHom (R : Type u) (G : Type v) [CommRing R]
519 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
520 [IsTopologicalGroup G] :
521 MonoidAlgebra R G →+* CompletedGroupAlgebraCarrier R G where
522 toFun := toCompletedGroupAlgebra R G
523 map_zero' := by
524 apply completedGroupAlgebra_ext (R := R) (G := G)
525 intro U
526 exact map_zero (completedGroupAlgebraStageMap R G U)
527 map_one' := by
528 apply completedGroupAlgebra_ext (R := R) (G := G)
529 intro U
530 exact map_one (completedGroupAlgebraStageMap R G U)
531 map_add' x y := by
532 apply completedGroupAlgebra_ext (R := R) (G := G)
533 intro U
534 exact map_add (completedGroupAlgebraStageMap R G U) x y
535 map_mul' x y := by
536 apply completedGroupAlgebra_ext (R := R) (G := G)
537 intro U
538 exact map_mul (completedGroupAlgebraStageMap R G U) x y
540/--
541Restricting the all-finite completion to its \(C\)-indexed coordinates after applying the
542all-finite dense map agrees with the canonical \(C\)-indexed dense map.
543-/
544@[simp]
545theorem completedGroupAlgebraToInClass_comp_toCompletedGroupAlgebra
546 (C : ProCGroups.FiniteGroupClass.{v}) :
547 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ).comp
548 (toCompletedGroupAlgebraRingHom R G) =
549 toCompletedGroupAlgebraInClassRingHom C R G := by
550 apply RingHom.ext
551 intro x
552 apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
553 intro U
554 rfl
556/--
557Under the formation and pro-\(C\) hypotheses, transporting the \(C\)-indexed dense map back to the
558all-finite completion recovers the all-finite dense map.
559-/
560@[simp]
561theorem completedGroupAlgebraFromInClassRingHom_comp_toCompletedGroupAlgebraInClass
562 (C : ProCGroups.FiniteGroupClass.{v})
563 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
564 (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG).comp
565 (toCompletedGroupAlgebraInClassRingHom C R G) =
566 toCompletedGroupAlgebraRingHom R G := by
567 rw [← completedGroupAlgebraToInClass_comp_toCompletedGroupAlgebra (R := R) (G := G) C ,
568 ← RingHom.comp_assoc, completedGroupAlgebraFromInClassRingHom_comp_toInClassRingHom]
569 rfl
571/-- The canonical map \(R[G] \to \widehat{R[G]}\) as an \(R\)-algebra homomorphism. -/
572def toCompletedGroupAlgebraAlgHom (R : Type u) (G : Type v) [CommRing R]
573 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
574 [IsTopologicalGroup G] :
575 MonoidAlgebra R G →ₐ[R] CompletedGroupAlgebraCarrier R G where
576 toRingHom := toCompletedGroupAlgebraRingHom R G
577 commutes' := by
578 intro r
579 apply completedGroupAlgebra_ext (R := R) (G := G)
580 intro U
581 change completedGroupAlgebraStageMap R G U (algebraMap R (MonoidAlgebra R G) r) =
582 algebraMap R (CompletedGroupAlgebraStage R G U) r
583 exact completedGroupAlgebraStageMap_algebraMap (R := R) (G := G) U r
585/-- The canonical map \(R[G] \to \widehat{R[G]}\) as an \(R\)-linear map. -/
586def toCompletedGroupAlgebraLinearMap (R : Type u) (G : Type v) [CommRing R]
587 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
588 [IsTopologicalGroup G] :
589 MonoidAlgebra R G →ₗ[R] CompletedGroupAlgebraCarrier R G where
590 toFun := toCompletedGroupAlgebra R G
591 map_add' := by
592 intro x y
593 exact map_add (toCompletedGroupAlgebraRingHom R G) x y
594 map_smul' := toCompletedGroupAlgebra_smul (R := R) (G := G)
596/--
597Composing the \(U\)-coordinate projection from the all-finite completion with its canonical dense
598ring homomorphism gives the all-finite stage map at \(U\).
599-/
600@[simp]
601theorem completedGroupAlgebraProjection_comp_toCompletedGroupAlgebra
602 (U : CompletedGroupAlgebraIndex G) :
603 (completedGroupAlgebraProjection R G U).comp
604 (toCompletedGroupAlgebraRingHom R G) =
605 completedGroupAlgebraStageMap R G U := by
606 apply RingHom.ext
607 intro x
608 exact completedGroupAlgebraProjection_toCompletedGroupAlgebra (R := R) (G := G) U x
610omit G [Group G] [TopologicalSpace G] [IsTopologicalGroup G] in
611end
613end CompletedGroupAlgebra