Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.AddCommGroup
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.System
3/-!
4# Fox differential: coefficient rings — prime-power completed group algebra — coeff — add comm group
6The principal declarations in this module are:
8- `instAddCommGroupPrimePowerCompletedCoeffStage`
9 Each coefficient stage \(\mathbb{Z}/\ell^i\mathbb{Z}\) carries its standard additive group.
10- `instAddCommGroupPrimePowerCompletedCoeffFamily`
11 The dependent family of prime-power coefficient stages carries the pointwise additive commutative
12 group structure.
13- `coe_zero_primePowerCompletedCoeff`
14 The inclusion of the prime-power completed coefficient ring preserves zero.
15- `coe_add_primePowerCompletedCoeff`
16 The inclusion of the prime-power completed coefficient ring 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 of the prime-power completed coefficient ring is the compatible family of
33finite-stage zero elements.
34-/
35instance instZeroPrimePowerCompletedCoeff : Zero (PrimePowerCompletedCoeff ℓ G) where
36 zero := ⟨fun i => (0 : ZMod (ℓ ^ i.1)), by
37 intro i j hij
38 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
39 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
40 exact map_zero
41 (modNCompletedCoeffMap
42 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
43 (primePow_dvd_primePow (ℓ := ℓ) hij.1))⟩
45/--
46Addition in the prime-power completed coefficient ring is defined coordinatewise through
47finite-stage coefficient additions.
48-/
49instance instAddPrimePowerCompletedCoeff : Add (PrimePowerCompletedCoeff ℓ G) where
50 add x y := ⟨fun i =>
51 (show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i), by
52 intro i j hij
53 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
54 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
55 change modNCompletedCoeffMap
56 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
57 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
58 ((show ZMod (ℓ ^ j.1) from x.1 j) + (show ZMod (ℓ ^ j.1) from y.1 j)) =
59 (show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i)
60 rw [map_add]
61 exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩
63/--
64Coordinatewise zero and addition on the prime-power completed coefficient ring satisfy the left
65and right zero laws.
66-/
67instance instAddZeroClassPrimePowerCompletedCoeff :
68 AddZeroClass (PrimePowerCompletedCoeff ℓ G) where
69 zero := 0
70 add := (· + ·)
71 zero_add x := by
72 apply Subtype.ext
73 funext i
74 change (0 : ZMod (ℓ ^ i.1)) + (show ZMod (ℓ ^ i.1) from x.1 i) =
75 (show ZMod (ℓ ^ i.1) from x.1 i)
76 simp only [zero_add]
77 add_zero x := by
78 apply Subtype.ext
79 funext i
80 change (show ZMod (ℓ ^ i.1) from x.1 i) + (0 : ZMod (ℓ ^ i.1)) =
81 (show ZMod (ℓ ^ i.1) from x.1 i)
82 simp only [add_zero]
84/--
85Negation on the prime-power completed coefficient ring is defined coordinatewise through
86finite-stage coefficient negations.
87-/
88instance instNegPrimePowerCompletedCoeff : Neg (PrimePowerCompletedCoeff ℓ G) where
89 neg x := ⟨fun i => -(show ZMod (ℓ ^ i.1) from x.1 i), by
90 intro i j hij
91 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
92 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
93 change modNCompletedCoeffMap
94 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
95 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
96 (-(show ZMod (ℓ ^ j.1) from x.1 j)) =
97 -(show ZMod (ℓ ^ i.1) from x.1 i)
98 rw [map_neg]
99 exact congrArg Neg.neg (x.2 i j hij)⟩
101/--
102Subtraction in the prime-power completed coefficient ring is defined coordinatewise through
103finite-stage coefficient-ring subtractions.
104-/
105instance instSubPrimePowerCompletedCoeff : Sub (PrimePowerCompletedCoeff ℓ G) where
106 sub x y := ⟨fun i =>
107 (show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 i), by
108 intro i j hij
109 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
110 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
111 change modNCompletedCoeffMap
112 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
113 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
114 ((show ZMod (ℓ ^ j.1) from x.1 j) - (show ZMod (ℓ ^ j.1) from y.1 j)) =
115 (show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) 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 prime-power completed coefficient ring carries natural-number scalar multiplication
121coordinatewise at every finite coefficient stage.
122-/
123instance instSMulNatPrimePowerCompletedCoeff : SMul ℕ (PrimePowerCompletedCoeff ℓ G) where
124 smul m x := ⟨fun i => m • (show ZMod (ℓ ^ i.1) from x.1 i), by
125 intro i j hij
126 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
127 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
128 change modNCompletedCoeffMap
129 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
130 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
131 (m • (show ZMod (ℓ ^ j.1) from x.1 j)) =
132 m • (show ZMod (ℓ ^ i.1) from x.1 i)
133 rw [map_nsmul]
134 exact congrArg (m • ·) (x.2 i j hij)⟩
136/--
137The prime-power completed coefficient ring carries integer scalar multiplication coordinatewise
138at every finite coefficient stage.
139-/
140instance instSMulIntPrimePowerCompletedCoeff : SMul ℤ (PrimePowerCompletedCoeff ℓ G) where
141 smul m x := ⟨fun i => m • (show ZMod (ℓ ^ i.1) from x.1 i), by
142 intro i j hij
143 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
144 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
145 change modNCompletedCoeffMap
146 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
147 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
148 (m • (show ZMod (ℓ ^ j.1) from x.1 j)) =
149 m • (show ZMod (ℓ ^ i.1) from x.1 i)
150 rw [map_zsmul]
151 exact congrArg (m • ·) (x.2 i j hij)⟩
153/-- Each coefficient stage \(\mathbb{Z}/\ell^i\mathbb{Z}\) carries its standard additive group. -/
154@[reducible] def instAddCommGroupPrimePowerCompletedCoeffStage
155 (i : PrimePowerCompletedGroupAlgebraIndex G) :
156 AddCommGroup ((primePowerCompletedCoeffSystem ℓ G).X i) := by
157 dsimp [primePowerCompletedCoeffSystem]
158 infer_instance
160attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
162/--
163The dependent family of prime-power coefficient stages carries the pointwise additive
164commutative group structure.
165-/
166@[reducible] def instAddCommGroupPrimePowerCompletedCoeffFamily :
167 AddCommGroup
168 ((i : PrimePowerCompletedGroupAlgebraIndex G) →
169 (primePowerCompletedCoeffSystem ℓ G).X i) :=
170 inferInstance
172attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
174omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
175/-- The inclusion of the prime-power completed coefficient ring preserves zero. -/
176@[simp]
177theorem coe_zero_primePowerCompletedCoeff :
178 ((0 : PrimePowerCompletedCoeff ℓ G) :
179 (i : PrimePowerCompletedGroupAlgebraIndex G) →
180 (primePowerCompletedCoeffSystem ℓ G).X i) = 0 := by
181 funext i
182 rfl
184omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
185/-- The inclusion of the prime-power completed coefficient ring preserves addition. -/
186@[simp]
187theorem coe_add_primePowerCompletedCoeff
188 (x y : PrimePowerCompletedCoeff ℓ G) :
189 ((x + y : PrimePowerCompletedCoeff ℓ G) :
190 (i : PrimePowerCompletedGroupAlgebraIndex G) →
191 (primePowerCompletedCoeffSystem ℓ G).X i) = x + y := by
192 funext i
193 rfl
195omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
196/-- The inclusion of the prime-power completed coefficient ring preserves negation. -/
197@[simp]
198theorem coe_neg_primePowerCompletedCoeff
199 (x : PrimePowerCompletedCoeff ℓ G) :
200 ((-x : PrimePowerCompletedCoeff ℓ G) :
201 (i : PrimePowerCompletedGroupAlgebraIndex G) →
202 (primePowerCompletedCoeffSystem ℓ G).X i) = -x := by
203 funext i
204 rfl
206omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
207/-- The inclusion of the prime-power completed coefficient ring preserves subtraction. -/
208@[simp]
209theorem coe_sub_primePowerCompletedCoeff
210 (x y : PrimePowerCompletedCoeff ℓ G) :
211 ((x - y : PrimePowerCompletedCoeff ℓ G) :
212 (i : PrimePowerCompletedGroupAlgebraIndex G) →
213 (primePowerCompletedCoeffSystem ℓ G).X i) = x - y := by
214 funext i
215 rfl
217omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
218/--
219The inclusion of the prime-power completed coefficient ring preserves natural-number scalar
220multiplication.
221-/
222@[simp]
223theorem coe_nsmul_primePowerCompletedCoeff
224 (m : ℕ) (x : PrimePowerCompletedCoeff ℓ G) :
225 ((m • x : PrimePowerCompletedCoeff ℓ G) :
226 (i : PrimePowerCompletedGroupAlgebraIndex G) →
227 (primePowerCompletedCoeffSystem ℓ G).X i) = m • x := by
228 funext i
229 rfl
231omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
232/--
233The inclusion of the prime-power completed coefficient ring preserves integer scalar
234multiplication.
235-/
236@[simp]
237theorem coe_zsmul_primePowerCompletedCoeff
238 (m : ℤ) (x : PrimePowerCompletedCoeff ℓ G) :
239 ((m • x : PrimePowerCompletedCoeff ℓ G) :
240 (i : PrimePowerCompletedGroupAlgebraIndex G) →
241 (primePowerCompletedCoeffSystem ℓ G).X i) = m • x := by
242 funext i
243 rfl
245/--
246The prime-power completed coefficient ring inherits an additive commutative group structure from
247its injective inclusion into the family of coefficient stages.
248-/
249@[reducible] def instAddCommGroupPrimePowerCompletedCoeff :
250 AddCommGroup (PrimePowerCompletedCoeff ℓ G) :=
251 Function.Injective.addCommGroup
252 (fun x : PrimePowerCompletedCoeff ℓ G =>
253 (x :
254 (i : PrimePowerCompletedGroupAlgebraIndex G) →
255 (primePowerCompletedCoeffSystem ℓ G).X i))
256 Subtype.val_injective
257 (coe_zero_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
258 (coe_add_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
259 (coe_neg_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
260 (coe_sub_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
261 (fun x m => coe_nsmul_primePowerCompletedCoeff (ℓ := ℓ) (G := G) m x)
262 (fun x m => coe_zsmul_primePowerCompletedCoeff (ℓ := ℓ) (G := G) m x)
264attribute [local instance] instAddCommGroupPrimePowerCompletedCoeff
266end
268end FoxDifferential