ProCGroups/Completion/ProCGroupAlgebra.lean
1import Mathlib.Algebra.MonoidAlgebra.Basic
2import Mathlib.Data.Finsupp.Fintype
3import ProCGroups.Completion.ProCInteger
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/Completion/ProCGroupAlgebra.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Completed pro-C group algebras
16Builds completed group algebras from finite quotient stages and finite cyclic coefficient stages, with coordinatewise ring operations and projection formulas.
17-/
19open scoped Topology
21namespace ProCGroups.Completion
23noncomputable section
25universe u v
27variable (C : FiniteGroupClass.{u})
28variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
30/-- The open-normal quotient coordinate in the completed group-algebra indexing set. -/
31abbrev ProCCompletedGroupAlgebraQuotientIndex :=
32 OrderDual (ProC.OpenNormalSubgroupInClass C G)
34/-- The full indexing set: a coefficient modulus and a group quotient. -/
35abbrev ProCCompletedGroupAlgebraIndex :=
38/-- The quotient group `G/U` at one group-coordinate. -/
40 (U : ProCCompletedGroupAlgebraQuotientIndex C G) :=
41 (ProC.openNormalSubgroupInClassSystem C G).X U
43/-- The finite stage `(ZMod n)[G/U]`. -/
45 (i : ProCCompletedGroupAlgebraIndex C G) :=
46 MonoidAlgebra (ProCIntegerStage C i.1)
47 (ProCCompletedGroupAlgebraQuotient C G i.2)
49/-- Each finite group-algebra stage carries the discrete topology. -/
51 (i : ProCCompletedGroupAlgebraIndex C G) :
52 TopologicalSpace (ProCCompletedGroupAlgebraStage C G i) :=
53 ⊥
55/-- Each finite group-algebra stage is discrete. -/
57 (i : ProCCompletedGroupAlgebraIndex C G) :
58 DiscreteTopology (ProCCompletedGroupAlgebraStage C G i) :=
59 ⟨rfl⟩
61/-- The group quotient in each completed group-algebra coordinate is finite. -/
63 (U : ProCCompletedGroupAlgebraQuotientIndex C G) :
64 Finite (ProCCompletedGroupAlgebraQuotient C G U) := by
65 dsimp [ProCCompletedGroupAlgebraQuotient, ProC.openNormalSubgroupInClassSystem]
66 exact FiniteGroupClass.finite (C := C) (OrderDual.ofDual U).2
68/-- Each completed group-algebra stage is finite. -/
70 (i : ProCCompletedGroupAlgebraIndex C G) :
71 Finite (ProCCompletedGroupAlgebraStage C G i) := by
72 classical
73 letI : NeZero i.1.modulus := ⟨Nat.ne_of_gt i.1.positive⟩
74 letI : Fintype (ProCIntegerStage C i.1) := ZMod.fintype i.1.modulus
75 letI : Fintype (ProCCompletedGroupAlgebraQuotient C G i.2) := Fintype.ofFinite _
76 letI : DecidableEq (ProCCompletedGroupAlgebraQuotient C G i.2) := Classical.decEq _
78 change Finite (ProCCompletedGroupAlgebraQuotient C G i.2 →₀ ZMod i.1.modulus)
79 exact Finite.of_fintype _
81/-- The quotient transition map between the group coordinates. -/
83 {U V : ProCCompletedGroupAlgebraQuotientIndex C G} (hUV : U ≤ V) :
84 ProCCompletedGroupAlgebraQuotient C G V →*
85 ProCCompletedGroupAlgebraQuotient C G U :=
86 ProC.OpenNormalSubgroupInClass.map (C := C) (G := G)
87 (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV
89/-- The transition map `(ZMod m)[G/V] -> (ZMod n)[G/U]` for a refinement of coordinates. -/
91 {i j : ProCCompletedGroupAlgebraIndex C G} (hij : i ≤ j) :
92 ProCCompletedGroupAlgebraStage C G j →+*
93 ProCCompletedGroupAlgebraStage C G i :=
94 (MonoidAlgebra.mapDomainRingHom (ProCIntegerStage C i.1)
95 (proCCompletedGroupAlgebraQuotientTransition (C := C) (G := G) hij.2)).comp
96 (MonoidAlgebra.mapRangeRingHom
97 (ProCCompletedGroupAlgebraQuotient C G j.2)
98 (proCIntegerTransition (C := C) hij.1))
100/-- Compatibility condition for a point of the inverse limit defining the completed group algebra. -/
102 (x : ∀ i : ProCCompletedGroupAlgebraIndex C G,
103 ProCCompletedGroupAlgebraStage C G i) : Prop :=
104 ∀ i j, ∀ hij : i ≤ j,
105 proCCompletedGroupAlgebraTransition (C := C) (G := G) hij (x j) = x i
107/-- Explicit carrier-level name for the `ProCGroups`-side pro-`C` inverse-limit implementation of
109abbrev ProCCompletedGroupAlgebraLimitCarrier : Type _ :=
110 {x : ∀ i : ProCCompletedGroupAlgebraIndex C G,
111 ProCCompletedGroupAlgebraStage C G i //
114/-- The `ProCGroups`-side pro-`C` inverse-limit model of the completed group algebra, bundled with
115its topological ring structure and canonical coefficient and group maps.
119fields on the carrier bundle. -/
120structure ProCCompletedGroupAlgebraModel where
121 carrier : Type v
122 [ring : Ring carrier]
123 [topology : TopologicalSpace carrier]
124 [topologicalRing : IsTopologicalRing carrier]
125 compact : CompactSpace carrier
126 t2 : T2Space carrier
127 coeff : ProCIntegerLimitCarrier C →+* carrier
128 groupMap : G →* carrierˣ
130/-- Projection from the pro-`C` completed group-algebra carrier to a finite group-algebra stage. -/
131def proCCompletedGroupAlgebraProj (i : ProCCompletedGroupAlgebraIndex C G) :
133 fun x => x.1 i
135/-- Extensionality through finite group-algebra projections. -/
136@[ext]
137theorem ProCCompletedGroupAlgebraLimitCarrier.ext {x y : ProCCompletedGroupAlgebraLimitCarrier C G}
138 (h : ∀ i : ProCCompletedGroupAlgebraIndex C G,
139 proCCompletedGroupAlgebraProj (C := C) (G := G) i x =
140 proCCompletedGroupAlgebraProj (C := C) (G := G) i y) :
141 x = y :=
142 Subtype.ext (funext h)
144/-- The zero element of the completed group algebra is defined coordinatewise. -/
145instance instZeroProCCompletedGroupAlgebra :
146 Zero (ProCCompletedGroupAlgebraLimitCarrier C G) where
148 intro i j hij
149 exact map_zero (proCCompletedGroupAlgebraTransition (C := C) (G := G) hij)⟩
151/-- Addition on the completed group algebra is defined coordinatewise. -/
152instance instAddProCCompletedGroupAlgebra :
153 Add (ProCCompletedGroupAlgebraLimitCarrier C G) where
155 intro i j hij
157 exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩
159/-- Negation on the completed group algebra is defined coordinatewise. -/
160instance instNegProCCompletedGroupAlgebra :
161 Neg (ProCCompletedGroupAlgebraLimitCarrier C G) where
163 intro i j hij
164 rw [map_neg]
165 exact congrArg Neg.neg (x.2 i j hij)⟩
167/-- Subtraction on the completed group algebra is defined coordinatewise. -/
168instance instSubProCCompletedGroupAlgebra :
169 Sub (ProCCompletedGroupAlgebraLimitCarrier C G) where
171 intro i j hij
172 rw [map_sub]
173 exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩
175/-- Natural-number scalar multiplication on the completed group algebra is defined
176coordinatewise. -/
177instance instSMulNatProCCompletedGroupAlgebra :
178 SMul ℕ (ProCCompletedGroupAlgebraLimitCarrier C G) where
179 smul n x := ⟨fun i => n • x.1 i, by
180 intro i j hij
181 rw [map_nsmul]
182 exact congrArg (n • ·) (x.2 i j hij)⟩
184/-- Integer scalar multiplication on the completed group algebra is defined coordinatewise. -/
185instance instSMulIntProCCompletedGroupAlgebra :
186 SMul ℤ (ProCCompletedGroupAlgebraLimitCarrier C G) where
187 smul n x := ⟨fun i => n • x.1 i, by
188 intro i j hij
189 rw [map_zsmul]
190 exact congrArg (n • ·) (x.2 i j hij)⟩
192/-- The unit of the completed group algebra is defined coordinatewise. -/
193instance instOneProCCompletedGroupAlgebra :
194 One (ProCCompletedGroupAlgebraLimitCarrier C G) where
196 intro i j hij
197 exact map_one (proCCompletedGroupAlgebraTransition (C := C) (G := G) hij)⟩
199/-- Multiplication on the completed group algebra is defined coordinatewise. -/
200instance instMulProCCompletedGroupAlgebra :
201 Mul (ProCCompletedGroupAlgebraLimitCarrier C G) where
202 mul x y := ⟨fun i => x.1 i * y.1 i, by
203 intro i j hij
205 exact congrArg₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩
207/-- Natural-number casts into the completed group algebra are defined coordinatewise. -/
208instance instNatCastProCCompletedGroupAlgebra :
209 NatCast (ProCCompletedGroupAlgebraLimitCarrier C G) where
210 natCast n := ⟨fun _ => n, by
211 intro i j hij
212 exact map_natCast (proCCompletedGroupAlgebraTransition (C := C) (G := G) hij) n⟩
214/-- Integer casts into the completed group algebra are defined coordinatewise. -/
215instance instIntCastProCCompletedGroupAlgebra :
216 IntCast (ProCCompletedGroupAlgebraLimitCarrier C G) where
217 intCast n := ⟨fun _ => n, by
218 intro i j hij
219 exact map_intCast (proCCompletedGroupAlgebraTransition (C := C) (G := G) hij) n⟩
221/-- Powers in the completed group algebra are defined coordinatewise. -/
222instance instPowProCCompletedGroupAlgebra :
223 Pow (ProCCompletedGroupAlgebraLimitCarrier C G) ℕ where
224 pow x n := ⟨fun i => x.1 i ^ n, by
225 intro i j hij
226 rw [map_pow]
227 exact congrArg (fun t => t ^ n) (x.2 i j hij)⟩
229/-- The underlying compatible family of the completed group algebra computes zero coordinatewise. -/
230@[simp]
231theorem coe_zero_proCCompletedGroupAlgebra :
232 ((0 : ProCCompletedGroupAlgebraLimitCarrier C G) :
233 ∀ i : ProCCompletedGroupAlgebraIndex C G,
234 ProCCompletedGroupAlgebraStage C G i) = 0 := by
235 funext i
236 rfl
238/-- The underlying compatible family of the completed group algebra computes one coordinatewise. -/
239@[simp]
240theorem coe_one_proCCompletedGroupAlgebra :
241 ((1 : ProCCompletedGroupAlgebraLimitCarrier C G) :
242 ∀ i : ProCCompletedGroupAlgebraIndex C G,
243 ProCCompletedGroupAlgebraStage C G i) = 1 := by
244 funext i
245 rfl
247/-- The underlying compatible family of the completed group algebra computes addition coordinatewise. -/
248@[simp]
249theorem coe_add_proCCompletedGroupAlgebra (x y : ProCCompletedGroupAlgebraLimitCarrier C G) :
250 ((x + y : ProCCompletedGroupAlgebraLimitCarrier C G) :
251 ∀ i : ProCCompletedGroupAlgebraIndex C G,
252 ProCCompletedGroupAlgebraStage C G i) = x + y := by
253 funext i
254 rfl
256/-- The underlying compatible family of the completed group algebra computes multiplication coordinatewise. -/
257@[simp]
258theorem coe_mul_proCCompletedGroupAlgebra (x y : ProCCompletedGroupAlgebraLimitCarrier C G) :
259 ((x * y : ProCCompletedGroupAlgebraLimitCarrier C G) :
260 ∀ i : ProCCompletedGroupAlgebraIndex C G,
261 ProCCompletedGroupAlgebraStage C G i) = x * y := by
262 funext i
263 rfl
265/-- The underlying compatible family of the completed group algebra computes negation coordinatewise. -/
266@[simp]
267theorem coe_neg_proCCompletedGroupAlgebra (x : ProCCompletedGroupAlgebraLimitCarrier C G) :
268 ((-x : ProCCompletedGroupAlgebraLimitCarrier C G) :
269 ∀ i : ProCCompletedGroupAlgebraIndex C G,
270 ProCCompletedGroupAlgebraStage C G i) = -x := by
271 funext i
272 rfl
274/-- The underlying compatible family of the completed group algebra computes subtraction coordinatewise. -/
275@[simp]
276theorem coe_sub_proCCompletedGroupAlgebra (x y : ProCCompletedGroupAlgebraLimitCarrier C G) :
277 ((x - y : ProCCompletedGroupAlgebraLimitCarrier C G) :
278 ∀ i : ProCCompletedGroupAlgebraIndex C G,
279 ProCCompletedGroupAlgebraStage C G i) = x - y := by
280 funext i
281 rfl
283/-- The underlying compatible family of the completed group algebra computes natural-number casts coordinatewise. -/
284@[simp]
285theorem coe_natCast_proCCompletedGroupAlgebra (n : ℕ) :
286 ((n : ProCCompletedGroupAlgebraLimitCarrier C G) :
287 ∀ i : ProCCompletedGroupAlgebraIndex C G,
288 ProCCompletedGroupAlgebraStage C G i) = n := by
289 funext i
290 rfl
292/-- The underlying compatible family of the completed group algebra computes integer casts coordinatewise. -/
293@[simp]
294theorem coe_intCast_proCCompletedGroupAlgebra (n : ℤ) :
295 ((n : ProCCompletedGroupAlgebraLimitCarrier C G) :
296 ∀ i : ProCCompletedGroupAlgebraIndex C G,
297 ProCCompletedGroupAlgebraStage C G i) =
298 fun i => (n : ProCCompletedGroupAlgebraStage C G i) := by
299 funext i
300 rfl
302/-- The underlying compatible family of the completed group algebra computes powers coordinatewise. -/
303@[simp]
304theorem coe_pow_proCCompletedGroupAlgebra (x : ProCCompletedGroupAlgebraLimitCarrier C G) (n : ℕ) :
305 ((x ^ n : ProCCompletedGroupAlgebraLimitCarrier C G) :
306 ∀ i : ProCCompletedGroupAlgebraIndex C G,
307 ProCCompletedGroupAlgebraStage C G i) = x ^ n := by
308 funext i
309 rfl
311/-- The completed group algebra is a ring by coordinatewise operations on finite stages. -/
312instance instRingProCCompletedGroupAlgebra : Ring (ProCCompletedGroupAlgebraLimitCarrier C G) :=
313 Function.Injective.ring
314 (fun x : ProCCompletedGroupAlgebraLimitCarrier C G =>
315 (x : ∀ i : ProCCompletedGroupAlgebraIndex C G,
316 ProCCompletedGroupAlgebraStage C G i))
317 Subtype.val_injective
318 (coe_zero_proCCompletedGroupAlgebra (C := C) (G := G))
319 (coe_one_proCCompletedGroupAlgebra (C := C) (G := G))
320 (coe_add_proCCompletedGroupAlgebra (C := C) (G := G))
321 (coe_mul_proCCompletedGroupAlgebra (C := C) (G := G))
322 (coe_neg_proCCompletedGroupAlgebra (C := C) (G := G))
323 (coe_sub_proCCompletedGroupAlgebra (C := C) (G := G))
324 (by intro n x; funext i; change (n • x).1 i = n • x.1 i; rfl)
325 (by intro n x; funext i; change (n • x).1 i = n • x.1 i; rfl)
326 (coe_pow_proCCompletedGroupAlgebra (C := C) (G := G))
327 (coe_natCast_proCCompletedGroupAlgebra (C := C) (G := G))
328 (coe_intCast_proCCompletedGroupAlgebra (C := C) (G := G))
330/-- Finite group-algebra projections commute with `0`. -/
331@[simp]
333 (i : ProCCompletedGroupAlgebraIndex C G) :
334 proCCompletedGroupAlgebraProj (C := C) (G := G) i
335 (0 : ProCCompletedGroupAlgebraLimitCarrier C G) = 0 :=
336 by rfl
338/-- Finite group-algebra projections commute with `1`. -/
339@[simp]
341 (i : ProCCompletedGroupAlgebraIndex C G) :
342 proCCompletedGroupAlgebraProj (C := C) (G := G) i
343 (1 : ProCCompletedGroupAlgebraLimitCarrier C G) = 1 :=
344 by rfl
346/-- Finite group-algebra projections commute with addition. -/
347@[simp]
349 (i : ProCCompletedGroupAlgebraIndex C G) (x y : ProCCompletedGroupAlgebraLimitCarrier C G) :
350 proCCompletedGroupAlgebraProj (C := C) (G := G) i (x + y) =
351 proCCompletedGroupAlgebraProj (C := C) (G := G) i x +
352 proCCompletedGroupAlgebraProj (C := C) (G := G) i y :=
353 by rfl
355/-- Finite group-algebra projections commute with multiplication. -/
356@[simp]
358 (i : ProCCompletedGroupAlgebraIndex C G) (x y : ProCCompletedGroupAlgebraLimitCarrier C G) :
359 proCCompletedGroupAlgebraProj (C := C) (G := G) i (x * y) =
360 proCCompletedGroupAlgebraProj (C := C) (G := G) i x *
361 proCCompletedGroupAlgebraProj (C := C) (G := G) i y :=
362 by rfl
364/-- Finite group-algebra projections commute with negation. -/
365@[simp]
367 (i : ProCCompletedGroupAlgebraIndex C G) (x : ProCCompletedGroupAlgebraLimitCarrier C G) :
368 proCCompletedGroupAlgebraProj (C := C) (G := G) i (-x) =
369 -proCCompletedGroupAlgebraProj (C := C) (G := G) i x :=
370 by rfl
372/-- Finite group-algebra projections commute with subtraction. -/
373@[simp]
375 (i : ProCCompletedGroupAlgebraIndex C G) (x y : ProCCompletedGroupAlgebraLimitCarrier C G) :
376 proCCompletedGroupAlgebraProj (C := C) (G := G) i (x - y) =
377 proCCompletedGroupAlgebraProj (C := C) (G := G) i x -
378 proCCompletedGroupAlgebraProj (C := C) (G := G) i y :=
379 by rfl
381/-- Projection from the completed group algebra to a finite group-algebra stage as a ring homomorphism. -/
383 (i : ProCCompletedGroupAlgebraIndex C G) :
384 ProCCompletedGroupAlgebraLimitCarrier C G →+* ProCCompletedGroupAlgebraStage C G i where
385 toFun := proCCompletedGroupAlgebraProj (C := C) (G := G) i
386 map_zero' := by simp only [proCCompletedGroupAlgebraProj_zero]
387 map_one' := by simp only [proCCompletedGroupAlgebraProj_one]
388 map_add' := by intro x y; simp only [proCCompletedGroupAlgebraProj_add]
389 map_mul' := by intro x y; simp only [proCCompletedGroupAlgebraProj_mul]
391/-- The ring-hom version of a completed group-algebra projection evaluates to the projection map. -/
392@[simp]
394 (i : ProCCompletedGroupAlgebraIndex C G) (x : ProCCompletedGroupAlgebraLimitCarrier C G) :
395 proCCompletedGroupAlgebraProjRingHom (C := C) (G := G) i x =
396 proCCompletedGroupAlgebraProj (C := C) (G := G) i x :=
397 rfl
399/-- Each finite projection from the completed group algebra is continuous. -/
401 (i : ProCCompletedGroupAlgebraIndex C G) :
402 Continuous (proCCompletedGroupAlgebraProj (C := C) (G := G) i) :=
403 (continuous_apply i).comp continuous_subtype_val
405/-- Compatibility of the finite projections with completed group-algebra transition maps. -/
407 {i j : ProCCompletedGroupAlgebraIndex C G} (hij : i ≤ j)
408 (x : ProCCompletedGroupAlgebraLimitCarrier C G) :
409 proCCompletedGroupAlgebraTransition (C := C) (G := G) hij
410 (proCCompletedGroupAlgebraProj (C := C) (G := G) j x) =
411 proCCompletedGroupAlgebraProj (C := C) (G := G) i x :=
412 x.2 i j hij
414/-- The compatibility condition defining the completed group algebra is closed in the product of
417 IsClosed {x : ∀ i : ProCCompletedGroupAlgebraIndex C G,
418 ProCCompletedGroupAlgebraStage C G i |
419 ProCCompletedGroupAlgebraCompatible C G x} := by
420 simp only [ProCCompletedGroupAlgebraCompatible, Set.setOf_forall]
421 refine isClosed_iInter fun i => isClosed_iInter fun j => isClosed_iInter fun hij => ?_
422 have hleft :
423 Continuous fun x : (∀ k : ProCCompletedGroupAlgebraIndex C G,
424 ProCCompletedGroupAlgebraStage C G k) =>
425 proCCompletedGroupAlgebraTransition (C := C) (G := G) hij (x j) := by
426 exact (continuous_of_discreteTopology :
427 Continuous (proCCompletedGroupAlgebraTransition (C := C) (G := G) hij)).comp
428 (continuous_apply j)
429 exact isClosed_eq hleft (continuous_apply i)
431/-- The completed group-algebra limit carrier is compact as a closed subspace of a product of
434 CompactSpace (ProCCompletedGroupAlgebraLimitCarrier C G) := by
435 letI : ∀ i : ProCCompletedGroupAlgebraIndex C G,
436 CompactSpace (ProCCompletedGroupAlgebraStage C G i) := fun _ => inferInstance
437 let hs : IsClosed {x : ∀ i : ProCCompletedGroupAlgebraIndex C G,
438 ProCCompletedGroupAlgebraStage C G i |
439 ProCCompletedGroupAlgebraCompatible C G x} :=
440 isClosed_setOf_completedGroupAlgebraCompatible (C := C) (G := G)
441 simpa [ProCCompletedGroupAlgebraLimitCarrier] using hs.isClosedEmbedding_subtypeVal.compactSpace
443/-- The completed group-algebra limit carrier is Hausdorff. -/
445 T2Space (ProCCompletedGroupAlgebraLimitCarrier C G) := by
446 change T2Space {x : ∀ i : ProCCompletedGroupAlgebraIndex C G,
447 ProCCompletedGroupAlgebraStage C G i //
449 infer_instance
451/-- Addition on the completed group-algebra limit carrier is continuous coordinatewise. -/
453 ContinuousAdd (ProCCompletedGroupAlgebraLimitCarrier C G) where
454 continuous_add := by
455 refine Continuous.subtype_mk (continuous_pi fun i => ?_) (fun p => (p.1 + p.2).2)
456 change Continuous fun p : ProCCompletedGroupAlgebraLimitCarrier C G ×
458 proCCompletedGroupAlgebraProj (C := C) (G := G) i p.1 +
459 proCCompletedGroupAlgebraProj (C := C) (G := G) i p.2
460 exact ((continuous_proCCompletedGroupAlgebraProj (C := C) (G := G) i).comp
462 ((continuous_proCCompletedGroupAlgebraProj (C := C) (G := G) i).comp continuous_snd)
464/-- Multiplication on the completed group-algebra limit carrier is continuous coordinatewise. -/
466 ContinuousMul (ProCCompletedGroupAlgebraLimitCarrier C G) where
467 continuous_mul := by
468 refine Continuous.subtype_mk (continuous_pi fun i => ?_) (fun p => (p.1 * p.2).2)
469 change Continuous fun p : ProCCompletedGroupAlgebraLimitCarrier C G ×
471 proCCompletedGroupAlgebraProj (C := C) (G := G) i p.1 *
472 proCCompletedGroupAlgebraProj (C := C) (G := G) i p.2
473 exact ((continuous_proCCompletedGroupAlgebraProj (C := C) (G := G) i).comp
474 continuous_fst).mul
475 ((continuous_proCCompletedGroupAlgebraProj (C := C) (G := G) i).comp continuous_snd)
477/-- Negation on the completed group-algebra limit carrier is continuous coordinatewise. -/
479 ContinuousNeg (ProCCompletedGroupAlgebraLimitCarrier C G) where
480 continuous_neg := by
481 refine Continuous.subtype_mk (continuous_pi fun i => ?_) (fun x => (-x).2)
482 change Continuous fun x : ProCCompletedGroupAlgebraLimitCarrier C G =>
483 -proCCompletedGroupAlgebraProj (C := C) (G := G) i x
484 exact (continuous_proCCompletedGroupAlgebraProj (C := C) (G := G) i).neg
486/-- The completed group-algebra limit carrier is a topological ring. -/
487instance ProCCompletedGroupAlgebraLimitCarrier.instIsTopologicalRing :
488 IsTopologicalRing (ProCCompletedGroupAlgebraLimitCarrier C G) := by
489 letI : ContinuousAdd (ProCCompletedGroupAlgebraLimitCarrier C G) :=
490 instContinuousAddProCCompletedGroupAlgebraLimitCarrier (C := C) (G := G)
491 letI : ContinuousMul (ProCCompletedGroupAlgebraLimitCarrier C G) :=
492 instContinuousMulProCCompletedGroupAlgebraLimitCarrier (C := C) (G := G)
493 letI : ContinuousNeg (ProCCompletedGroupAlgebraLimitCarrier C G) :=
494 instContinuousNegProCCompletedGroupAlgebraLimitCarrier (C := C) (G := G)
495 letI : IsTopologicalSemiring (ProCCompletedGroupAlgebraLimitCarrier C G) :=
496 IsTopologicalSemiring.mk
497 exact IsTopologicalRing.mk
499/-- The coefficient embedding into the completed group algebra. -/
501 ProCIntegerLimitCarrier C →+* ProCCompletedGroupAlgebraLimitCarrier C G where
502 toFun z := ⟨fun i =>
503 algebraMap (ProCIntegerStage C i.1) (ProCCompletedGroupAlgebraStage C G i)
504 (proCIntegerProj (C := C) i.1 z), by
505 intro i j hij
506 simp only [proCCompletedGroupAlgebraTransition, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,
507 RingHom.coe_id, Function.comp_apply, id_eq, RingHom.coe_comp, MonoidAlgebra.mapRangeRingHom_single,
508 proCIntegerProj_transition (C := C) hij.1 z, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single,
510 map_zero' := by
511 apply ProCCompletedGroupAlgebraLimitCarrier.ext
512 intro i
513 exact map_zero (algebraMap (ProCIntegerStage C i.1)
514 (ProCCompletedGroupAlgebraStage C G i))
515 map_one' := by
516 apply ProCCompletedGroupAlgebraLimitCarrier.ext
517 intro i
518 exact map_one (algebraMap (ProCIntegerStage C i.1)
519 (ProCCompletedGroupAlgebraStage C G i))
520 map_add' := by
521 intro x y
522 apply ProCCompletedGroupAlgebraLimitCarrier.ext
523 intro i
524 exact map_add (algebraMap (ProCIntegerStage C i.1)
525 (ProCCompletedGroupAlgebraStage C G i))
526 (proCIntegerProj (C := C) i.1 x) (proCIntegerProj (C := C) i.1 y)
527 map_mul' := by
528 intro x y
529 apply ProCCompletedGroupAlgebraLimitCarrier.ext
530 intro i
531 exact map_mul (algebraMap (ProCIntegerStage C i.1)
532 (ProCCompletedGroupAlgebraStage C G i))
533 (proCIntegerProj (C := C) i.1 x) (proCIntegerProj (C := C) i.1 y)
535/-- Projecting the coefficient embedding into the completed group algebra applies the stage algebra map. -/
536@[simp]
538 (i : ProCCompletedGroupAlgebraIndex C G) (z : ProCIntegerLimitCarrier C) :
539 proCCompletedGroupAlgebraProj (C := C) (G := G) i
540 (proCIntegerToProCCompletedGroupAlgebra (C := C) (G := G) z) =
541 algebraMap (ProCIntegerStage C i.1) (ProCCompletedGroupAlgebraStage C G i)
542 (proCIntegerProj (C := C) i.1 z) :=
543 rfl
545/-- The completed group-algebra limit carrier is an algebra over its pro-`C` coefficient ring. -/
547 Algebra (ProCIntegerLimitCarrier C) (ProCCompletedGroupAlgebraLimitCarrier C G) :=
548 RingHom.toAlgebra'
549 (proCIntegerToProCCompletedGroupAlgebra (C := C) (G := G))
550 (by
551 intro z x
552 apply ProCCompletedGroupAlgebraLimitCarrier.ext
553 intro i
554 change
555 algebraMap (ProCIntegerStage C i.1) (ProCCompletedGroupAlgebraStage C G i)
556 (proCIntegerProj (C := C) i.1 z) *
557 proCCompletedGroupAlgebraProj (C := C) (G := G) i x =
558 proCCompletedGroupAlgebraProj (C := C) (G := G) i x *
559 algebraMap (ProCIntegerStage C i.1) (ProCCompletedGroupAlgebraStage C G i)
560 (proCIntegerProj (C := C) i.1 z)
561 exact Algebra.commutes _ _)
563/-- The canonical group map into the completed group algebra, sending `g` to its compatible system of group
564basis elements. -/
565def proCCompletedGroupAlgebraOf : G →* ProCCompletedGroupAlgebraLimitCarrier C G where
566 toFun g := ⟨fun i =>
567 MonoidAlgebra.of (ProCIntegerStage C i.1)
568 (ProCCompletedGroupAlgebraQuotient C G i.2)
569 (ProC.openNormalSubgroupInClassProj (C := C) (G := G) i.2 g), by
570 intro i j hij
571 have hq :=
572 congrFun (ProC.openNormalSubgroupInClassProj_compatible
573 (C := C) (G := G) i.2 j.2 hij.2) g
576 congrArg (fun q =>
577 MonoidAlgebra.of (ProCIntegerStage C i.1)
578 (ProCCompletedGroupAlgebraQuotient C G i.2) q) hq⟩
579 map_one' := by
580 apply ProCCompletedGroupAlgebraLimitCarrier.ext
581 intro i
582 change
583 MonoidAlgebra.of (ProCIntegerStage C i.1)
584 (ProCCompletedGroupAlgebraQuotient C G i.2)
585 (ProC.openNormalSubgroupInClassProj (C := C) (G := G) i.2 1) =
586 1
587 rfl
588 map_mul' g h := by
589 apply ProCCompletedGroupAlgebraLimitCarrier.ext
590 intro i
591 change
592 MonoidAlgebra.of (ProCIntegerStage C i.1)
593 (ProCCompletedGroupAlgebraQuotient C G i.2)
594 (ProC.openNormalSubgroupInClassProj (C := C) (G := G) i.2 (g * h)) =
595 MonoidAlgebra.of (ProCIntegerStage C i.1)
596 (ProCCompletedGroupAlgebraQuotient C G i.2)
597 (ProC.openNormalSubgroupInClassProj (C := C) (G := G) i.2 g) *
598 MonoidAlgebra.of (ProCIntegerStage C i.1)
599 (ProCCompletedGroupAlgebraQuotient C G i.2)
600 (ProC.openNormalSubgroupInClassProj (C := C) (G := G) i.2 h)
601 simp only [ProC.openNormalSubgroupInClassProj, QuotientGroup.mk'_apply, QuotientGroup.mk_mul,
602 MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one]
604/-- Projecting a group element into the completed group algebra gives the corresponding finite basis element. -/
605@[simp]
607 (i : ProCCompletedGroupAlgebraIndex C G) (g : G) :
608 proCCompletedGroupAlgebraProj (C := C) (G := G) i
609 (proCCompletedGroupAlgebraOf (C := C) (G := G) g) =
610 MonoidAlgebra.of (ProCIntegerStage C i.1)
611 (ProCCompletedGroupAlgebraQuotient C G i.2)
612 (ProC.openNormalSubgroupInClassProj (C := C) (G := G) i.2 g) :=
613 rfl
615/-- A group element gives a unit in the completed group-algebra limit carrier. -/
616def groupBasisUnit (g : G) : (ProCCompletedGroupAlgebraLimitCarrier C G)ˣ where
617 val := proCCompletedGroupAlgebraOf (C := C) (G := G) g
618 inv := proCCompletedGroupAlgebraOf (C := C) (G := G) g⁻¹
619 val_inv := by
622 inv_val := by
626/-- The canonical map from `G` to units in the completed group-algebra limit carrier. -/
627def ProCCompletedGroupAlgebraModel.groupToUnits : G →* (ProCCompletedGroupAlgebraLimitCarrier C G)ˣ where
628 toFun := groupBasisUnit (C := C) (G := G)
629 map_one' := by
630 ext
631 simp only [groupBasisUnit, map_one, inv_one, proCCompletedGroupAlgebraProj_one, Units.val_one]
632 map_mul' g h := by
633 ext
634 simp only [groupBasisUnit, map_mul, mul_inv_rev, proCCompletedGroupAlgebraProj_mul,
635 proCCompletedGroupAlgebraProj_of, MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one, Units.val_mul]
637namespace ProCCompletedGroupAlgebraModel
639/-- Compatible maps into the finite stages lift to the completed group-algebra limit carrier. -/
640def lift
641 {R : Type v} [Ring R] [TopologicalSpace R] [IsTopologicalRing R]
642 (f : ∀ i : ProCCompletedGroupAlgebraIndex C G,
643 R →+* ProCCompletedGroupAlgebraStage C G i)
644 (hf_compat : ∀ i j (hij : i ≤ j),
645 (proCCompletedGroupAlgebraTransition (C := C) (G := G) hij).comp (f j) = f i) :
646 R →+* ProCCompletedGroupAlgebraLimitCarrier C G where
647 toFun r := ⟨fun i => f i r, by
648 intro i j hij
649 exact congrArg (fun φ : R →+* ProCCompletedGroupAlgebraStage C G i => φ r)
650 (hf_compat i j hij)⟩
651 map_zero' := by
652 apply ProCCompletedGroupAlgebraLimitCarrier.ext
653 intro i
655 map_one' := by
656 apply ProCCompletedGroupAlgebraLimitCarrier.ext
657 intro i
659 map_add' := by
660 intro x y
661 apply ProCCompletedGroupAlgebraLimitCarrier.ext
662 intro i
664 map_mul' := by
665 intro x y
666 apply ProCCompletedGroupAlgebraLimitCarrier.ext
667 intro i
672/-- The inverse-limit carrier bundled as a completed group-algebra object. -/
674 ProCCompletedGroupAlgebraModel C G where
675 carrier := ProCCompletedGroupAlgebraLimitCarrier C G
676 ring := inferInstance
677 topology := inferInstance
678 topologicalRing := inferInstance
679 compact := inferInstance
680 t2 := inferInstance
681 coeff := proCIntegerToProCCompletedGroupAlgebra (C := C) (G := G)
682 groupMap := ProCCompletedGroupAlgebraModel.groupToUnits (C := C) (G := G)
684end
686end ProCGroups.Completion