CompletedGroupAlgebra/Basic/InClass/LimitAlgebra.lean
1import CompletedGroupAlgebra.Basic.InClass.System
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/Basic/InClass/LimitAlgebra.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Class-Indexed Completed Group Algebras
14Finite-class-indexed inverse systems and inverse limits for completed group algebras.
15-/
17open scoped Topology
19namespace CompletedGroupAlgebra
21noncomputable section
23open ProCGroups
24open ProCGroups.ProC
25open ProCGroups.InverseSystems
27universe u v w
29variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
30variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
33/-- The `C`-indexed completed group algebra as an inverse limit of finite-stage group algebras. -/
34abbrev CompletedGroupAlgebraInClass
35 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
36 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
37 [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
38 Type (max u v) :=
39 (completedGroupAlgebraSystemInClass C hC R G).inverseLimit
42 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
43 Ring (CompletedGroupAlgebraInClass C hC R G) := by
44 change Ring (completedGroupAlgebraSystemInClass C hC R G).inverseLimit
45 infer_instance
47/-- Change coefficients on the `C`-indexed completed group algebra stagewise. -/
49 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
50 (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
51 (f : R →+* S) :
52 CompletedGroupAlgebraInClass C hC R G →+* CompletedGroupAlgebraInClass C hC S G where
53 toFun x := ⟨fun U =>
54 completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U (x.1 U), by
55 intro U V hUV
56 have hcompat := congrFun
57 (congrArg DFunLike.coe
59 (R := R) (G := G) C S f hUV))
60 (x.1 V)
61 calc
62 completedGroupAlgebraTransitionInClass C S G hUV
63 (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f V (x.1 V))
64 =
65 completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U
66 (completedGroupAlgebraTransitionInClass C R G hUV (x.1 V)) := hcompat.symm
67 _ =
68 completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U (x.1 U) := by
69 exact congrArg (completedGroupAlgebraStageCoeffMapInClass
70 (R := R) (G := G) C S f U) (x.2 U V hUV)⟩
71 map_zero' := by
72 apply Subtype.ext
73 funext U
74 exact map_zero (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)
75 map_one' := by
76 apply Subtype.ext
77 funext U
78 exact map_one (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)
79 map_add' x y := by
80 apply Subtype.ext
81 funext U
82 exact map_add (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)
83 (x.1 U) (y.1 U)
84 map_mul' x y := by
85 apply Subtype.ext
86 funext U
87 exact map_mul (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)
88 (x.1 U) (y.1 U)
91 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
92 SMul R (CompletedGroupAlgebraInClass C hC R G) where
93 smul r x := ⟨fun U =>
94 r • (show CompletedGroupAlgebraStageInClass C R G U from x.1 U), by
95 intro U V hUV
96 change completedGroupAlgebraTransitionInClass C R G hUV
97 (r • (show CompletedGroupAlgebraStageInClass C R G V from x.1 V)) =
98 r • (show CompletedGroupAlgebraStageInClass C R G U from x.1 U)
100 exact congrArg (r • ·) (x.2 U V hUV)⟩
102/-- Scalar multiplication in the inverse-limit algebra is computed stagewise. -/
103@[simp]
105 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
106 (r : R) (x : CompletedGroupAlgebraInClass C hC R G) :
107 ((r • x : CompletedGroupAlgebraInClass C hC R G) :
108 (U : CompletedGroupAlgebraIndexInClass G C) →
109 (completedGroupAlgebraSystemInClass C hC R G).X U) =
110 fun U => r • (show CompletedGroupAlgebraStageInClass C R G U from x.1 U) := by
111 funext U
112 rfl
114/-- Evaluation of a `C`-indexed completed group algebra element as a compatible family,
115bundled as an additive monoid homomorphism. -/
117 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
118 CompletedGroupAlgebraInClass C hC R G →+
119 ((U : CompletedGroupAlgebraIndexInClass G C) →
120 CompletedGroupAlgebraStageInClass C R G U) where
121 toFun x := fun U => (show CompletedGroupAlgebraStageInClass C R G U from x.1 U)
122 map_zero' := by
123 funext U
124 rfl
125 map_add' x y := by
126 funext U
127 rfl
130 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
131 Module R (CompletedGroupAlgebraInClass C hC R G) :=
132 Function.Injective.module R
133 (completedGroupAlgebraInClassValAddMonoidHom (R := R) (G := G) C hC)
134 (fun x y h => by
135 apply Subtype.ext
136 funext U
137 exact congrFun h U)
138 (fun r x => by
139 funext U
140 rfl)
142/-- The coefficient-ring map into the `C`-indexed completed group algebra. -/
144 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
145 R →+* CompletedGroupAlgebraInClass C hC R G where
146 toFun r := ⟨fun U => algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r, by
147 intro U V hUV
148 exact completedGroupAlgebraTransitionInClass_algebraMap (R := R) (G := G) C hUV r⟩
149 map_zero' := by
150 apply (completedGroupAlgebraSystemInClass C hC R G).ext
151 intro U
153 map_one' := by
154 apply (completedGroupAlgebraSystemInClass C hC R G).ext
155 intro U
157 map_add' r s := by
158 apply (completedGroupAlgebraSystemInClass C hC R G).ext
159 intro U
161 map_mul' r s := by
162 apply (completedGroupAlgebraSystemInClass C hC R G).ext
163 intro U
167 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C) :
168 Algebra R (CompletedGroupAlgebraInClass C hC R G) where
169 algebraMap := completedGroupAlgebraAlgebraMapInClass (R := R) (G := G) C hC
170 commutes' := by
171 intro r x
172 apply (completedGroupAlgebraSystemInClass C hC R G).ext
173 intro U
174 change algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r *
175 (show CompletedGroupAlgebraStageInClass C R G U from x.1 U) =
176 (show CompletedGroupAlgebraStageInClass C R G U from x.1 U) *
177 algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r
178 exact Algebra.commutes r (show CompletedGroupAlgebraStageInClass C R G U from x.1 U)
179 smul_def' := by
180 intro r x
181 apply (completedGroupAlgebraSystemInClass C hC R G).ext
182 intro U
183 change r • (show CompletedGroupAlgebraStageInClass C R G U from x.1 U) =
184 algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r *
185 (show CompletedGroupAlgebraStageInClass C R G U from x.1 U)
186 rw [Algebra.smul_def]
189end