FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Module.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Projection
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Module.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Completed coefficient algebras
14Coefficient algebras, residue stages, and completed group-algebra maps are kept as the scalar layer for completed Fox calculus.
15-/
16namespace FoxDifferential
18noncomputable section
20open ProCGroups.InverseSystems
21open ProCGroups.ProC
23universe u
25variable (ℓ : ℕ) [Fact (0 < ℓ)]
26variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28omit [Fact (0 < ℓ)] in
29/-- 素冪係数で定めた 遷移写像が関手的写像が有限段階射影と両立することを述べる。 -/
30@[simp]
32 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j)
33 (a : ZMod (ℓ ^ j.1)) :
34 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
35 (algebraMap (ZMod (ℓ ^ j.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G j) a) =
36 algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
38 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
39 (primePow_dvd_primePow (ℓ := ℓ) hij.1) a) := by
40 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
41 classical
44 modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe, map_intCast]
46omit [Fact (0 < ℓ)] in
47/-- 素冪係数で定めた augmentation または augmentation ideal への標準写像が関手的写像が有限段階射影と両立することを述べる。 -/
48@[simp]
50 (i : PrimePowerCompletedGroupAlgebraIndex G) (a : ZMod (ℓ ^ i.1)) :
51 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
52 (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i) a) = a := by
53 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
54 classical
55 simp only [modNCompletedGroupAlgebraStageAugmentation, map_intCast]
57/-- The coefficient inverse limit maps canonically into the completed group algebra by taking
58the stagewise scalar units. -/
60 PrimePowerCompletedCoeff ℓ G →+* PrimePowerCompletedGroupAlgebra ℓ G where
61 toFun a := ⟨fun i =>
62 algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
63 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a), by
64 intro i j hij
65 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
66 (algebraMap (ZMod (ℓ ^ j.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G j)
67 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)) =
68 algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
69 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a)
71 exact congrArg
72 (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
73 (a.2 i j hij)⟩
74 map_one' := by
75 apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
76 intro i
77 change algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
78 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (1 : PrimePowerCompletedCoeff ℓ G))
79 = 1
81 exact map_one (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
82 map_mul' := by
83 intro a b
84 apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
85 intro i
86 change algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
87 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a * b)) =
88 algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
89 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) *
90 algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
91 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b)
93 exact
95 (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
96 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a)
97 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b)
98 map_zero' := by
99 apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
100 intro i
101 change algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
102 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (0 : PrimePowerCompletedCoeff ℓ G))
103 = 0
105 exact map_zero (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
106 map_add' := by
107 intro a b
108 apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
109 intro i
110 change algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
111 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a + b)) =
112 algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
113 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) +
114 algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
115 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b)
117 exact
119 (algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i))
120 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a)
121 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b)
123omit [Fact (0 < ℓ)] in
124/-- 素冪係数で定めた 有限段階射影が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
125@[simp]
127 (i : PrimePowerCompletedGroupAlgebraIndex G) (a : PrimePowerCompletedCoeff ℓ G) :
128 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
129 (primePowerCompletedCoeffToGroupAlgebra (ℓ := ℓ) (G := G) a) =
130 algebraMap (ZMod (ℓ ^ i.1)) (PrimePowerCompletedGroupAlgebraStage ℓ G i)
131 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) := by
132 rfl
134omit [Fact (0 < ℓ)] in
135/-- 素冪係数段階で、有限段階間の遷移写像はスカラー倍と両立する。 -/
136@[simp]
138 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j)
139 (a : ZMod (ℓ ^ j.1))
140 (x : PrimePowerCompletedGroupAlgebraStage ℓ G j) :
141 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij (a • x) =
143 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
144 (primePow_dvd_primePow (ℓ := ℓ) hij.1) a) •
145 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij x := by
146 rw [Algebra.smul_def, map_mul, primePowerCompletedGroupAlgebraTransition_algebraMap]
147 rw [← Algebra.smul_def]
150 CommRing (PrimePowerCompletedCoeff ℓ G) := by
151 infer_instance
154 SMul (PrimePowerCompletedCoeff ℓ G)
155 ((i : PrimePowerCompletedGroupAlgebraIndex G) →
156 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) where
157 smul a x := fun i =>
158 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
159 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i)
162 Module (PrimePowerCompletedCoeff ℓ G)
163 ((i : PrimePowerCompletedGroupAlgebraIndex G) →
164 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) where
165 one_smul x := by
166 funext i
167 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
168 (1 : PrimePowerCompletedCoeff ℓ G)) •
169 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) =
170 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i)
171 rw [primePowerCompletedCoeffProjection_one, one_smul]
172 mul_smul a b x := by
173 funext i
174 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a * b)) •
175 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) =
176 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
177 ((primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b) •
178 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i))
179 rw [primePowerCompletedCoeffProjection_mul, mul_smul]
180 smul_zero a := by
181 funext i
182 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
183 (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) = 0
184 rw [smul_zero]
185 smul_add a x y := by
186 funext i
187 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
188 ((show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) +
189 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y i)) =
190 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
191 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) +
192 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
193 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y i)
194 rw [smul_add]
195 add_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 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) +
201 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b) •
202 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i)
203 rw [primePowerCompletedCoeffProjection_add, add_smul]
204 zero_smul x := by
205 funext i
206 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
207 (0 : PrimePowerCompletedCoeff ℓ G)) •
208 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x i) = 0
209 rw [primePowerCompletedCoeffProjection_zero, zero_smul]
212 SMul (PrimePowerCompletedCoeff ℓ G)
213 (PrimePowerCompletedGroupAlgebra ℓ G) where
214 smul a x := ⟨fun i =>
215 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
216 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i), by
217 intro i j hij
218 calc
219 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
220 ((primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a) •
221 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)) =
223 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
224 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
225 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)) •
226 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
227 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) := by
228 simpa using
230 (ℓ := ℓ) (G := G) hij
231 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)
232 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)
233 _ =
234 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
235 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) := by
236 exact congrArg₂ HSMul.hSMul (a.2 i j hij) (x.2 i j hij)⟩
238omit [Fact (0 < ℓ)] in
239/-- 素冪係数で定めた 部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
240@[simp]
242 (a : PrimePowerCompletedCoeff ℓ G)
243 (x : PrimePowerCompletedGroupAlgebra ℓ G) :
245 (ℓ := ℓ) (G := G)
246 ((a • x : PrimePowerCompletedGroupAlgebra ℓ G) :
247 (i : PrimePowerCompletedGroupAlgebraIndex G) →
248 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =
249 a • (x :
250 (i : PrimePowerCompletedGroupAlgebraIndex G) →
251 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by
252 funext i
253 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
254 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) =
255 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
256 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
257 rfl
259omit [Fact (0 < ℓ)] in
260/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影はスカラー倍と両立する。 -/
261@[simp]
264 (a : PrimePowerCompletedCoeff ℓ G)
265 (x : PrimePowerCompletedGroupAlgebra ℓ G) :
266 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (a • x) =
267 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
268 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x := by
269 rfl
272 Module (PrimePowerCompletedCoeff ℓ G)
273 (PrimePowerCompletedGroupAlgebra ℓ G) :=
274 Function.Injective.module (PrimePowerCompletedCoeff ℓ G)
275 { toFun := Subtype.val
276 map_zero' := rfl
277 map_add' := fun _ _ => rfl }
278 Subtype.val_injective
279 (coe_smul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
281omit [Fact (0 < ℓ)] in
282/-- 素冪係数で定めた augmentation または augmentation ideal への標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
283@[simp]
285 (i : PrimePowerCompletedGroupAlgebraIndex G) (a : PrimePowerCompletedCoeff ℓ G) :
286 modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
287 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
288 (primePowerCompletedCoeffToGroupAlgebra (ℓ := ℓ) (G := G) a)) =
289 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a := by
291 exact primePowerCompletedGroupAlgebraStageAugmentation_algebraMap (ℓ := ℓ) (G := G) i
292 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a)
294end
296end FoxDifferential