CompletedGroupAlgebra/Basic/ClassComparison.lean
1import CompletedGroupAlgebra.Basic.AllFinite.Topology
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/Basic/ClassComparison.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 Algebra Class Comparisons
15-/
17open scoped Topology
19namespace CompletedGroupAlgebra
21noncomputable section
23open ProCGroups
24open ProCGroups.ProC
25open ProCGroups.InverseSystems
26open ProCGroups.Completion
28universe u v w
30variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
33/-- Projection from the all-finite completed group algebra to a stage indexed by a finite-only
34class `C`. -/
36 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
37 (U : CompletedGroupAlgebraIndexInClass G C) :
38 Carrier R G → CompletedGroupAlgebraStageInClass C R G U :=
40 (completedGroupAlgebraIndexInClassToAllFinite G C hC U)
42@[simp]
44 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
45 (U : CompletedGroupAlgebraIndexInClass G C) (x : Carrier R G) :
46 completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C hC U x =
48 (completedGroupAlgebraIndexInClassToAllFinite G C hC U) x :=
49 rfl
52 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
53 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
54 (x : Carrier R G) :
55 completedGroupAlgebraTransitionInClass C R G hUV
56 (completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C hC V x) =
57 completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C hC U x := by
58 change completedGroupAlgebraTransition R G
59 (completedGroupAlgebraIndexInClassToAllFinite_le (G := G) C hC hUV)
61 (completedGroupAlgebraIndexInClassToAllFinite G C hC V) x) =
63 (completedGroupAlgebraIndexInClassToAllFinite G C hC U) x
64 exact completedGroupAlgebraProjection_compatible (R := R) (G := G) x
65 (completedGroupAlgebraIndexInClassToAllFinite_le (G := G) C hC hUV)
67/-- The comparison map from the ordinary all-finite completed group algebra to the inverse limit
70 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
71 Carrier R G → CompletedGroupAlgebraInClass C hC R G :=
72 (completedGroupAlgebraSystemInClass C hC R G).inverseLimitLift
73 (fun U => completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C hC U)
74 (by
75 intro U V hUV
76 funext x
78 (R := R) (G := G) C hC hUV x)
80@[simp]
82 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
83 (U : CompletedGroupAlgebraIndexInClass G C) (x : Carrier R G) :
84 completedGroupAlgebraProjectionInClass C hC R G U
85 (completedGroupAlgebraToInClass (R := R) (G := G) C hC x) =
86 completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C hC U x :=
87 rfl
89/-- The comparison from the all-finite completed group algebra to the `C`-indexed inverse limit,
90as a ring homomorphism. -/
92 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
93 Carrier R G →+* CompletedGroupAlgebraInClass C hC R G where
94 toFun := completedGroupAlgebraToInClass (R := R) (G := G) C hC
95 map_zero' := by
96 apply (completedGroupAlgebraSystemInClass C hC R G).ext
97 intro U
98 rfl
99 map_one' := by
100 apply (completedGroupAlgebraSystemInClass C hC R G).ext
101 intro U
102 rfl
103 map_add' x y := by
104 apply (completedGroupAlgebraSystemInClass C hC R G).ext
105 intro U
106 rfl
107 map_mul' x y := by
108 apply (completedGroupAlgebraSystemInClass C hC R G).ext
109 intro U
110 rfl
112@[simp]
114 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
115 (x : Carrier R G) :
116 completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC x =
117 completedGroupAlgebraToInClass (R := R) (G := G) C hC x :=
118 rfl
120/-- The comparison from the all-finite completed group algebra to the `C`-indexed inverse limit,
121as an `R`-algebra homomorphism. -/
123 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
124 Carrier R G →ₐ[R] CompletedGroupAlgebraInClass C hC R G where
125 toRingHom := completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC
126 commutes' := by
127 intro r
128 apply (completedGroupAlgebraSystemInClass C hC R G).ext
129 intro U
130 rfl
132@[simp]
134 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
135 (x : Carrier R G) :
136 completedGroupAlgebraToInClassAlgHom (R := R) (G := G) C hC x =
137 completedGroupAlgebraToInClass (R := R) (G := G) C hC x :=
138 rfl
141 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
142 Continuous (completedGroupAlgebraToInClass (R := R) (G := G) C hC) := by
143 let S := completedGroupAlgebraSystemInClass C hC R G
144 letI : ∀ U : CompletedGroupAlgebraIndexInClass G C,
145 TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
146 fun U => S.topologicalSpace U
147 have hval : Continuous fun x : Carrier R G =>
148 fun U : CompletedGroupAlgebraIndexInClass G C =>
149 (show CompletedGroupAlgebraStageInClass C R G U from
150 (completedGroupAlgebraToInClass (R := R) (G := G) C hC x).1 U) := by
151 apply continuous_pi
152 intro U
153 change Continuous
154 (completedGroupAlgebraProjectionToStageInClass (R := R) (G := G) C hC U)
155 simpa [completedGroupAlgebraProjectionToStageInClass] using
156 (completedGroupAlgebraSystem R G).continuous_projection
157 (completedGroupAlgebraIndexInClassToAllFinite G C hC U)
158 exact Continuous.subtype_mk hval fun x =>
159 (completedGroupAlgebraToInClass (R := R) (G := G) C hC x).2
161/-- For a pro-`C` group, the `C`-indexed inverse limit maps back to the ordinary all-finite
162completed group algebra by reading the same open-normal quotient stages. -/
164 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
165 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
166 CompletedGroupAlgebraInClass C hC R G → Carrier R G :=
168 (fun U : CompletedGroupAlgebraIndex G =>
169 completedGroupAlgebraProjectionInClass C hC R G
170 (completedGroupAlgebraIndexToInClass G C hForm hG U))
171 (by
172 intro U V hUV
173 funext x
174 change completedGroupAlgebraTransitionInClass C R G
175 (completedGroupAlgebraIndexToInClass_le (G := G) C hForm hG hUV)
176 (completedGroupAlgebraProjectionInClass C hC R G
177 (completedGroupAlgebraIndexToInClass G C hForm hG V) x) =
178 completedGroupAlgebraProjectionInClass C hC R G
179 (completedGroupAlgebraIndexToInClass G C hForm hG U) x
181 (R := R) (G := G) C hC
182 (completedGroupAlgebraIndexToInClass_le (G := G) C hForm hG hUV) x)
184@[simp]
186 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
187 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (U : CompletedGroupAlgebraIndex G)
188 (x : CompletedGroupAlgebraInClass C hC R G) :
190 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x) =
191 completedGroupAlgebraProjectionInClass C hC R G
192 (completedGroupAlgebraIndexToInClass G C hForm hG U) x :=
193 rfl
195/-- Ring-homomorphism form of `completedGroupAlgebraFromInClass`. -/
197 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
198 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
199 CompletedGroupAlgebraInClass C hC R G →+* Carrier R G where
200 toFun := completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG
201 map_zero' := by
202 apply (completedGroupAlgebraSystem R G).ext
203 intro U
204 change completedGroupAlgebraProjection R G U
205 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG 0) =
206 completedGroupAlgebraProjection R G U (0 : Carrier R G)
208 exact map_zero (completedGroupAlgebraProjectionRingHomInClass C hC R G
209 (completedGroupAlgebraIndexToInClass G C hForm hG U))
210 map_one' := by
211 apply (completedGroupAlgebraSystem R G).ext
212 intro U
213 change completedGroupAlgebraProjection R G U
214 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG 1) =
215 completedGroupAlgebraProjection R G U (1 : Carrier R G)
217 exact map_one (completedGroupAlgebraProjectionRingHomInClass C hC R G
218 (completedGroupAlgebraIndexToInClass G C hForm hG U))
219 map_add' x y := by
220 apply (completedGroupAlgebraSystem R G).ext
221 intro U
222 change completedGroupAlgebraProjection R G U
223 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG (x + y)) =
225 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x +
226 completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG y)
228 exact map_add (completedGroupAlgebraProjectionRingHomInClass C hC R G
229 (completedGroupAlgebraIndexToInClass G C hForm hG U)) x y
230 map_mul' x y := by
231 apply (completedGroupAlgebraSystem R G).ext
232 intro U
233 change completedGroupAlgebraProjection R G U
234 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG (x * y)) =
236 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x *
237 completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG y)
239 exact map_mul (completedGroupAlgebraProjectionRingHomInClass C hC R G
240 (completedGroupAlgebraIndexToInClass G C hForm hG U)) x y
242@[simp]
244 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
245 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : CompletedGroupAlgebraInClass C hC R G) :
246 completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG x =
247 completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x :=
248 rfl
250/-- Algebra-homomorphism form of `completedGroupAlgebraFromInClass`. -/
252 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
253 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
254 CompletedGroupAlgebraInClass C hC R G →ₐ[R] Carrier R G where
255 toRingHom := completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG
256 commutes' := by
257 intro r
258 apply (completedGroupAlgebraSystem R G).ext
259 intro U
260 change completedGroupAlgebraProjection R G U
261 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG
262 (algebraMap R (CompletedGroupAlgebraInClass C hC R G) r)) =
263 completedGroupAlgebraProjection R G U (algebraMap R (Carrier R G) r)
265 change completedGroupAlgebraProjectionInClass C hC R G
266 (completedGroupAlgebraIndexToInClass G C hForm hG U)
267 (algebraMap R (CompletedGroupAlgebraInClass C hC R G) r) =
268 algebraMap R (CompletedGroupAlgebraStage R G U) r
269 exact completedGroupAlgebraProjectionInClass_algebraMap (R := R) (G := G) C hC
270 (completedGroupAlgebraIndexToInClass G C hForm hG U) r
272@[simp]
274 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
275 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : CompletedGroupAlgebraInClass C hC R G) :
276 completedGroupAlgebraFromInClassAlgHom (R := R) (G := G) C hC hForm hG x =
277 completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x :=
278 rfl
281 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
282 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
283 Continuous (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG) := by
284 let S := completedGroupAlgebraSystem R G
285 letI : ∀ U : CompletedGroupAlgebraIndex G, TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
286 fun U => S.topologicalSpace U
287 have hval : Continuous fun x : CompletedGroupAlgebraInClass C hC R G =>
288 fun U : CompletedGroupAlgebraIndex G =>
289 (show CompletedGroupAlgebraStage R G U from
290 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x).1 U) := by
291 apply continuous_pi
292 intro U
293 letI : TopologicalSpace
294 (CompletedGroupAlgebraStageInClass C R G (completedGroupAlgebraIndexToInClass G C hForm hG U)) :=
295 (completedGroupAlgebraSystemInClass C hC R G).topologicalSpace
296 (completedGroupAlgebraIndexToInClass G C hForm hG U)
297 change Continuous (completedGroupAlgebraProjectionInClass C hC R G
298 (completedGroupAlgebraIndexToInClass G C hForm hG U))
299 simpa using continuous_completedGroupAlgebraProjectionInClass
300 (R := R) (G := G) C hC (completedGroupAlgebraIndexToInClass G C hForm hG U)
301 exact Continuous.subtype_mk hval fun x =>
302 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x).2
304@[simp]
306 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
307 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : Carrier R G) :
308 completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG
309 (completedGroupAlgebraToInClass (R := R) (G := G) C hC x) = x := by
310 apply (completedGroupAlgebraSystem R G).ext
311 intro U
312 change completedGroupAlgebraProjection R G U
313 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG
314 (completedGroupAlgebraToInClass (R := R) (G := G) C hC x)) =
315 completedGroupAlgebraProjection R G U x
317 change x.1
319 (completedGroupAlgebraIndexToInClass G C hForm hG U)) = x.1 U
320 cases U
321 rfl
323@[simp]
325 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
326 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : CompletedGroupAlgebraInClass C hC R G) :
327 completedGroupAlgebraToInClass (R := R) (G := G) C hC
328 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x) = x := by
329 apply (completedGroupAlgebraSystemInClass C hC R G).ext
330 intro U
331 change completedGroupAlgebraProjectionInClass C hC R G U
332 (completedGroupAlgebraToInClass (R := R) (G := G) C hC
333 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x)) =
334 completedGroupAlgebraProjectionInClass C hC R G U x
336 change completedGroupAlgebraProjection R G
337 (completedGroupAlgebraIndexInClassToAllFinite G C hC U)
338 (completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x) =
339 completedGroupAlgebraProjectionInClass C hC R G U x
341 change x.1
342 (completedGroupAlgebraIndexToInClass G C hForm hG
343 (completedGroupAlgebraIndexInClassToAllFinite G C hC U)) = x.1 U
344 cases U
345 rfl
347@[simp]
349 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
350 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
351 (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG).comp
352 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC) =
353 RingHom.id (Carrier R G) := by
354 apply RingHom.ext
355 intro x
356 exact completedGroupAlgebraFromInClass_toInClass (R := R) (G := G) C hC hForm hG x
358@[simp]
360 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
361 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
362 (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC).comp
363 (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG) =
364 RingHom.id (CompletedGroupAlgebraInClass C hC R G) := by
365 apply RingHom.ext
366 intro x
367 exact completedGroupAlgebraToInClass_fromInClass (R := R) (G := G) C hC hForm hG x
369/-- For a pro-`C` group, the all-finite and `C`-indexed completed group algebras are the same
370ring, via the comparison maps. -/
372 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
373 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
374 Carrier R G ≃+* CompletedGroupAlgebraInClass C hC R G where
375 toFun := completedGroupAlgebraToInClass (R := R) (G := G) C hC
376 invFun := completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG
377 left_inv := by
378 intro x
379 exact completedGroupAlgebraFromInClass_toInClass (R := R) (G := G) C hC hForm hG x
380 right_inv := by
381 intro x
382 exact completedGroupAlgebraToInClass_fromInClass (R := R) (G := G) C hC hForm hG x
383 map_mul' := by
384 intro x y
385 exact map_mul (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC) x y
386 map_add' := by
387 intro x y
388 exact map_add (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC) x y
390@[simp]
392 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
393 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : Carrier R G) :
394 completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hC hForm hG x =
395 completedGroupAlgebraToInClass (R := R) (G := G) C hC x :=
396 rfl
398@[simp]
400 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
401 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : CompletedGroupAlgebraInClass C hC R G) :
402 (completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hC hForm hG).symm x =
403 completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x :=
404 rfl
406/-- For a pro-`C` group, the all-finite and `C`-indexed completed group algebras are the same
407`R`-algebra. -/
409 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
410 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
411 Carrier R G ≃ₐ[R] CompletedGroupAlgebraInClass C hC R G :=
412 AlgEquiv.ofRingEquiv (f := completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hC hForm hG)
413 (by
414 intro r
415 rfl)
417@[simp]
419 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
420 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : Carrier R G) :
421 completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hC hForm hG x =
422 completedGroupAlgebraToInClass (R := R) (G := G) C hC x :=
423 rfl
425@[simp]
427 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
428 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : CompletedGroupAlgebraInClass C hC R G) :
429 (completedGroupAlgebraInClassAlgEquiv (R := R) (G := G) C hC hForm hG).symm x =
430 completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x :=
431 rfl
433/-- The comparison equivalence is an equivalence of topological spaces. -/
435 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
436 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
437 Carrier R G ≃ₜ CompletedGroupAlgebraInClass C hC R G where
438 toEquiv := (completedGroupAlgebraInClassRingEquiv (R := R) (G := G) C hC hForm hG).toEquiv
439 continuous_toFun := continuous_completedGroupAlgebraToInClass (R := R) (G := G) C hC
440 continuous_invFun := continuous_completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG
442@[simp]
444 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
445 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : Carrier R G) :
446 completedGroupAlgebraInClassHomeomorph (R := R) (G := G) C hC hForm hG x =
447 completedGroupAlgebraToInClass (R := R) (G := G) C hC x :=
448 rfl
450@[simp]
452 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
453 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) (x : CompletedGroupAlgebraInClass C hC R G) :
454 (completedGroupAlgebraInClassHomeomorph (R := R) (G := G) C hC hForm hG).symm x =
455 completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x :=
456 rfl
459 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
460 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
461 Function.Surjective (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C hC) := by
462 intro x
463 refine ⟨completedGroupAlgebraFromInClass (R := R) (G := G) C hC hForm hG x, ?_⟩
464 exact completedGroupAlgebraToInClass_fromInClass (R := R) (G := G) C hC hForm hG x
467 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
468 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
469 Function.Surjective (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hC hForm hG) := by
470 intro x
471 refine ⟨completedGroupAlgebraToInClass (R := R) (G := G) C hC x, ?_⟩
472 exact completedGroupAlgebraFromInClass_toInClass (R := R) (G := G) C hC hForm hG x
474end