Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Additive
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Stage
3/-!
4# Fox differential: completed — coefficient rings — prime-power augmentation ideal — additive
6The principal declarations in this module are:
8- `instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage`
9 Each finite-stage prime-power augmentation ideal inherits an additive commutative group structure
10 from its ambient finite group algebra.
11- `instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealFamily`
12 The dependent family of finite-stage prime-power augmentation ideals carries the pointwise
13 additive commutative group structure.
14- `coe_zero_primePowerCompletedGroupAlgebraAugmentationIdeal`
15 The inclusion of the completed augmentation ideal preserves zero.
16- `coe_add_primePowerCompletedGroupAlgebraAugmentationIdeal`
17 The inclusion of the completed augmentation ideal preserves addition.
18-/
20namespace FoxDifferential
22noncomputable section
24open ProCGroups.InverseSystems
26universe u
29variable (ℓ : ℕ) [Fact (0 < ℓ)]
30variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
32/--
33The zero element of the prime-power completed augmentation ideal is the compatible family of
34zero elements at all finite stages.
35-/
36instance instZeroPrimePowerCompletedGroupAlgebraAugmentationIdeal :
37 Zero (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
38 zero := ⟨fun i =>
39 (0 : primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i), by
40 intro i j hij
41 apply Subtype.ext
42 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
43 (0 : PrimePowerCompletedGroupAlgebraStage ℓ G j) = 0
44 exact map_zero _⟩
46/--
47Addition in the prime-power completed augmentation ideal is defined coordinatewise through
48finite stages.
49-/
50instance instAddPrimePowerCompletedGroupAlgebraAugmentationIdeal :
51 Add (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
52 add x y := ⟨fun i =>
53 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
54 from x.1 i) +
55 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
56 from y.1 i), by
57 intro i j hij
58 apply Subtype.ext
59 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
60 (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
61 from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j) +
62 ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
63 from y.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j)) =
64 (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
65 from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i) +
66 ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
67 from y.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i))
68 rw [map_add]
69 exact congrArg₂ HAdd.hAdd
70 (congrArg Subtype.val (x.2 i j hij))
71 (congrArg Subtype.val (y.2 i j hij))⟩
73/--
74Coordinatewise zero and addition on the prime-power completed augmentation ideal satisfy the
75left and right zero laws.
76-/
77instance instAddZeroClassPrimePowerCompletedGroupAlgebraAugmentationIdeal :
78 AddZeroClass (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
79 zero := 0
80 add := (· + ·)
81 zero_add x := by
82 apply Subtype.ext
83 funext i
84 apply Subtype.ext
85 change (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) +
86 ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x.1 i) :
87 PrimePowerCompletedGroupAlgebraStage ℓ G i) =
88 ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x.1 i) :
89 PrimePowerCompletedGroupAlgebraStage ℓ G i)
90 simp only [zero_add]
91 add_zero x := by
92 apply Subtype.ext
93 funext i
94 apply Subtype.ext
95 change ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal
96 (ℓ := ℓ) (G := G) i from x.1 i) :
97 PrimePowerCompletedGroupAlgebraStage ℓ G i) +
98 (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) =
99 ((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x.1 i) :
100 PrimePowerCompletedGroupAlgebraStage ℓ G i)
101 simp only [add_zero]
103/--
104Negation on the prime-power completed augmentation ideal is defined coordinatewise through
105finite-stage negations.
106-/
107instance instNegPrimePowerCompletedGroupAlgebraAugmentationIdeal :
108 Neg (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
109 neg x := ⟨fun i =>
110 -(show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
111 from x.1 i), by
112 intro i j hij
113 apply Subtype.ext
114 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
115 (-(((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
116 from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j))) =
117 -(((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
118 from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i))
119 rw [map_neg]
120 exact congrArg Neg.neg (congrArg Subtype.val (x.2 i j hij))⟩
122/--
123Subtraction on the prime-power completed augmentation ideal is defined coordinatewise through
124the finite-stage augmentation ideals.
125-/
126instance instSubPrimePowerCompletedGroupAlgebraAugmentationIdeal :
127 Sub (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
128 sub x y := ⟨fun i =>
129 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
130 from x.1 i) -
131 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
132 from y.1 i), by
133 intro i j hij
134 apply Subtype.ext
135 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
136 ((((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
137 from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j)) -
138 (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
139 from y.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j))) =
140 ((((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
141 from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i)) -
142 (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
143 from y.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i)))
144 rw [map_sub]
145 exact congrArg₂ HSub.hSub
146 (congrArg Subtype.val (x.2 i j hij))
147 (congrArg Subtype.val (y.2 i j hij))⟩
149/--
150The prime-power completed augmentation ideal carries natural-number scalar multiplication
151coordinatewise at every finite quotient stage.
152-/
153instance instSMulNatPrimePowerCompletedGroupAlgebraAugmentationIdeal :
154 SMul ℕ (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
155 smul m x := ⟨fun i =>
156 m • (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
157 from x.1 i), by
158 intro i j hij
159 apply Subtype.ext
160 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
161 (m • (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
162 from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j))) =
163 m • (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
164 from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i))
165 rw [map_nsmul]
166 exact congrArg (m • ·) (congrArg Subtype.val (x.2 i j hij))⟩
168/--
169The prime-power completed augmentation ideal carries integer scalar multiplication
170coordinatewise at every finite quotient stage.
171-/
172instance instSMulIntPrimePowerCompletedGroupAlgebraAugmentationIdeal :
173 SMul ℤ (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
174 smul m x := ⟨fun i =>
175 m • (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
176 from x.1 i), by
177 intro i j hij
178 apply Subtype.ext
179 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
180 (m • (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
181 from x.1 j) : PrimePowerCompletedGroupAlgebraStage ℓ G j))) =
182 m • (((show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
183 from x.1 i) : PrimePowerCompletedGroupAlgebraStage ℓ G i))
184 rw [map_zsmul]
185 exact congrArg (m • ·) (congrArg Subtype.val (x.2 i j hij))⟩
187/--
188Each finite-stage prime-power augmentation ideal inherits an additive commutative group structure
189from its ambient finite group algebra.
190-/
191@[reducible]
192private def instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage
193 (i : PrimePowerCompletedGroupAlgebraIndex G) :
194 AddCommGroup ((primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) := by
195 dsimp [primePowerCompletedGroupAlgebraAugmentationIdealSystem]
196 infer_instance
197attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealStage
199/--
200The dependent family of finite-stage prime-power augmentation ideals carries the pointwise
201additive commutative group structure.
202-/
203@[reducible]
204private def instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealFamily :
205 AddCommGroup
206 ((i : PrimePowerCompletedGroupAlgebraIndex G) →
207 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) :=
208 inferInstance
209attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdealFamily
211omit [Fact (0 < ℓ)] in
212/-- The inclusion of the completed augmentation ideal preserves zero. -/
213@[simp]
214theorem coe_zero_primePowerCompletedGroupAlgebraAugmentationIdeal :
215 ((0 : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
216 (i : PrimePowerCompletedGroupAlgebraIndex G) →
217 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = 0 := by
218 funext i
219 rfl
221omit [Fact (0 < ℓ)] in
222/-- The inclusion of the completed augmentation ideal preserves addition. -/
223@[simp]
224theorem coe_add_primePowerCompletedGroupAlgebraAugmentationIdeal
225 (x y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
226 ((x + y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
227 (i : PrimePowerCompletedGroupAlgebraIndex G) →
228 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = x + y := by
229 funext i
230 rfl
232omit [Fact (0 < ℓ)] in
233/-- The inclusion of the completed augmentation ideal preserves negation. -/
234@[simp]
235theorem coe_neg_primePowerCompletedGroupAlgebraAugmentationIdeal
236 (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
237 ((-x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
238 (i : PrimePowerCompletedGroupAlgebraIndex G) →
239 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = -x := by
240 funext i
241 rfl
243omit [Fact (0 < ℓ)] in
244/-- The inclusion of the completed augmentation ideal preserves subtraction. -/
245@[simp]
246theorem coe_sub_primePowerCompletedGroupAlgebraAugmentationIdeal
247 (x y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
248 ((x - y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
249 (i : PrimePowerCompletedGroupAlgebraIndex G) →
250 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = x - y := by
251 funext i
252 rfl
254omit [Fact (0 < ℓ)] in
255/--
256The inclusion of the completed augmentation ideal preserves natural-number scalar
257multiplication.
258-/
259@[simp]
260theorem coe_nsmul_primePowerCompletedGroupAlgebraAugmentationIdeal
261 (m : ℕ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
262 ((m • x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
263 (i : PrimePowerCompletedGroupAlgebraIndex G) →
264 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = m • x := by
265 funext i
266 rfl
268omit [Fact (0 < ℓ)] in
269/-- The inclusion of the completed augmentation ideal preserves integer scalar multiplication. -/
270@[simp]
271theorem coe_zsmul_primePowerCompletedGroupAlgebraAugmentationIdeal
272 (m : ℤ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
273 ((m • x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
274 (i : PrimePowerCompletedGroupAlgebraIndex G) →
275 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) = m • x := by
276 funext i
277 rfl
279/--
280The prime-power completed augmentation ideal inherits an additive commutative group structure
281from its injective inclusion into the family of finite-stage ideals.
282-/
283instance instAddCommGroupPrimePowerCompletedGroupAlgebraAugmentationIdeal :
284 AddCommGroup (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :=
285 Function.Injective.addCommGroup
286 (fun x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G =>
287 (x :
288 (i : PrimePowerCompletedGroupAlgebraIndex G) →
289 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i))
290 Subtype.val_injective
291 (coe_zero_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G))
292 (coe_add_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G))
293 (coe_neg_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G))
294 (coe_sub_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G))
295 (fun x m => coe_nsmul_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) m x)
296 (fun x m => coe_zsmul_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) m x)
299end
301end FoxDifferential