Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.AddCommGroup
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Basic
3/-!
4# Fox differential: prime-power completed group algebra — system — ring — add comm group
6The principal declarations in this module are:
8- `instAddCommGroupPrimePowerCompletedGroupAlgebraStage`
9 Each finite prime-power group-algebra stage carries its standard additive group.
10- `instAddCommGroupPrimePowerCompletedGroupAlgebraFamily`
11 The dependent family of finite prime-power group-algebra stages carries the pointwise additive
12 commutative group structure.
13- `coe_zero_primePowerCompletedGroupAlgebra`
14 The inclusion of the prime-power completed group algebra preserves zero.
15- `coe_add_primePowerCompletedGroupAlgebra`
16 The inclusion of the prime-power completed group algebra preserves addition.
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 instZeroPrimePowerCompletedGroupAlgebra : Zero (PrimePowerCompletedGroupAlgebra ℓ G) where
36 zero := ⟨fun i => (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i), by
37 intro i j hij
38 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
39 (0 : PrimePowerCompletedGroupAlgebraStage ℓ G j) = 0
40 exact map_zero _⟩
42/--
43Addition in the prime-power completed group algebra is defined coordinatewise through
44finite-stage group-algebra additions.
45-/
46instance instAddPrimePowerCompletedGroupAlgebra : Add (PrimePowerCompletedGroupAlgebra ℓ G) where
47 add x y := ⟨fun i =>
48 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) +
49 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i), by
50 intro i j hij
51 calc
52 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
53 ((show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) +
54 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j))
55 =
56 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
57 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) +
58 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
59 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j) := by
60 rw [map_add]
61 _ =
62 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) +
63 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i) := by
64 exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩
66/--
67Coordinatewise zero and addition on the prime-power completed group algebra satisfy the left and
68right zero laws.
69-/
70instance instAddZeroClassPrimePowerCompletedGroupAlgebra :
71 AddZeroClass (PrimePowerCompletedGroupAlgebra ℓ G) where
72 zero := 0
73 add := (· + ·)
74 zero_add x := by
75 apply Subtype.ext
76 funext i
77 change (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) +
78 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) =
79 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
80 simp only [zero_add]
81 add_zero x := by
82 apply Subtype.ext
83 funext i
84 change (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) +
85 (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) =
86 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
87 simp only [add_zero]
89/--
90Negation on the prime-power completed group algebra is defined coordinatewise through
91finite-stage group-algebra negations.
92-/
93instance instNegPrimePowerCompletedGroupAlgebra : Neg (PrimePowerCompletedGroupAlgebra ℓ G) where
94 neg x := ⟨fun i => -(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i), by
95 intro i j hij
96 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
97 (-(show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)) =
98 -(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
99 rw [map_neg]
100 exact congrArg Neg.neg (x.2 i j hij)⟩
102/--
103Subtraction on the completed group algebra is defined coordinatewise through the finite-stage
104group-algebra subtractions.
105-/
106instance instSubPrimePowerCompletedGroupAlgebra : Sub (PrimePowerCompletedGroupAlgebra ℓ G) where
107 sub x y := ⟨fun i =>
108 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) -
109 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i), by
110 intro i j hij
111 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
112 ((show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) -
113 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j)) =
114 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) -
115 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i)
116 rw [map_sub]
117 exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩
119/--
120The completed group algebra carries coefficient-ring scalar multiplication by applying the
121scalar action at every finite quotient stage.
122-/
123instance instSMulNatPrimePowerCompletedGroupAlgebra :
124 SMul ℕ (PrimePowerCompletedGroupAlgebra ℓ G) where
125 smul m x := ⟨fun i => m • (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i), by
126 intro i j hij
127 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
128 (m • (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)) =
129 m • (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
130 rw [map_nsmul]
131 exact congrArg (m • ·) (x.2 i j hij)⟩
133/--
134The completed group algebra carries coefficient-ring scalar multiplication by applying the
135scalar action at every finite quotient stage.
136-/
137instance instSMulIntPrimePowerCompletedGroupAlgebra :
138 SMul ℤ (PrimePowerCompletedGroupAlgebra ℓ G) where
139 smul m x := ⟨fun i => m • (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i), by
140 intro i j hij
141 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
142 (m • (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)) =
143 m • (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
144 rw [map_zsmul]
145 exact congrArg (m • ·) (x.2 i j hij)⟩
147/-- Each finite prime-power group-algebra stage carries its standard additive group. -/
148@[reducible] def instAddCommGroupPrimePowerCompletedGroupAlgebraStage
149 (i : PrimePowerCompletedGroupAlgebraIndex G) :
150 AddCommGroup ((primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by
151 dsimp [primePowerCompletedGroupAlgebraSystem, PrimePowerCompletedGroupAlgebraStage]
152 infer_instance
154attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage
156/--
157The dependent family of finite prime-power group-algebra stages carries the pointwise additive
158commutative group structure.
159-/
160@[reducible] def instAddCommGroupPrimePowerCompletedGroupAlgebraFamily :
161 AddCommGroup
162 ((i : PrimePowerCompletedGroupAlgebraIndex G) →
163 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) :=
164 inferInstance
166attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily
168omit [Fact (0 < ℓ)] in
169/-- The inclusion of the prime-power completed group algebra preserves zero. -/
170@[simp]
171theorem coe_zero_primePowerCompletedGroupAlgebra :
172 ((0 : PrimePowerCompletedGroupAlgebra ℓ G) :
173 (i : PrimePowerCompletedGroupAlgebraIndex G) →
174 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = 0 := by
175 funext i
176 rfl
178omit [Fact (0 < ℓ)] in
179/-- The inclusion of the prime-power completed group algebra preserves addition. -/
180@[simp]
181theorem coe_add_primePowerCompletedGroupAlgebra
182 (x y : PrimePowerCompletedGroupAlgebra ℓ G) :
183 ((x + y : PrimePowerCompletedGroupAlgebra ℓ G) :
184 (i : PrimePowerCompletedGroupAlgebraIndex G) →
185 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = x + y := by
186 funext i
187 rfl
189omit [Fact (0 < ℓ)] in
190/-- The inclusion of the prime-power completed group algebra preserves negation. -/
191@[simp]
192theorem coe_neg_primePowerCompletedGroupAlgebra
193 (x : PrimePowerCompletedGroupAlgebra ℓ G) :
194 ((-x : PrimePowerCompletedGroupAlgebra ℓ G) :
195 (i : PrimePowerCompletedGroupAlgebraIndex G) →
196 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = -x := by
197 funext i
198 rfl
200omit [Fact (0 < ℓ)] in
201/-- The inclusion of the prime-power completed group algebra preserves subtraction. -/
202@[simp]
203theorem coe_sub_primePowerCompletedGroupAlgebra
204 (x y : PrimePowerCompletedGroupAlgebra ℓ G) :
205 ((x - y : PrimePowerCompletedGroupAlgebra ℓ G) :
206 (i : PrimePowerCompletedGroupAlgebraIndex G) →
207 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = x - y := by
208 funext i
209 rfl
211omit [Fact (0 < ℓ)] in
212/--
213The inclusion of the prime-power completed group algebra preserves natural-number scalar
214multiplication.
215-/
216@[simp]
217theorem coe_nsmul_primePowerCompletedGroupAlgebra
218 (m : ℕ) (x : PrimePowerCompletedGroupAlgebra ℓ G) :
219 ((m • x : PrimePowerCompletedGroupAlgebra ℓ G) :
220 (i : PrimePowerCompletedGroupAlgebraIndex G) →
221 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = m • x := by
222 funext i
223 rfl
225omit [Fact (0 < ℓ)] in
226/--
227The inclusion of the prime-power completed group algebra preserves integer scalar
228multiplication.
229-/
230@[simp]
231theorem coe_zsmul_primePowerCompletedGroupAlgebra
232 (m : ℤ) (x : PrimePowerCompletedGroupAlgebra ℓ G) :
233 ((m • x : PrimePowerCompletedGroupAlgebra ℓ G) :
234 (i : PrimePowerCompletedGroupAlgebraIndex G) →
235 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = m • x := by
236 funext i
237 rfl
239/--
240The prime-power completion inherits an additive commutative group structure from its injective
241inclusion into the family of finite stages.
242-/
243@[reducible] def instAddCommGroupPrimePowerCompletedGroupAlgebra :
244 AddCommGroup (PrimePowerCompletedGroupAlgebra ℓ G) :=
245 Function.Injective.addCommGroup
246 (fun x : PrimePowerCompletedGroupAlgebra ℓ G =>
247 (x :
248 (i : PrimePowerCompletedGroupAlgebraIndex G) →
249 (primePowerCompletedGroupAlgebraSystem ℓ G).X i))
250 Subtype.val_injective
251 (coe_zero_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
252 (coe_add_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
253 (coe_neg_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
254 (coe_sub_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))
255 (fun x m => coe_nsmul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) m x)
256 (fun x m => coe_zsmul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) m x)
258attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebra
260end
262end FoxDifferential