CompletedGroupAlgebra/Basic/AllFinite/Additive.lean
1import CompletedGroupAlgebra.Basic.AllFinite.Stage
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/Basic/AllFinite/Additive.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Additive and module structure
14This module constructs the additive and module structures on the all-finite completed group algebra by transporting the finite-stage structures through the inverse limit.
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/-- The completed group algebra carrier `[[R G]] = lim_U R[G/U]`, as in RZ §5.3. -/
34abbrev Carrier (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
35 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
36 Type (max u v) :=
37 (completedGroupAlgebraSystem R G).inverseLimit
39/-- Projection from `[[R G]]` to one finite-stage group algebra `R[G/U]`. -/
40abbrev completedGroupAlgebraProjection (R : Type u) (G : Type v) [CommRing R]
41 [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
42 [IsTopologicalGroup G]
43 (U : CompletedGroupAlgebraIndex G) :
44 Carrier R G → CompletedGroupAlgebraStage R G U :=
45 (completedGroupAlgebraSystem R G).projection U
47instance instZeroCompletedGroupAlgebra : Zero (Carrier R G) where
48 zero := ⟨fun U => (0 : CompletedGroupAlgebraStage R G U), by
49 intro U V hUV
50 change completedGroupAlgebraTransition R G hUV
51 (0 : CompletedGroupAlgebraStage R G V) = 0
52 exact map_zero (completedGroupAlgebraTransition R G hUV)⟩
54instance instAddCompletedGroupAlgebra : Add (Carrier R G) where
56 (show CompletedGroupAlgebraStage R G U from x.1 U) +
57 (show CompletedGroupAlgebraStage R G U from y.1 U), by
58 intro U V hUV
59 calc
60 completedGroupAlgebraTransition R G hUV
61 ((show CompletedGroupAlgebraStage R G V from x.1 V) +
62 (show CompletedGroupAlgebraStage R G V from y.1 V))
63 =
64 completedGroupAlgebraTransition R G hUV
65 (show CompletedGroupAlgebraStage R G V from x.1 V) +
66 completedGroupAlgebraTransition R G hUV
67 (show CompletedGroupAlgebraStage R G V from y.1 V) := by
69 _ = (show CompletedGroupAlgebraStage R G U from x.1 U) +
70 (show CompletedGroupAlgebraStage R G U from y.1 U) := by
71 exact congrArg₂ HAdd.hAdd (x.2 U V hUV) (y.2 U V hUV)⟩
73instance instAddZeroClassCompletedGroupAlgebra : AddZeroClass (Carrier R G) where
76 zero_add x := by
77 apply Subtype.ext
78 funext U
79 change (0 : CompletedGroupAlgebraStage R G U) +
80 (show CompletedGroupAlgebraStage R G U from x.1 U) =
81 (show CompletedGroupAlgebraStage R G U from x.1 U)
82 simp only [zero_add]
83 add_zero x := by
84 apply Subtype.ext
85 funext U
86 change (show CompletedGroupAlgebraStage R G U from x.1 U) +
87 (0 : CompletedGroupAlgebraStage R G U) =
88 (show CompletedGroupAlgebraStage R G U from x.1 U)
89 simp only [add_zero]
91instance instNegCompletedGroupAlgebra : Neg (Carrier R G) where
92 neg x := ⟨fun U => -(show CompletedGroupAlgebraStage R G U from x.1 U), by
93 intro U V hUV
94 change completedGroupAlgebraTransition R G hUV
95 (-(show CompletedGroupAlgebraStage R G V from x.1 V)) =
96 -(show CompletedGroupAlgebraStage R G U from x.1 U)
97 rw [map_neg]
98 exact congrArg Neg.neg (x.2 U V hUV)⟩
100instance instSubCompletedGroupAlgebra : Sub (Carrier R G) where
102 (show CompletedGroupAlgebraStage R G U from x.1 U) -
103 (show CompletedGroupAlgebraStage R G U from y.1 U), by
104 intro U V hUV
105 change completedGroupAlgebraTransition R G hUV
106 ((show CompletedGroupAlgebraStage R G V from x.1 V) -
107 (show CompletedGroupAlgebraStage R G V from y.1 V)) =
108 (show CompletedGroupAlgebraStage R G U from x.1 U) -
109 (show CompletedGroupAlgebraStage R G U from y.1 U)
110 rw [map_sub]
111 exact congrArg₂ HSub.hSub (x.2 U V hUV) (y.2 U V hUV)⟩
113instance instSMulNatCompletedGroupAlgebra : SMul ℕ (Carrier R G) where
114 smul n x := ⟨fun U => n • (show CompletedGroupAlgebraStage R G U from x.1 U), by
115 intro U V hUV
116 change completedGroupAlgebraTransition R G hUV
117 (n • (show CompletedGroupAlgebraStage R G V from x.1 V)) =
118 n • (show CompletedGroupAlgebraStage R G U from x.1 U)
119 rw [map_nsmul]
120 exact congrArg (n • ·) (x.2 U V hUV)⟩
122instance instSMulIntCompletedGroupAlgebra : SMul ℤ (Carrier R G) where
123 smul n x := ⟨fun U => n • (show CompletedGroupAlgebraStage R G U from x.1 U), by
124 intro U V hUV
125 change completedGroupAlgebraTransition R G hUV
126 (n • (show CompletedGroupAlgebraStage R G V from x.1 V)) =
127 n • (show CompletedGroupAlgebraStage R G U from x.1 U)
128 rw [map_zsmul]
129 exact congrArg (n • ·) (x.2 U V hUV)⟩
132 (U : CompletedGroupAlgebraIndex G) :
133 AddCommGroup ((completedGroupAlgebraSystem R G).X U) := by
135 infer_instance
138 AddCommGroup
139 ((U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) :=
140 inferInstance
142/-- Coordinatewise coercion formula for the inverse-limit completed group algebra. -/
143@[simp]
144theorem coe_zero_completedGroupAlgebra :
145 ((0 : Carrier R G) :
146 (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) = 0 := by
147 funext U
148 rfl
150/-- Coordinatewise coercion formula for the inverse-limit completed group algebra. -/
151@[simp]
152theorem coe_add_completedGroupAlgebra (x y : Carrier R G) :
153 ((x + y : Carrier R G) :
154 (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
155 x + y := by
156 funext U
157 rfl
159/-- Coordinatewise coercion formula for the inverse-limit completed group algebra. -/
160@[simp]
161theorem coe_neg_completedGroupAlgebra (x : Carrier R G) :
162 ((-x : Carrier R G) :
163 (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
164 -x := by
165 funext U
166 rfl
168/-- Coordinatewise coercion formula for the inverse-limit completed group algebra. -/
169@[simp]
170theorem coe_sub_completedGroupAlgebra (x y : Carrier R G) :
171 ((x - y : Carrier R G) :
172 (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
173 x - y := by
174 funext U
175 rfl
177/-- Coordinatewise coercion formula for the inverse-limit completed group algebra. -/
178@[simp]
179theorem coe_nsmul_completedGroupAlgebra (n : ℕ) (x : Carrier R G) :
180 ((n • x : Carrier R G) :
181 (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
182 n • x := by
183 funext U
184 rfl
186/-- Coordinatewise coercion formula for the inverse-limit completed group algebra. -/
187@[simp]
188theorem coe_zsmul_completedGroupAlgebra (n : ℤ) (x : Carrier R G) :
189 ((n • x : Carrier R G) :
190 (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
191 n • x := by
192 funext U
193 rfl
195instance instAddCommGroupCompletedGroupAlgebra : AddCommGroup (Carrier R G) :=
196 Function.Injective.addCommGroup
197 (fun x : Carrier R G =>
198 (x : (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U))
199 Subtype.val_injective
200 (coe_zero_completedGroupAlgebra (R := R) (G := G))
201 (coe_add_completedGroupAlgebra (R := R) (G := G))
202 (coe_neg_completedGroupAlgebra (R := R) (G := G))
203 (coe_sub_completedGroupAlgebra (R := R) (G := G))
204 (fun x n => coe_nsmul_completedGroupAlgebra (R := R) (G := G) n x)
205 (fun x n => coe_zsmul_completedGroupAlgebra (R := R) (G := G) n x)
207omit [TopologicalSpace R] [IsTopologicalRing R] in
208/-- Transition maps commute with coefficient scalar multiplication. -/
210 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
211 (r : R) (x : CompletedGroupAlgebraStage R G V) :
212 completedGroupAlgebraTransition R G hUV (r • x) =
213 r • completedGroupAlgebraTransition R G hUV x := by
215 congr 1
216 simp only [completedGroupAlgebraTransition, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,
217 RingHom.coe_id, Function.comp_apply, id_eq, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single, map_one]
219instance instSMulCoeffCompletedGroupAlgebra : SMul R (Carrier R G) where
220 smul r x := ⟨fun U => r • (show CompletedGroupAlgebraStage R G U from x.1 U), by
221 intro U V hUV
222 change completedGroupAlgebraTransition R G hUV
223 (r • (show CompletedGroupAlgebraStage R G V from x.1 V)) =
224 r • (show CompletedGroupAlgebraStage R G U from x.1 U)
226 exact congrArg (r • ·) (x.2 U V hUV)⟩
228/-- Coordinatewise coercion formula for the inverse-limit completed group algebra. -/
229@[simp]
230theorem coe_smul_completedGroupAlgebra (r : R) (x : Carrier R G) :
231 ((r • x : Carrier R G) :
232 (U : CompletedGroupAlgebraIndex G) → (completedGroupAlgebraSystem R G).X U) =
233 fun U => r • (show CompletedGroupAlgebraStage R G U from x.1 U) := by
234 funext U
235 rfl
237/-- The coordinatewise additive monoid homomorphism from the completed group algebra. -/
239 Carrier R G →+
240 ((U : CompletedGroupAlgebraIndex G) → CompletedGroupAlgebraStage R G U) where
241 toFun x := fun U => (show CompletedGroupAlgebraStage R G U from x.1 U)
242 map_zero' := by
243 funext U
244 rfl
245 map_add' x y := by
246 funext U
247 rfl
249instance instModuleCoeffCompletedGroupAlgebra : Module R (Carrier R G) :=
250 Function.Injective.module R
251 (completedGroupAlgebraValAddMonoidHom (R := R) (G := G))
252 (fun x y h => by
253 apply Subtype.ext
254 funext U
255 exact congrFun h U)
256 (fun r x => by
257 funext U
258 change (show CompletedGroupAlgebraStage R G U from (r • x).1 U) =
259 r • (show CompletedGroupAlgebraStage R G U from x.1 U)
260 rfl)
262end