Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Module
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Projection
3/-!
4# Fox differential: completed — coefficient rings — prime-power completed group algebra — module
6The principal declarations in this module are:
8- `primePowerCompletedCoeffToGroupAlgebra`
9 The coefficient inverse limit maps canonically into the completed group algebra by taking the
10 stagewise scalar units.
11- `primePowerCompletedGroupAlgebraTransition_algebraMap`
12 Finite-stage transitions send scalar coefficients through the reduced coefficient algebra map.
13- `primePowerCompletedGroupAlgebraStageAugmentation_algebraMap`
14 The finite-stage prime-power augmentation agrees with the scalar algebra map on coefficients.
15- `primePowerCompletedGroupAlgebraProjection_coeffToGroupAlgebra`
16 The prime-power completed group-algebra projection on coefficients is computed by the
17 corresponding group-algebra coordinate map.
18-/
20namespace FoxDifferential
22noncomputable section
24open ProCGroups.InverseSystems
25open ProCGroups.ProC
27universe u
29variable (ℓ : ℕ) [Fact (0 < ℓ)]
30variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
32attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
33attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
34attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
35attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
37omit [Fact (0 < ℓ)] in
38/--
39Finite-stage transitions send scalar coefficients through the reduced coefficient algebra map.
40-/
41@[simp]
42theorem primePowerCompletedGroupAlgebraTransition_algebraMap
43 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j)
44 (a : ZMod (ℓ ^ j.1)) :
45 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
46 (algebraMap (ZMod (ℓ ^ j.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G j) a) =
47 algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
48 (modNCompletedCoeffMap
49 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
50 (primePow_dvd_primePow (ℓ := ℓ) hij.1) a) := by
51 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
52 classical
53 rw [primePowerCompletedGroupAlgebraTransition_eq']
54 simp only [modNCompletedGroupAlgebraTransition, modNCompletedGroupAlgebraStageCoeffMap,
55 modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe, map_intCast]
57omit [Fact (0 < ℓ)] in
58/-- The finite-stage prime-power augmentation agrees with the scalar algebra map on coefficients. -/
59@[simp]
60theorem primePowerCompletedGroupAlgebraStageAugmentation_algebraMap
61 (i : PrimePowerCompletedGroupAlgebraIndex G) (a : ZMod (ℓ ^ i.1)) :
62 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
63 (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i) a) = a := by
64 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
65 classical
66 simp only [modNCompletedGroupAlgebraStageAugmentation, map_intCast]
68/--
69The coefficient inverse limit maps canonically into the completed group algebra by taking the
70stagewise scalar units.
71-/
72def primePowerCompletedCoeffToGroupAlgebra :
73 PrimePowerCompletedCoeff ℓ G →+* PrimePowerCompletedGroupAlgebra ℓ G where
74 toFun a := ⟨fun i =>
75 algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
76 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a), by
77 intro i j hij
78 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
79 (algebraMap (ZMod (ℓ ^ j.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G j)
80 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)) =
81 algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
82 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a)
83 rw [primePowerCompletedGroupAlgebraTransition_algebraMap]
84 exact congrArg
85 (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
86 (a.2 i j hij)⟩
87 map_one' := by
88 apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
89 intro i
90 change algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
91 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (1 : PrimePowerCompletedCoeff ℓ G))
92 = 1
93 rw [primePowerCompletedCoeffProjection_one]
94 exact map_one (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
95 map_mul' := by
96 intro a b
97 apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
98 intro i
99 change algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
100 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a * b)) =
101 algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
102 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) *
103 algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
104 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b)
105 rw [primePowerCompletedCoeffProjection_mul]
106 exact
107 map_mul
108 (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
109 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a)
110 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b)
111 map_zero' := by
112 apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
113 intro i
114 change algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
115 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (0 : PrimePowerCompletedCoeff ℓ G))
116 = 0
117 rw [primePowerCompletedCoeffProjection_zero]
118 exact map_zero (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
119 map_add' := by
120 intro a b
121 apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
122 intro i
123 change algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
124 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a + b)) =
125 algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
126 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) +
127 algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
128 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b)
129 rw [primePowerCompletedCoeffProjection_add]
130 exact
131 map_add
132 (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
133 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a)
134 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b)
136omit [Fact (0 < ℓ)] in
137/--
138The prime-power completed group-algebra projection on coefficients is computed by the
139corresponding group-algebra coordinate map.
140-/
141@[simp]
142theorem primePowerCompletedGroupAlgebraProjection_coeffToGroupAlgebra
143 (i : PrimePowerCompletedGroupAlgebraIndex G) (a : PrimePowerCompletedCoeff ℓ G) :
144 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
145 (primePowerCompletedCoeffToGroupAlgebra (ℓ := ℓ) (G := G) a) =
146 algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
147 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) := by
148 rfl
150omit [Fact (0 < ℓ)] in
151/--
152Finite-stage transitions commute with scalar multiplication after reducing the scalar
153coefficient.
154-/
155@[simp]
156theorem primePowerCompletedGroupAlgebraTransition_smul
157 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j)
158 (a : ZMod (ℓ ^ j.1))
159 (x : PrimePowerCompletedGroupAlgebraStage ℓ G j) :
160 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij (a • x) =
161 (modNCompletedCoeffMap
162 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
163 (primePow_dvd_primePow (ℓ := ℓ) hij.1) a) •
164 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij x := by
165 rw [Algebra.smul_def, map_mul, primePowerCompletedGroupAlgebraTransition_algebraMap]
166 rw [← Algebra.smul_def]
168/--
169The ambient family of prime-power group-algebra stages carries pointwise scalar multiplication,
170using the projection of a completed coefficient at each index.
171-/
172instance instSMulPrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebraFamily :
173 SMul (PrimePowerCompletedCoeff ℓ G)
174 ((i : PrimePowerCompletedGroupAlgebraIndex G) →
175 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) where
176 smul a x := fun i =>
177 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
178 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i)
180/--
181The prime-power completed group-algebra family is a module over the prime-power completed
182coefficient ring.
183-/
184instance instModulePrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebraFamily :
185 Module (PrimePowerCompletedCoeff ℓ G)
186 ((i : PrimePowerCompletedGroupAlgebraIndex G) →
187 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) where
188 one_smul x := by
189 funext i
190 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
191 (1 : PrimePowerCompletedCoeff ℓ G)) •
192 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) =
193 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i)
194 rw [primePowerCompletedCoeffProjection_one, one_smul]
195 mul_smul a b x := by
196 funext i
197 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a * b)) •
198 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) =
199 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
200 ((primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b) •
201 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i))
202 rw [primePowerCompletedCoeffProjection_mul, mul_smul]
203 smul_zero a := by
204 funext i
205 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
206 (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) = 0
207 rw [smul_zero]
208 smul_add a x y := by
209 funext i
210 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
211 ((show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) +
212 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y i)) =
213 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
214 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) +
215 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
216 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y i)
217 rw [smul_add]
218 add_smul a b x := by
219 funext i
220 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a + b)) •
221 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) =
222 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
223 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) +
224 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b) •
225 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i)
226 rw [primePowerCompletedCoeffProjection_add, add_smul]
227 zero_smul x := by
228 funext i
229 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
230 (0 : PrimePowerCompletedCoeff ℓ G)) •
231 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) = 0
232 rw [primePowerCompletedCoeffProjection_zero, zero_smul]
234/--
235The completed group algebra carries coefficient-ring scalar multiplication by applying the
236scalar action at every finite quotient stage.
237-/
238instance instSMulPrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebra :
239 SMul (PrimePowerCompletedCoeff ℓ G)
240 (PrimePowerCompletedGroupAlgebra ℓ G) where
241 smul a x := ⟨fun i =>
242 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
243 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i), by
244 intro i j hij
245 calc
246 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
247 ((primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a) •
248 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)) =
249 (modNCompletedCoeffMap
250 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
251 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
252 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)) •
253 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
254 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) := by
255 simpa using
256 primePowerCompletedGroupAlgebraTransition_smul
257 (ℓ := ℓ) (G := G) hij
258 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)
259 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)
260 _ =
261 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
262 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) := by
263 exact congrArg₂ HSMul.hSMul (a.2 i j hij) (x.2 i j hij)⟩
265omit [Fact (0 < ℓ)] in
266/-- The inclusion of the prime-power completed group algebra preserves scalar multiplication. -/
267@[simp]
268theorem coe_smul_primePowerCompletedGroupAlgebra
269 (a : PrimePowerCompletedCoeff ℓ G)
270 (x : PrimePowerCompletedGroupAlgebra ℓ G) :
271 letI := instSMulPrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebra
272 (ℓ := ℓ) (G := G)
273 ((a • x : PrimePowerCompletedGroupAlgebra ℓ G) :
274 (i : PrimePowerCompletedGroupAlgebraIndex G) →
275 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
276 a • (x :
277 (i : PrimePowerCompletedGroupAlgebraIndex G) →
278 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by
279 funext i
280 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
281 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) =
282 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
283 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
284 rfl
286omit [Fact (0 < ℓ)] in
287/-- The finite-stage projection is compatible with scalar multiplication. -/
288@[simp]
289theorem primePowerCompletedGroupAlgebraProjection_smul
290 (i : PrimePowerCompletedGroupAlgebraIndex G)
291 (a : PrimePowerCompletedCoeff ℓ G)
292 (x : PrimePowerCompletedGroupAlgebra ℓ G) :
293 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (a • x) =
294 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
295 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x := by
296 rfl
298/--
299The prime-power completed group algebra is a module over the prime-power completed coefficient
300ring.
301-/
302instance instModulePrimePowerCompletedCoeffPrimePowerCompletedGroupAlgebra :
303 Module (PrimePowerCompletedCoeff ℓ G)
304 (PrimePowerCompletedGroupAlgebra ℓ G) :=
305 Function.Injective.module (PrimePowerCompletedCoeff ℓ G)
306 { toFun := Subtype.val
307 map_zero' := rfl
308 map_add' := fun _ _ => rfl }
309 Subtype.val_injective
310 (coe_smul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
312omit [Fact (0 < ℓ)] in
313/--
314The prime-power completed augmentation is left inverse to the coefficient-to-group-algebra map.
315-/
316@[simp]
317theorem primePowerCompletedGroupAlgebraAugmentation_coeffToGroupAlgebra
318 (i : PrimePowerCompletedGroupAlgebraIndex G) (a : PrimePowerCompletedCoeff ℓ G) :
319 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
320 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
321 (primePowerCompletedCoeffToGroupAlgebra (ℓ := ℓ) (G := G) a)) =
322 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a := by
323 rw [primePowerCompletedGroupAlgebraProjection_coeffToGroupAlgebra]
324 exact primePowerCompletedGroupAlgebraStageAugmentation_algebraMap (ℓ := ℓ) (G := G) i
325 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a)
327end
329end FoxDifferential