Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.AddCommGroup
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Basic
3/-!
4# Fox differential: in class — system — ring — add comm group
6The principal declarations in this module are:
8- `instAddCommGroupPrimePowerCompletedGroupAlgebraInClass`
9 The class-indexed prime-power completion inherits an additive commutative group structure from its
10 injective inclusion into the family of finite stages.
11- `coe_zero_primePowerCompletedGroupAlgebraInClass`
12 The inclusion of the class-indexed prime-power completed group algebra preserves zero.
13- `coe_add_primePowerCompletedGroupAlgebraInClass`
14 The inclusion of the class-indexed prime-power completed group algebra preserves addition.
15- `coe_neg_primePowerCompletedGroupAlgebraInClass`
16 The inclusion of the class-indexed prime-power completed group algebra preserves negation.
17-/
19namespace FoxDifferential
21noncomputable section
23open ProCGroups.InverseSystems
24open ProCGroups.ProC
26universe u
28variable (ℓ : ℕ) [Fact (0 < ℓ)]
29variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31/--
32The zero element is defined coordinatewise as the compatible family of zero elements at all
33finite stages.
34-/
35instance instZeroPrimePowerCompletedGroupAlgebraInClass
36 (C : ProCGroups.FiniteGroupClass.{u}) :
37 Zero (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
38 zero := ⟨fun i => (0 : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i), by
39 intro i j hij
40 change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
41 (0 : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j) = 0
42 exact map_zero _⟩
44/--
45Addition in the prime-power completed group algebra is defined coordinatewise through
46finite-stage group-algebra additions.
47-/
48instance instAddPrimePowerCompletedGroupAlgebraInClass
49 (C : ProCGroups.FiniteGroupClass.{u}) :
50 Add (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
51 add x y := ⟨fun i =>
52 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) +
53 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from y.1 i), by
54 intro i j hij
55 calc
56 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
57 ((show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) +
58 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from y.1 j))
59 =
60 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
61 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) +
62 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
63 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from y.1 j) := by
64 rw [map_add]
65 _ =
66 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) +
67 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from y.1 i) := by
68 exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩
70/--
71Coordinatewise zero and addition on the class-indexed prime-power completed group algebra satisfy
72the left and right zero laws.
73-/
74instance instAddZeroClassPrimePowerCompletedGroupAlgebraInClass
75 (C : ProCGroups.FiniteGroupClass.{u}) :
76 AddZeroClass (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
77 zero := 0
78 add := (· + ·)
79 zero_add x := by
80 apply Subtype.ext
81 funext i
82 change (0 : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) +
83 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) =
84 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
85 simp only [zero_add]
86 add_zero x := by
87 apply Subtype.ext
88 funext i
89 change (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) +
90 (0 : PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) =
91 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
92 simp only [add_zero]
94/--
95Negation on the \(C\)-indexed prime-power completed group algebra is defined coordinatewise
96through finite-stage group-algebra negations.
97-/
98instance instNegPrimePowerCompletedGroupAlgebraInClass
99 (C : ProCGroups.FiniteGroupClass.{u}) :
100 Neg (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
101 neg x := ⟨fun i => -(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i), by
102 intro i j hij
103 change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
104 (-(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j)) =
105 -(show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
106 rw [map_neg]
107 exact congrArg Neg.neg (x.2 i j hij)⟩
109/--
110Subtraction on the completed group algebra is defined coordinatewise through the finite-stage
111group-algebra subtractions.
112-/
113instance instSubPrimePowerCompletedGroupAlgebraInClass
114 (C : ProCGroups.FiniteGroupClass.{u}) :
115 Sub (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
116 sub x y := ⟨fun i =>
117 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) -
118 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from y.1 i), by
119 intro i j hij
120 change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
121 ((show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j) -
122 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from y.1 j)) =
123 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i) -
124 (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from y.1 i)
125 rw [map_sub]
126 exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩
128/--
129The completed group algebra carries coefficient-ring scalar multiplication by applying the
130scalar action at every finite quotient stage.
131-/
132instance instSMulNatPrimePowerCompletedGroupAlgebraInClass
133 (C : ProCGroups.FiniteGroupClass.{u}) :
134 SMul ℕ (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
135 smul m x := ⟨fun i =>
136 m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i), by
137 intro i j hij
138 change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
139 (m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j)) =
140 m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
141 rw [map_nsmul]
142 exact congrArg (m • ·) (x.2 i j hij)⟩
144/--
145The completed group algebra carries coefficient-ring scalar multiplication by applying the
146scalar action at every finite quotient stage.
147-/
148instance instSMulIntPrimePowerCompletedGroupAlgebraInClass
149 (C : ProCGroups.FiniteGroupClass.{u}) :
150 SMul ℤ (PrimePowerCompletedGroupAlgebraInClass ℓ G C) where
151 smul m x := ⟨fun i =>
152 m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i), by
153 intro i j hij
154 change primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
155 (m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C j from x.1 j)) =
156 m • (show PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i from x.1 i)
157 rw [map_zsmul]
158 exact congrArg (m • ·) (x.2 i j hij)⟩
160omit [Fact (0 < ℓ)] in
161/-- The inclusion of the class-indexed prime-power completed group algebra preserves zero. -/
162@[simp]
163theorem coe_zero_primePowerCompletedGroupAlgebraInClass
164 (C : ProCGroups.FiniteGroupClass.{u}) :
165 ((0 : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
166 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
167 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = 0 := by
168 funext i
169 rfl
171omit [Fact (0 < ℓ)] in
172/-- The inclusion of the class-indexed prime-power completed group algebra preserves addition. -/
173@[simp]
174theorem coe_add_primePowerCompletedGroupAlgebraInClass
175 (C : ProCGroups.FiniteGroupClass.{u})
176 (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
177 ((x + y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
178 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
179 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = x + y := by
180 funext i
181 rfl
183omit [Fact (0 < ℓ)] in
184/-- The inclusion of the class-indexed prime-power completed group algebra preserves negation. -/
185@[simp]
186theorem coe_neg_primePowerCompletedGroupAlgebraInClass
187 (C : ProCGroups.FiniteGroupClass.{u})
188 (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
189 ((-x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
190 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
191 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = -x := by
192 funext i
193 rfl
195omit [Fact (0 < ℓ)] in
196/--
197Subtraction in the \(C\)-indexed prime-power completed group algebra is computed coordinatewise.
198-/
199@[simp]
200theorem coe_sub_primePowerCompletedGroupAlgebraInClass
201 (C : ProCGroups.FiniteGroupClass.{u})
202 (x y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
203 ((x - y : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
204 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
205 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = x - y := by
206 funext i
207 rfl
209omit [Fact (0 < ℓ)] in
210/--
211The inclusion of the class-indexed prime-power completed group algebra preserves natural-number
212scalar multiplication.
213-/
214@[simp]
215theorem coe_nsmul_primePowerCompletedGroupAlgebraInClass
216 (C : ProCGroups.FiniteGroupClass.{u})
217 (m : ℕ) (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
218 ((m • x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
219 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
220 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = m • x := by
221 funext i
222 rfl
224omit [Fact (0 < ℓ)] in
225/--
226The inclusion of the class-indexed prime-power completed group algebra preserves integer scalar
227multiplication.
228-/
229@[simp]
230theorem coe_zsmul_primePowerCompletedGroupAlgebraInClass
231 (C : ProCGroups.FiniteGroupClass.{u})
232 (m : ℤ) (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
233 ((m • x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
234 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
235 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i) = m • x := by
236 funext i
237 rfl
239/--
240The class-indexed prime-power completion inherits an additive commutative group structure from
241its injective inclusion into the family of finite stages.
242-/
243@[reducible] def instAddCommGroupPrimePowerCompletedGroupAlgebraInClass
244 (C : ProCGroups.FiniteGroupClass.{u}) :
245 AddCommGroup (PrimePowerCompletedGroupAlgebraInClass ℓ G C) :=
246 Function.Injective.addCommGroup
247 (fun x : PrimePowerCompletedGroupAlgebraInClass ℓ G C =>
248 (x :
249 (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) →
250 PrimePowerCompletedGroupAlgebraStageInClass ℓ G C i))
251 Subtype.val_injective
252 (coe_zero_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C)
253 (coe_add_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C)
254 (coe_neg_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C)
255 (coe_sub_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C)
256 (fun x m => coe_nsmul_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C m x)
257 (fun x m => coe_zsmul_primePowerCompletedGroupAlgebraInClass (ℓ := ℓ) (G := G) C m x)
259attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraInClass
261end
263end FoxDifferential