CompletedGroupAlgebra/Basic/AllFinite/Ring.lean
1import CompletedGroupAlgebra.Basic.AllFinite.Additive
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/Basic/AllFinite/Ring.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Ring and algebra structure
14This module builds the ring and algebra structure on the all-finite completed group algebra by coordinatewise operations on finite stages.
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]
33instance instOneCompletedGroupAlgebra : One (Carrier R G) where
34 one := ⟨fun U => (1 : CompletedGroupAlgebraStage R G U), by
35 intro U V hUV
36 change completedGroupAlgebraTransition R G hUV
37 (1 : CompletedGroupAlgebraStage R G V) = 1
38 exact map_one (completedGroupAlgebraTransition R G hUV)⟩
40instance instMulCompletedGroupAlgebra : Mul (Carrier R G) where
41 mul x y := ⟨fun U =>
42 (show CompletedGroupAlgebraStage R G U from x.1 U) *
43 (show CompletedGroupAlgebraStage R G U from y.1 U), by
44 intro U V hUV
45 calc
46 completedGroupAlgebraTransition R G hUV
47 ((show CompletedGroupAlgebraStage R G V from x.1 V) *
48 (show CompletedGroupAlgebraStage R G V from y.1 V))
49 =
50 completedGroupAlgebraTransition R G hUV
51 (show CompletedGroupAlgebraStage R G V from x.1 V) *
52 completedGroupAlgebraTransition R G hUV
53 (show CompletedGroupAlgebraStage R G V from y.1 V) := by
55 _ = (show CompletedGroupAlgebraStage R G U from x.1 U) *
56 (show CompletedGroupAlgebraStage R G U from y.1 U) := by
57 exact congrArg₂ HMul.hMul (x.2 U V hUV) (y.2 U V hUV)⟩
59instance instNatCastCompletedGroupAlgebra : NatCast (Carrier R G) where
60 natCast n := ⟨fun U => (n : CompletedGroupAlgebraStage R G U), by
61 intro U V hUV
62 change completedGroupAlgebraTransition R G hUV
63 (n : CompletedGroupAlgebraStage R G V) = n
64 exact map_natCast (completedGroupAlgebraTransition R G hUV) n⟩
66instance instIntCastCompletedGroupAlgebra : IntCast (Carrier R G) where
67 intCast n := ⟨fun U => (n : CompletedGroupAlgebraStage R G U), by
68 intro U V hUV
69 change completedGroupAlgebraTransition R G hUV
70 (n : CompletedGroupAlgebraStage R G V) = n
71 exact map_intCast (completedGroupAlgebraTransition R G hUV) n⟩
73instance instRingCompletedGroupAlgebraStage
74 (U : CompletedGroupAlgebraIndex G) :
75 Ring ((completedGroupAlgebraSystem R G).X U) := by
77 infer_instance
79instance instRingCompletedGroupAlgebraFamily :
80 Ring ((U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) :=
81 inferInstance
83instance instPowCompletedGroupAlgebra : Pow (Carrier R G) ℕ where
84 pow x n := ⟨fun U => (show CompletedGroupAlgebraStage R G U from x.1 U) ^ n, by
85 intro U V hUV
86 change completedGroupAlgebraTransition R G hUV
87 ((show CompletedGroupAlgebraStage R G V from x.1 V) ^ n) =
88 (show CompletedGroupAlgebraStage R G U from x.1 U) ^ n
89 rw [map_pow]
90 exact congrArg (fun t => t ^ n) (x.2 U V hUV)⟩
92/-- Coordinatewise coercion formula for the inverse-limit completed group algebra. -/
93@[simp]
94theorem coe_one_completedGroupAlgebra :
95 ((1 : Carrier R G) :
96 (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) = 1 := by
97 funext U
98 rfl
100/-- Coordinatewise coercion formula for the inverse-limit completed group algebra. -/
101@[simp]
102theorem coe_mul_completedGroupAlgebra (x y : Carrier R G) :
103 ((x * y : Carrier R G) :
104 (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
105 x * y := by
106 funext U
107 rfl
109/-- Coordinatewise coercion formula for the inverse-limit completed group algebra. -/
110@[simp]
111theorem coe_natCast_completedGroupAlgebra (n : ℕ) :
112 ((n : Carrier R G) :
113 (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
114 n := by
115 funext U
116 rfl
118/-- Coordinatewise coercion formula for the inverse-limit completed group algebra. -/
119@[simp]
120theorem coe_intCast_completedGroupAlgebra (n : ℤ) :
121 ((n : Carrier R G) :
122 (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
123 n := by
124 funext U
125 rfl
127/-- Coordinatewise coercion formula for the inverse-limit completed group algebra. -/
128@[simp]
129theorem coe_pow_completedGroupAlgebra (x : Carrier R G) (n : ℕ) :
130 ((x ^ n : Carrier R G) :
131 (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
132 x ^ n := by
133 funext U
134 rfl
136instance instRingCompletedGroupAlgebra : Ring (Carrier R G) :=
137 Function.Injective.ring
138 (fun x : Carrier R G =>
139 (x : (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U))
140 Subtype.val_injective
141 (coe_zero_completedGroupAlgebra (R := R) (G := G))
142 (coe_one_completedGroupAlgebra (R := R) (G := G))
143 (coe_add_completedGroupAlgebra (R := R) (G := G))
144 (coe_mul_completedGroupAlgebra (R := R) (G := G))
145 (coe_neg_completedGroupAlgebra (R := R) (G := G))
146 (coe_sub_completedGroupAlgebra (R := R) (G := G))
147 (fun n x => coe_nsmul_completedGroupAlgebra (R := R) (G := G) n x)
148 (fun n x => coe_zsmul_completedGroupAlgebra (R := R) (G := G) n x)
149 (fun x n => coe_pow_completedGroupAlgebra (R := R) (G := G) x n)
150 (by intro n; exact coe_natCast_completedGroupAlgebra (R := R) (G := G) n)
151 (by intro n; exact coe_intCast_completedGroupAlgebra (R := R) (G := G) n)
153/-- Change coefficients on the all-finite completed group algebra stagewise. -/
155 (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
156 (f : R →+* S) :
157 Carrier R G →+* Carrier S G where
158 toFun x := ⟨fun U => completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U (x.1 U), by
159 intro U V hUV
160 have hcompat := congrFun
161 (congrArg DFunLike.coe
163 (R := R) (G := G) S f hUV))
164 (x.1 V)
165 calc
166 completedGroupAlgebraTransition S G hUV
167 (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f V (x.1 V))
168 =
169 completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U
170 (completedGroupAlgebraTransition R G hUV (x.1 V)) := hcompat.symm
171 _ =
172 completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U (x.1 U) := by
173 exact congrArg (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U)
174 (x.2 U V hUV)⟩
175 map_zero' := by
176 apply Subtype.ext
177 funext U
178 exact map_zero (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U)
179 map_one' := by
180 apply Subtype.ext
181 funext U
182 exact map_one (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U)
183 map_add' x y := by
184 apply Subtype.ext
185 funext U
186 exact map_add (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U) (x.1 U) (y.1 U)
187 map_mul' x y := by
188 apply Subtype.ext
189 funext U
190 exact map_mul (completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U) (x.1 U) (y.1 U)
192@[simp]
194 (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
195 (f : R →+* S) (U : CompletedGroupAlgebraIndex G)
196 (x : Carrier R G) :
198 (completedGroupAlgebraCoeffMap (R := R) (G := G) S f x) =
199 completedGroupAlgebraStageCoeffMap (R := R) (G := G) S f U
200 (completedGroupAlgebraProjection R G U x) :=
201 rfl
203/-- The finite-stage projection preserves zero. -/
204@[simp]
205theorem completedGroupAlgebraProjection_zero (U : CompletedGroupAlgebraIndex G) :
206 completedGroupAlgebraProjection R G U (0 : Carrier R G) = 0 := rfl
208/-- The finite-stage projection preserves add. -/
209@[simp]
210theorem completedGroupAlgebraProjection_add (U : CompletedGroupAlgebraIndex G)
211 (x y : Carrier R G) :
212 completedGroupAlgebraProjection R G U (x + y) =
213 completedGroupAlgebraProjection R G U x + completedGroupAlgebraProjection R G U y := rfl
215/-- The finite-stage projection preserves smul. -/
216@[simp]
217theorem completedGroupAlgebraProjection_smul (U : CompletedGroupAlgebraIndex G)
218 (r : R) (x : Carrier R G) :
219 completedGroupAlgebraProjection R G U (r • x) =
220 r • completedGroupAlgebraProjection R G U x := rfl
222/-- The finite-stage projection preserves one. -/
223@[simp]
224theorem completedGroupAlgebraProjection_one (U : CompletedGroupAlgebraIndex G) :
225 completedGroupAlgebraProjection R G U (1 : Carrier R G) = 1 := rfl
227/-- The finite-stage projection preserves mul. -/
228@[simp]
229theorem completedGroupAlgebraProjection_mul (U : CompletedGroupAlgebraIndex G)
230 (x y : Carrier R G) :
231 completedGroupAlgebraProjection R G U (x * y) =
232 completedGroupAlgebraProjection R G U x * completedGroupAlgebraProjection R G U y := rfl
234omit [TopologicalSpace R] [IsTopologicalRing R] in
235/-- Transition maps preserve coefficient algebra-map elements. -/
237 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (r : R) :
238 completedGroupAlgebraTransition R G hUV
239 (algebraMap R (CompletedGroupAlgebraStage R G V) r) =
240 algebraMap R (CompletedGroupAlgebraStage R G U) r := by
241 simp only [completedGroupAlgebraTransition, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,
242 RingHom.coe_id, Function.comp_apply, id_eq, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, map_one]
244/-- The coefficient-ring map into the completed group algebra. -/
245def completedGroupAlgebraAlgebraMap (R : Type u) (G : Type v) [CommRing R]
246 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
247 [IsTopologicalGroup G] : R →+* Carrier R G where
248 toFun r := ⟨fun U => algebraMap R (CompletedGroupAlgebraStage R G U) r, by
249 intro U V hUV
250 exact completedGroupAlgebraTransition_algebraMap (R := R) (G := G) hUV r⟩
251 map_zero' := by
252 apply (completedGroupAlgebraSystem R G).ext
253 intro U
254 change algebraMap R (CompletedGroupAlgebraStage R G U) (0 : R) = 0
255 exact map_zero (algebraMap R (CompletedGroupAlgebraStage R G U))
256 map_one' := by
257 apply (completedGroupAlgebraSystem R G).ext
258 intro U
259 change algebraMap R (CompletedGroupAlgebraStage R G U) (1 : R) = 1
260 exact map_one (algebraMap R (CompletedGroupAlgebraStage R G U))
261 map_add' r s := by
262 apply (completedGroupAlgebraSystem R G).ext
263 intro U
264 change algebraMap R (CompletedGroupAlgebraStage R G U) (r + s) =
265 algebraMap R (CompletedGroupAlgebraStage R G U) r +
266 algebraMap R (CompletedGroupAlgebraStage R G U) s
267 exact map_add (algebraMap R (CompletedGroupAlgebraStage R G U)) r s
268 map_mul' r s := by
269 apply (completedGroupAlgebraSystem R G).ext
270 intro U
271 change algebraMap R (CompletedGroupAlgebraStage R G U) (r * s) =
272 algebraMap R (CompletedGroupAlgebraStage R G U) r *
273 algebraMap R (CompletedGroupAlgebraStage R G U) s
274 exact map_mul (algebraMap R (CompletedGroupAlgebraStage R G U)) r s
276instance instAlgebraCompletedGroupAlgebra : Algebra R (Carrier R G) where
277 algebraMap := completedGroupAlgebraAlgebraMap R G
278 commutes' := by
279 intro r x
280 apply (completedGroupAlgebraSystem R G).ext
281 intro U
282 change algebraMap R (CompletedGroupAlgebraStage R G U) r *
283 completedGroupAlgebraProjection R G U x =
284 completedGroupAlgebraProjection R G U x *
285 algebraMap R (CompletedGroupAlgebraStage R G U) r
286 exact Algebra.commutes r (completedGroupAlgebraProjection R G U x)
287 smul_def' := by
288 intro r x
289 apply (completedGroupAlgebraSystem R G).ext
290 intro U
291 change completedGroupAlgebraProjection R G U (r • x) =
292 completedGroupAlgebraProjection R G U (completedGroupAlgebraAlgebraMap R G r * x)
294 change r • completedGroupAlgebraProjection R G U x =
295 algebraMap R (CompletedGroupAlgebraStage R G U) r *
296 completedGroupAlgebraProjection R G U x
297 rw [Algebra.smul_def]
299end