Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.AddCommGroup
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.Basic
3/-!
4# Fox differential: coefficient rings — mod-\(n\) completed group algebra — system — add comm group
6The principal declarations in this module are:
8- `instAddCommGroupModNCompletedGroupAlgebraStage`
9 Each finite mod-\(n\) group-algebra stage carries its standard additive commutative group.
10- `instAddCommGroupModNCompletedGroupAlgebraFamily`
11 The dependent family of finite mod-\(n\) group-algebra stages carries the pointwise additive
12 commutative group structure.
13- `coe_zero_modNCompletedGroupAlgebra`
14 The inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra
15 preserves zero.
16- `coe_add_modNCompletedGroupAlgebra`
17 The inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra
18 preserves addition.
19-/
21namespace FoxDifferential
23noncomputable section
25open ProCGroups.InverseSystems
26open ProCGroups.ProC
28universe u
31variable (n : ℕ) [Fact (0 < n)]
32variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
34/--
35The zero element is defined coordinatewise as the compatible family of zero elements at all
36finite stages.
37-/
38instance instZeroModNCompletedGroupAlgebra : Zero (ModNCompletedGroupAlgebra n G) where
39 zero := ⟨fun U => (0 : ModNCompletedGroupAlgebraStage n G U), by
40 intro U V hUV
41 change modNCompletedGroupAlgebraTransition n G hUV
42 (0 : ModNCompletedGroupAlgebraStage n G V) = 0
43 exact map_zero (modNCompletedGroupAlgebraTransition n G hUV)⟩
45/--
46Addition in the mod-\(n\) completed group algebra is defined coordinatewise through finite-stage
47group-algebra additions.
48-/
49instance instAddModNCompletedGroupAlgebra : Add (ModNCompletedGroupAlgebra n G) where
50 add x y := ⟨fun U =>
51 (show ModNCompletedGroupAlgebraStage n G U from x.1 U) +
52 (show ModNCompletedGroupAlgebraStage n G U from y.1 U), by
53 intro U V hUV
54 calc
55 modNCompletedGroupAlgebraTransition n G hUV
56 ((show ModNCompletedGroupAlgebraStage n G V from x.1 V) +
57 (show ModNCompletedGroupAlgebraStage n G V from y.1 V))
58 =
59 modNCompletedGroupAlgebraTransition n G hUV
60 (show ModNCompletedGroupAlgebraStage n G V from x.1 V) +
61 modNCompletedGroupAlgebraTransition n G hUV
62 (show ModNCompletedGroupAlgebraStage n G V from y.1 V) := by
63 rw [map_add]
64 _ =
65 (show ModNCompletedGroupAlgebraStage n G U from x.1 U) +
66 (show ModNCompletedGroupAlgebraStage n G U from y.1 U) := by
67 exact congrArg₂ HAdd.hAdd (x.2 U V hUV) (y.2 U V hUV)⟩
69/--
70Coordinatewise zero and addition on the mod-\(n\) completed group algebra satisfy the left and
71right zero laws.
72-/
73instance instAddZeroClassModNCompletedGroupAlgebra :
74 AddZeroClass (ModNCompletedGroupAlgebra n G) where
75 zero := 0
76 add := (· + ·)
77 zero_add x := by
78 apply Subtype.ext
79 funext U
80 change (0 : ModNCompletedGroupAlgebraStage n G U) +
81 (show ModNCompletedGroupAlgebraStage n G U from x.1 U) =
82 (show ModNCompletedGroupAlgebraStage n G U from x.1 U)
83 simp only [zero_add]
84 add_zero x := by
85 apply Subtype.ext
86 funext U
87 change (show ModNCompletedGroupAlgebraStage n G U from x.1 U) +
88 (0 : ModNCompletedGroupAlgebraStage n G U) =
89 (show ModNCompletedGroupAlgebraStage n G U from x.1 U)
90 simp only [add_zero]
92/--
93Negation on the mod-\(n\) completed group algebra is defined coordinatewise through finite-stage
94group-algebra negations.
95-/
96instance instNegModNCompletedGroupAlgebra : Neg (ModNCompletedGroupAlgebra n G) where
97 neg x := ⟨fun U => -(show ModNCompletedGroupAlgebraStage n G U from x.1 U), by
98 intro U V hUV
99 change modNCompletedGroupAlgebraTransition n G hUV
100 (-(show ModNCompletedGroupAlgebraStage n G V from x.1 V)) =
101 -(show ModNCompletedGroupAlgebraStage n G U from x.1 U)
102 rw [map_neg]
103 exact congrArg Neg.neg (x.2 U V hUV)⟩
105/--
106Subtraction on the completed group algebra is defined coordinatewise through the finite-stage
107group-algebra subtractions.
108-/
109instance instSubModNCompletedGroupAlgebra : Sub (ModNCompletedGroupAlgebra n G) where
110 sub x y := ⟨fun U =>
111 (show ModNCompletedGroupAlgebraStage n G U from x.1 U) -
112 (show ModNCompletedGroupAlgebraStage n G U from y.1 U), by
113 intro U V hUV
114 change modNCompletedGroupAlgebraTransition n G hUV
115 ((show ModNCompletedGroupAlgebraStage n G V from x.1 V) -
116 (show ModNCompletedGroupAlgebraStage n G V from y.1 V)) =
117 (show ModNCompletedGroupAlgebraStage n G U from x.1 U) -
118 (show ModNCompletedGroupAlgebraStage n G U from y.1 U)
119 rw [map_sub]
120 exact congrArg₂ HSub.hSub (x.2 U V hUV) (y.2 U V hUV)⟩
122/--
123The completed group algebra carries coefficient-ring scalar multiplication by applying the
124scalar action at every finite quotient stage.
125-/
126instance instSMulNatModNCompletedGroupAlgebra : SMul ℕ (ModNCompletedGroupAlgebra n G) where
127 smul m x := ⟨fun U => m • (show ModNCompletedGroupAlgebraStage n G U from x.1 U), by
128 intro U V hUV
129 change modNCompletedGroupAlgebraTransition n G hUV
130 (m • (show ModNCompletedGroupAlgebraStage n G V from x.1 V)) =
131 m • (show ModNCompletedGroupAlgebraStage n G U from x.1 U)
132 rw [map_nsmul]
133 exact congrArg (m • ·) (x.2 U V hUV)⟩
135/--
136The completed group algebra carries coefficient-ring scalar multiplication by applying the
137scalar action at every finite quotient stage.
138-/
139instance instSMulIntModNCompletedGroupAlgebra : SMul ℤ (ModNCompletedGroupAlgebra n G) where
140 smul m x := ⟨fun U => m • (show ModNCompletedGroupAlgebraStage n G U from x.1 U), by
141 intro U V hUV
142 change modNCompletedGroupAlgebraTransition n G hUV
143 (m • (show ModNCompletedGroupAlgebraStage n G V from x.1 V)) =
144 m • (show ModNCompletedGroupAlgebraStage n G U from x.1 U)
145 rw [map_zsmul]
146 exact congrArg (m • ·) (x.2 U V hUV)⟩
148/-- Each finite mod-\(n\) group-algebra stage carries its standard additive commutative group. -/
149@[reducible]
150private def instAddCommGroupModNCompletedGroupAlgebraStage (U :
151 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
152 AddCommGroup ((modNCompletedGroupAlgebraSystem n G).X U) := by
153 dsimp [modNCompletedGroupAlgebraSystem, ModNCompletedGroupAlgebraStage]
154 infer_instance
155attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraStage
157/--
158The dependent family of finite mod-\(n\) group-algebra stages carries the pointwise additive
159commutative group structure.
160-/
161@[reducible]
162private def instAddCommGroupModNCompletedGroupAlgebraFamily :
163 AddCommGroup ((i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) →
164 (modNCompletedGroupAlgebraSystem n G).X i) :=
165 inferInstance
166attribute [local instance] instAddCommGroupModNCompletedGroupAlgebraFamily
168omit [Fact (0 < n)] in
169/--
170The inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra
171preserves zero.
172-/
173@[simp]
174theorem coe_zero_modNCompletedGroupAlgebra :
175 ((0 : ModNCompletedGroupAlgebra n G) :
176 (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) →
177 (modNCompletedGroupAlgebraSystem n G).X i) = 0 := by
178 funext U
179 rfl
181omit [Fact (0 < n)] in
182/--
183The inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra
184preserves addition.
185-/
186@[simp]
187theorem coe_add_modNCompletedGroupAlgebra
188 (x y : ModNCompletedGroupAlgebra n G) :
189 ((x + y : ModNCompletedGroupAlgebra n G) :
190 (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) →
191 (modNCompletedGroupAlgebraSystem n G).X i) =
192 x + y := by
193 funext U
194 rfl
196omit [Fact (0 < n)] in
197/--
198The inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra
199preserves negation.
200-/
201@[simp]
202theorem coe_neg_modNCompletedGroupAlgebra
203 (x : ModNCompletedGroupAlgebra n G) :
204 ((-x : ModNCompletedGroupAlgebra n G) :
205 (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) →
206 (modNCompletedGroupAlgebraSystem n G).X i) =
207 -x := by
208 funext U
209 rfl
211omit [Fact (0 < n)] in
212/--
213The inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra
214preserves subtraction.
215-/
216@[simp]
217theorem coe_sub_modNCompletedGroupAlgebra
218 (x y : ModNCompletedGroupAlgebra n G) :
219 ((x - y : ModNCompletedGroupAlgebra n G) :
220 (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) →
221 (modNCompletedGroupAlgebraSystem n G).X i) =
222 x - y := by
223 funext U
224 rfl
226omit [Fact (0 < n)] in
227/--
228The inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra
229preserves natural-number scalar multiplication.
230-/
231@[simp]
232theorem coe_nsmul_modNCompletedGroupAlgebra
233 (m : ℕ) (x : ModNCompletedGroupAlgebra n G) :
234 ((m • x : ModNCompletedGroupAlgebra n G) :
235 (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) →
236 (modNCompletedGroupAlgebraSystem n G).X i) =
237 m • x := by
238 funext U
239 rfl
241omit [Fact (0 < n)] in
242/--
243The inclusion of the mod-\(n\) completed group algebra into the ambient completed group algebra
244preserves integer scalar multiplication.
245-/
246@[simp]
247theorem coe_zsmul_modNCompletedGroupAlgebra
248 (m : ℤ) (x : ModNCompletedGroupAlgebra n G) :
249 ((m • x : ModNCompletedGroupAlgebra n G) :
250 (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) →
251 (modNCompletedGroupAlgebraSystem n G).X i) =
252 m • x := by
253 funext U
254 rfl
256/--
257The mod-\(n\) completion inherits an additive commutative group structure from its injective
258inclusion into the family of finite stages.
259-/
260instance instAddCommGroupModNCompletedGroupAlgebra :
261 AddCommGroup (ModNCompletedGroupAlgebra n G) :=
262 Function.Injective.addCommGroup
263 (fun x : ModNCompletedGroupAlgebra n G =>
264 (x : (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) →
265 (modNCompletedGroupAlgebraSystem n G).X i))
266 Subtype.val_injective
267 (coe_zero_modNCompletedGroupAlgebra (n := n) (G := G))
268 (coe_add_modNCompletedGroupAlgebra (n := n) (G := G))
269 (coe_neg_modNCompletedGroupAlgebra (n := n) (G := G))
270 (coe_sub_modNCompletedGroupAlgebra (n := n) (G := G))
271 (fun x m => coe_nsmul_modNCompletedGroupAlgebra (n := n) (G := G) m x)
272 (fun x m => coe_zsmul_modNCompletedGroupAlgebra (n := n) (G := G) m x)
274omit [Fact (0 < n)] in
275/-- The finite-stage projection sends \(0\) to \(0\). -/
276@[simp]
277theorem modNCompletedGroupAlgebraProjection_zero (U :
278 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :
279 modNCompletedGroupAlgebraProjection n G U (0 : ModNCompletedGroupAlgebra n G) = 0 := by
280 change (0 : ModNCompletedGroupAlgebraStage n G U) = 0
281 rfl
283omit [Fact (0 < n)] in
284/-- The mod-\(n\) finite-stage projection preserves addition. -/
285@[simp]
286theorem modNCompletedGroupAlgebraProjection_add (U :
287 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
288 (x y : ModNCompletedGroupAlgebra n G) :
289 modNCompletedGroupAlgebraProjection n G U (x + y) =
290 modNCompletedGroupAlgebraProjection n G U x +
291 modNCompletedGroupAlgebraProjection n G U y := by
292 change (show ModNCompletedGroupAlgebraStage n G U from (x + y).1 U) =
293 (show ModNCompletedGroupAlgebraStage n G U from x.1 U) +
294 (show ModNCompletedGroupAlgebraStage n G U from y.1 U)
295 rfl
297omit [Fact (0 < n)] in
298/-- The mod-\(n\) finite-stage projection preserves negation. -/
299@[simp]
300theorem modNCompletedGroupAlgebraProjection_neg (U :
301 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
302 (x : ModNCompletedGroupAlgebra n G) :
303 modNCompletedGroupAlgebraProjection n G U (-x) =
304 -modNCompletedGroupAlgebraProjection n G U x := by
305 change (show ModNCompletedGroupAlgebraStage n G U from (-x).1 U) =
306 -(show ModNCompletedGroupAlgebraStage n G U from x.1 U)
307 rfl
309omit [Fact (0 < n)] in
310/-- The mod-\(n\) finite-stage projection preserves subtraction. -/
311@[simp]
312theorem modNCompletedGroupAlgebraProjection_sub (U :
313 _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
314 (x y : ModNCompletedGroupAlgebra n G) :
315 modNCompletedGroupAlgebraProjection n G U (x - y) =
316 modNCompletedGroupAlgebraProjection n G U x -
317 modNCompletedGroupAlgebraProjection n G U y := by
318 change (show ModNCompletedGroupAlgebraStage n G U from (x - y).1 U) =
319 (show ModNCompletedGroupAlgebraStage n G U from x.1 U) -
320 (show ModNCompletedGroupAlgebraStage n G U from y.1 U)
321 rfl
323omit [Fact (0 < n)] in
324end
326end FoxDifferential