CompletedGroupAlgebra/OpenFiniteQuotientTopology/OpenFiniteLimit/Algebra.lean
1import CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.System
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/OpenFiniteQuotientTopology/OpenFiniteLimit/Algebra.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
13-/
15open scoped Topology
17namespace CompletedGroupAlgebra
19noncomputable section
21open ProCGroups
22open ProCGroups.ProC
23open ProCGroups.InverseSystems
24open ProCGroups.Completion
26universe u v
28variable (R : Type u) [CommRing R] [TopologicalSpace R]
29variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
32 Zero (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
33 zero := ⟨fun K => (0 : CompletedGroupAlgebraOpenFiniteQuotientStage R G K), by
34 intro K L hKL
35 change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
36 (0 : CompletedGroupAlgebraOpenFiniteQuotientStage R G L) = 0
37 exact map_zero (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL)⟩
40 Add (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
42 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K) +
43 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from y.1 K), by
44 intro K L hKL
45 calc
47 ((show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L) +
48 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from y.1 L))
49 =
51 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L) +
53 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from y.1 L) := by
55 _ = (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K) +
56 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from y.1 K) := by
57 exact congrArg₂ HAdd.hAdd (x.2 K L hKL) (y.2 K L hKL)⟩
60 Neg (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
61 neg x := ⟨fun K => -(show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K), by
62 intro K L hKL
63 change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
64 (-(show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L)) =
65 -(show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K)
66 rw [map_neg]
67 exact congrArg Neg.neg (x.2 K L hKL)⟩
70 Sub (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
72 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K) -
73 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from y.1 K), by
74 intro K L hKL
75 change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
76 ((show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L) -
77 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from y.1 L)) =
78 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K) -
79 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from y.1 K)
80 rw [map_sub]
81 exact congrArg₂ HSub.hSub (x.2 K L hKL) (y.2 K L hKL)⟩
84 SMul ℕ (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
85 smul n x := ⟨fun K => n • (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K), by
86 intro K L hKL
87 change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
88 (n • (show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L)) =
89 n • (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K)
90 rw [map_nsmul]
91 exact congrArg (n • ·) (x.2 K L hKL)⟩
94 SMul ℤ (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
95 smul n x := ⟨fun K => n • (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K), by
96 intro K L hKL
97 change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
98 (n • (show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L)) =
99 n • (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K)
100 rw [map_zsmul]
101 exact congrArg (n • ·) (x.2 K L hKL)⟩
104 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
105 AddCommGroup ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
108 infer_instance
111 AddCommGroup
112 ((K : CompletedGroupAlgebraOpenQuotientIndex R G) →
113 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) :=
114 inferInstance
116/-- The coercion of zero in the open finite quotient limit is the zero family. -/
117@[simp]
119 ((0 : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
120 (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
121 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) = 0 := by
122 funext K
123 rfl
125/-- The coercion of a sum in the open finite quotient limit is computed coordinatewise. -/
126@[simp]
128 (x y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
129 ((x + y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
130 (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
131 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
132 x + y := by
133 funext K
134 rfl
136/-- The coercion of a negation in the open finite quotient limit is computed coordinatewise. -/
137@[simp]
139 (x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
140 ((-x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
141 (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
142 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
143 -x := by
144 funext K
145 rfl
147/-- The coercion of a subtraction in the open finite quotient limit is computed coordinatewise. -/
148@[simp]
150 (x y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
151 ((x - y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
152 (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
153 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
154 x - y := by
155 funext K
156 rfl
158/-- The coercion of a natural scalar multiple in the open finite quotient limit is coordinatewise. -/
159@[simp]
161 (n : ℕ) (x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
162 ((n • x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
163 (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
164 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
165 n • x := by
166 funext K
167 rfl
169/-- The coercion of an integer scalar multiple in the open finite quotient limit is coordinatewise. -/
170@[simp]
172 (n : ℤ) (x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
173 ((n • x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
174 (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
175 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
176 n • x := by
177 funext K
178 rfl
181 AddCommGroup (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
182 Function.Injective.addCommGroup
183 (fun x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G =>
184 (x : (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
185 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K))
186 Subtype.val_injective
187 (coe_zero_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
188 (coe_add_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
189 (coe_neg_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
190 (coe_sub_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
191 (fun x n => coe_nsmul_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G) n x)
192 (fun x n => coe_zsmul_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G) n x)
195 One (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
196 one := ⟨fun K => (1 : CompletedGroupAlgebraOpenFiniteQuotientStage R G K), by
197 intro K L hKL
198 change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
199 (1 : CompletedGroupAlgebraOpenFiniteQuotientStage R G L) = 1
200 exact map_one (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL)⟩
203 Mul (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
204 mul x y := ⟨fun K =>
205 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K) *
206 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from y.1 K), by
207 intro K L hKL
208 calc
210 ((show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L) *
211 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from y.1 L))
212 =
214 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L) *
216 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from y.1 L) := by
218 _ = (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K) *
219 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from y.1 K) := by
220 exact congrArg₂ HMul.hMul (x.2 K L hKL) (y.2 K L hKL)⟩
223 NatCast (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
224 natCast n := ⟨fun K => (n : CompletedGroupAlgebraOpenFiniteQuotientStage R G K), by
225 intro K L hKL
226 change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
227 (n : CompletedGroupAlgebraOpenFiniteQuotientStage R G L) = n
228 exact map_natCast (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL) n⟩
231 IntCast (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where
232 intCast n := ⟨fun K => (n : CompletedGroupAlgebraOpenFiniteQuotientStage R G K), by
233 intro K L hKL
234 change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
235 (n : CompletedGroupAlgebraOpenFiniteQuotientStage R G L) = n
236 exact map_intCast (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL) n⟩
239 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
240 Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
243 infer_instance
246 Ring ((K : CompletedGroupAlgebraOpenQuotientIndex R G) →
247 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) :=
248 inferInstance
251 Pow (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) ℕ where
252 pow x n := ⟨fun K => (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K) ^ n, by
253 intro K L hKL
254 change completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
255 ((show CompletedGroupAlgebraOpenFiniteQuotientStage R G L from x.1 L) ^ n) =
256 (show CompletedGroupAlgebraOpenFiniteQuotientStage R G K from x.1 K) ^ n
257 rw [map_pow]
258 exact congrArg (fun t => t ^ n) (x.2 K L hKL)⟩
260/-- The coercion of one in the open finite quotient limit is the one family. -/
261@[simp]
263 ((1 : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
264 (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
265 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) = 1 := by
266 funext K
267 rfl
269/-- The coercion of a product in the open finite quotient limit is computed coordinatewise. -/
270@[simp]
272 (x y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
273 ((x * y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
274 (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
275 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
276 x * y := by
277 funext K
278 rfl
280/-- Natural-number casts into the open finite quotient limit are computed coordinatewise. -/
281@[simp]
282theorem coe_natCast_completedGroupAlgebraOpenFiniteQuotientLimit (n : ℕ) :
283 ((n : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
284 (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
285 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
286 n := by
287 funext K
288 rfl
290/-- Integer casts into the open finite quotient limit are computed coordinatewise. -/
291@[simp]
292theorem coe_intCast_completedGroupAlgebraOpenFiniteQuotientLimit (n : ℤ) :
293 ((n : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
294 (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
295 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
296 n := by
297 funext K
298 rfl
300/-- Powers in the open finite quotient limit are computed coordinatewise. -/
301@[simp]
303 (x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) (n : ℕ) :
304 ((x ^ n : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
305 (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
306 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) =
307 x ^ n := by
308 funext K
309 rfl
312 Ring (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=
313 Function.Injective.ring
314 (fun x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G =>
315 (x : (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
316 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K))
317 Subtype.val_injective
318 (coe_zero_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
319 (coe_one_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
320 (coe_add_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
321 (coe_mul_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
322 (coe_neg_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
323 (coe_sub_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G))
324 (fun n x => coe_nsmul_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G) n x)
325 (fun n x => coe_zsmul_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G) n x)
326 (fun x n => coe_pow_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G) x n)
327 (by intro n; exact coe_natCast_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G) n)
328 (by intro n; exact coe_intCast_completedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G) n)
330/-- Projection from the open finite quotient limit sends zero to zero. -/
331@[simp]
333 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
335 (0 : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) = 0 := rfl
337/-- Projection from the open finite quotient limit preserves addition. -/
338@[simp]
340 (K : CompletedGroupAlgebraOpenQuotientIndex R G)
341 (x y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
342 completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K (x + y) =
344 completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K y := rfl
346/-- Projection from the open finite quotient limit preserves negation. -/
347@[simp]
349 (K : CompletedGroupAlgebraOpenQuotientIndex R G)
350 (x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
352 -completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K x := rfl
354/-- Projection from the open finite quotient limit preserves subtraction. -/
355@[simp]
357 (K : CompletedGroupAlgebraOpenQuotientIndex R G)
358 (x y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
359 completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K (x - y) =
361 completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K y := rfl
363/-- Projection from the open finite quotient limit sends one to one. -/
364@[simp]
366 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
368 (1 : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) = 1 := rfl
370/-- Projection from the open finite quotient limit preserves multiplication. -/
371@[simp]
373 (K : CompletedGroupAlgebraOpenQuotientIndex R G)
374 (x y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
375 completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K (x * y) =
377 completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K y := rfl
379/-- Projection from the two-parameter limit to one quotient, as a ring homomorphism. -/
381 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
382 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
383 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
385 CompletedGroupAlgebraOpenFiniteQuotientStage R G K where
386 toFun := completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K
387 map_zero' := completedGroupAlgebraOpenFiniteQuotientLimitProjection_zero (R := R) (G := G) K
388 map_one' := completedGroupAlgebraOpenFiniteQuotientLimitProjection_one (R := R) (G := G) K
389 map_add' := completedGroupAlgebraOpenFiniteQuotientLimitProjection_add (R := R) (G := G) K
390 map_mul' := completedGroupAlgebraOpenFiniteQuotientLimitProjection_mul (R := R) (G := G) K
392/-- The projection ring homomorphism has the same underlying function as the projection. -/
393@[simp]
395 [IsTopologicalRing R]
396 (K : CompletedGroupAlgebraOpenQuotientIndex R G)
397 (x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
400 rfl
403end