Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.AddCommGroup
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Basic
3/-!
4# Fox differential: coefficient rings — mod-\(n\) completed group algebra — in class — add comm group
6The principal declarations in this module are:
8- `coe_zero_modNCompletedGroupAlgebraInClass`
9 The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed
10 group algebra preserves zero.
11- `coe_add_modNCompletedGroupAlgebraInClass`
12 The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed
13 group algebra preserves addition.
14- `coe_neg_modNCompletedGroupAlgebraInClass`
15 The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed
16 group algebra preserves negation.
17- `coe_sub_modNCompletedGroupAlgebraInClass`
18 The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed
19 group algebra preserves subtraction.
20-/
22namespace FoxDifferential
24noncomputable section
26open ProCGroups.InverseSystems
27open ProCGroups.ProC
29universe 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 instZeroModNCompletedGroupAlgebraInClass
39 (C : ProCGroups.FiniteGroupClass.{u}) :
40 Zero (ModNCompletedGroupAlgebraInClass n G C) where
41 zero := ⟨fun U => (0 : ModNCompletedGroupAlgebraStageInClass n G C U), by
42 intro U V hUV
43 change modNCompletedGroupAlgebraTransitionInClass n G C hUV
44 (0 : ModNCompletedGroupAlgebraStageInClass n G C V) = 0
45 exact map_zero _⟩
47/--
48Addition in the mod-\(n\) completed group algebra is defined coordinatewise through finite-stage
49group-algebra additions.
50-/
51instance instAddModNCompletedGroupAlgebraInClass
52 (C : ProCGroups.FiniteGroupClass.{u}) :
53 Add (ModNCompletedGroupAlgebraInClass n G C) where
54 add x y := ⟨fun U =>
55 (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) +
56 (show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U), by
57 intro U V hUV
58 calc
59 modNCompletedGroupAlgebraTransitionInClass n G C hUV
60 ((show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V) +
61 (show ModNCompletedGroupAlgebraStageInClass n G C V from y.1 V))
62 =
63 modNCompletedGroupAlgebraTransitionInClass n G C hUV
64 (show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V) +
65 modNCompletedGroupAlgebraTransitionInClass n G C hUV
66 (show ModNCompletedGroupAlgebraStageInClass n G C V from y.1 V) := by
67 rw [map_add]
68 _ =
69 (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) +
70 (show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U) := by
71 exact congrArg₂ HAdd.hAdd (x.2 U V hUV) (y.2 U V hUV)⟩
73/--
74Coordinatewise zero and addition on the class-indexed mod-\(n\) completed group algebra satisfy
75the left and right zero laws.
76-/
77instance instAddZeroClassModNCompletedGroupAlgebraInClass
78 (C : ProCGroups.FiniteGroupClass.{u}) :
79 AddZeroClass (ModNCompletedGroupAlgebraInClass n G C) where
80 zero := 0
81 add := (· + ·)
82 zero_add x := by
83 apply Subtype.ext
84 funext U
85 change (0 : ModNCompletedGroupAlgebraStageInClass n G C U) +
86 (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) =
87 (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
88 simp only [zero_add]
89 add_zero x := by
90 apply Subtype.ext
91 funext U
92 change (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) +
93 (0 : ModNCompletedGroupAlgebraStageInClass n G C U) =
94 (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
95 simp only [add_zero]
97/--
98Negation on the \(C\)-indexed mod-\(n\) completed group algebra is defined coordinatewise
99through finite-stage group-algebra negations.
100-/
101instance instNegModNCompletedGroupAlgebraInClass
102 (C : ProCGroups.FiniteGroupClass.{u}) :
103 Neg (ModNCompletedGroupAlgebraInClass n G C) where
104 neg x := ⟨fun U => -(show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U), by
105 intro U V hUV
106 change modNCompletedGroupAlgebraTransitionInClass n G C hUV
107 (-(show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V)) =
108 -(show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
109 rw [map_neg]
110 exact congrArg Neg.neg (x.2 U V hUV)⟩
112/--
113Subtraction on the completed group algebra is defined coordinatewise through the finite-stage
114group-algebra subtractions.
115-/
116instance instSubModNCompletedGroupAlgebraInClass
117 (C : ProCGroups.FiniteGroupClass.{u}) :
118 Sub (ModNCompletedGroupAlgebraInClass n G C) where
119 sub x y := ⟨fun U =>
120 (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) -
121 (show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U), by
122 intro U V hUV
123 change modNCompletedGroupAlgebraTransitionInClass n G C hUV
124 ((show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V) -
125 (show ModNCompletedGroupAlgebraStageInClass n G C V from y.1 V)) =
126 (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U) -
127 (show ModNCompletedGroupAlgebraStageInClass n G C U from y.1 U)
128 rw [map_sub]
129 exact congrArg₂ HSub.hSub (x.2 U V hUV) (y.2 U V hUV)⟩
131/--
132The completed group algebra carries coefficient-ring scalar multiplication by applying the
133scalar action at every finite quotient stage.
134-/
135instance instSMulNatModNCompletedGroupAlgebraInClass
136 (C : ProCGroups.FiniteGroupClass.{u}) :
137 SMul ℕ (ModNCompletedGroupAlgebraInClass n G C) where
138 smul m x := ⟨fun U =>
139 m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U), by
140 intro U V hUV
141 change modNCompletedGroupAlgebraTransitionInClass n G C hUV
142 (m • (show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V)) =
143 m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
144 rw [map_nsmul]
145 exact congrArg (m • ·) (x.2 U V hUV)⟩
147/--
148The completed group algebra carries coefficient-ring scalar multiplication by applying the
149scalar action at every finite quotient stage.
150-/
151instance instSMulIntModNCompletedGroupAlgebraInClass
152 (C : ProCGroups.FiniteGroupClass.{u}) :
153 SMul ℤ (ModNCompletedGroupAlgebraInClass n G C) where
154 smul m x := ⟨fun U =>
155 m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U), by
156 intro U V hUV
157 change modNCompletedGroupAlgebraTransitionInClass n G C hUV
158 (m • (show ModNCompletedGroupAlgebraStageInClass n G C V from x.1 V)) =
159 m • (show ModNCompletedGroupAlgebraStageInClass n G C U from x.1 U)
160 rw [map_zsmul]
161 exact congrArg (m • ·) (x.2 U V hUV)⟩
163omit [Fact (0 < n)] in
164/--
165The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed
166group algebra preserves zero.
167-/
168@[simp]
169theorem coe_zero_modNCompletedGroupAlgebraInClass
170 (C : ProCGroups.FiniteGroupClass.{u}) :
171 ((0 : ModNCompletedGroupAlgebraInClass n G C) :
172 (U : CompletedGroupAlgebraIndexInClass G C) →
173 ModNCompletedGroupAlgebraStageInClass n G C U) = 0 := by
174 funext U
175 rfl
177omit [Fact (0 < n)] in
178/--
179The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed
180group algebra preserves addition.
181-/
182@[simp]
183theorem coe_add_modNCompletedGroupAlgebraInClass
184 (C : ProCGroups.FiniteGroupClass.{u})
185 (x y : ModNCompletedGroupAlgebraInClass n G C) :
186 ((x + y : ModNCompletedGroupAlgebraInClass n G C) :
187 (U : CompletedGroupAlgebraIndexInClass G C) →
188 ModNCompletedGroupAlgebraStageInClass n G C U) = x + y := by
189 funext U
190 rfl
192omit [Fact (0 < n)] in
193/--
194The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed
195group algebra preserves negation.
196-/
197@[simp]
198theorem coe_neg_modNCompletedGroupAlgebraInClass
199 (C : ProCGroups.FiniteGroupClass.{u})
200 (x : ModNCompletedGroupAlgebraInClass n G C) :
201 ((-x : ModNCompletedGroupAlgebraInClass n G C) :
202 (U : CompletedGroupAlgebraIndexInClass G C) →
203 ModNCompletedGroupAlgebraStageInClass n G C U) = -x := by
204 funext U
205 rfl
207omit [Fact (0 < n)] in
208/--
209The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed
210group algebra preserves subtraction.
211-/
212@[simp]
213theorem coe_sub_modNCompletedGroupAlgebraInClass
214 (C : ProCGroups.FiniteGroupClass.{u})
215 (x y : ModNCompletedGroupAlgebraInClass n G C) :
216 ((x - y : ModNCompletedGroupAlgebraInClass n G C) :
217 (U : CompletedGroupAlgebraIndexInClass G C) →
218 ModNCompletedGroupAlgebraStageInClass n G C U) = x - y := by
219 funext U
220 rfl
222omit [Fact (0 < n)] in
223/--
224The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed
225group algebra preserves natural-number scalar multiplication.
226-/
227@[simp]
228theorem coe_nsmul_modNCompletedGroupAlgebraInClass
229 (C : ProCGroups.FiniteGroupClass.{u})
230 (m : ℕ) (x : ModNCompletedGroupAlgebraInClass n G C) :
231 ((m • x : ModNCompletedGroupAlgebraInClass n G C) :
232 (U : CompletedGroupAlgebraIndexInClass G C) →
233 ModNCompletedGroupAlgebraStageInClass n G C U) = m • x := by
234 funext U
235 rfl
237omit [Fact (0 < n)] in
238/--
239The inclusion of the \(C\)-indexed mod-\(n\) completed group algebra into the ambient completed
240group algebra preserves integer scalar multiplication.
241-/
242@[simp]
243theorem coe_zsmul_modNCompletedGroupAlgebraInClass
244 (C : ProCGroups.FiniteGroupClass.{u})
245 (m : ℤ) (x : ModNCompletedGroupAlgebraInClass n G C) :
246 ((m • x : ModNCompletedGroupAlgebraInClass n G C) :
247 (U : CompletedGroupAlgebraIndexInClass G C) →
248 ModNCompletedGroupAlgebraStageInClass n G C U) = m • x := by
249 funext U
250 rfl
252/--
253The class-indexed mod-\(n\) completion inherits an additive commutative group structure from its
254injective inclusion into the family of finite stages.
255-/
256instance instAddCommGroupModNCompletedGroupAlgebraInClass
257 (C : ProCGroups.FiniteGroupClass.{u}) :
258 AddCommGroup (ModNCompletedGroupAlgebraInClass n G C) :=
259 Function.Injective.addCommGroup
260 (fun x : ModNCompletedGroupAlgebraInClass n G C =>
261 (x :
262 (U : CompletedGroupAlgebraIndexInClass G C) →
263 ModNCompletedGroupAlgebraStageInClass n G C U))
264 Subtype.val_injective
265 (coe_zero_modNCompletedGroupAlgebraInClass (n := n) (G := G) C)
266 (coe_add_modNCompletedGroupAlgebraInClass (n := n) (G := G) C)
267 (coe_neg_modNCompletedGroupAlgebraInClass (n := n) (G := G) C)
268 (coe_sub_modNCompletedGroupAlgebraInClass (n := n) (G := G) C)
269 (fun x m => coe_nsmul_modNCompletedGroupAlgebraInClass (n := n) (G := G) C m x)
270 (fun x m => coe_zsmul_modNCompletedGroupAlgebraInClass (n := n) (G := G) C m x)
272omit [Fact (0 < n)] in
273/-- The finite-stage projection sends \(0\) to \(0\). -/
274@[simp]
275theorem modNCompletedGroupAlgebraProjectionInClass_zero
276 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) :
277 modNCompletedGroupAlgebraProjectionInClass n G C U
278 (0 : ModNCompletedGroupAlgebraInClass n G C) = 0 := by
279 rfl
281omit [Fact (0 < n)] in
282/-- The mod-\(n\) finite-stage projection preserves addition. -/
283@[simp]
284theorem modNCompletedGroupAlgebraProjectionInClass_add
285 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
286 (x y : ModNCompletedGroupAlgebraInClass n G C) :
287 modNCompletedGroupAlgebraProjectionInClass n G C U (x + y) =
288 modNCompletedGroupAlgebraProjectionInClass n G C U x +
289 modNCompletedGroupAlgebraProjectionInClass n G C U y := by
290 rfl
292omit [Fact (0 < n)] in
293/-- The mod-\(n\) finite-stage projection preserves negation. -/
294@[simp]
295theorem modNCompletedGroupAlgebraProjectionInClass_neg
296 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
297 (x : ModNCompletedGroupAlgebraInClass n G C) :
298 modNCompletedGroupAlgebraProjectionInClass n G C U (-x) =
299 -modNCompletedGroupAlgebraProjectionInClass n G C U x := by
300 rfl
302omit [Fact (0 < n)] in
303/-- The mod-\(n\) finite-stage projection preserves subtraction. -/
304@[simp]
305theorem modNCompletedGroupAlgebraProjectionInClass_sub
306 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
307 (x y : ModNCompletedGroupAlgebraInClass n G C) :
308 modNCompletedGroupAlgebraProjectionInClass n G C U (x - y) =
309 modNCompletedGroupAlgebraProjectionInClass n G C U x -
310 modNCompletedGroupAlgebraProjectionInClass n G C U y := by
311 rfl
313omit [Fact (0 < n)] in
314/-- The finite-stage projection is compatible with natural-number scalar multiplication. -/
315@[simp]
316theorem modNCompletedGroupAlgebraProjectionInClass_nsmul
317 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
318 (m : ℕ) (x : ModNCompletedGroupAlgebraInClass n G C) :
319 modNCompletedGroupAlgebraProjectionInClass n G C U (m • x) =
320 m • modNCompletedGroupAlgebraProjectionInClass n G C U x := by
321 rfl
323omit [Fact (0 < n)] in
324/-- The finite-stage projection is compatible with integer scalar multiplication. -/
325@[simp]
326theorem modNCompletedGroupAlgebraProjectionInClass_zsmul
327 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C)
328 (m : ℤ) (x : ModNCompletedGroupAlgebraInClass n G C) :
329 modNCompletedGroupAlgebraProjectionInClass n G C U (m • x) =
330 m • modNCompletedGroupAlgebraProjectionInClass n G C U x := by
331 rfl
333end
335end FoxDifferential