Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Ring
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.AddCommGroup
3/-!
4# Fox differential: coefficient rings — prime-power completed group algebra — coeff — ring
6The principal declarations in this module are:
8- `instCommRingPrimePowerCompletedCoeffStage`
9 Each finite prime-power coefficient stage is a commutative ring.
10- `instCommRingPrimePowerCompletedCoeffFamily`
11 The family-level prime-power completed coefficient object is a commutative ring with operations
12 computed coordinatewise.
13- `coe_one_primePowerCompletedCoeff`
14 The multiplicative identity in the prime-power completed coefficient ring is computed
15 coordinatewise.
16- `coe_mul_primePowerCompletedCoeff`
17 Multiplication in the prime-power completed coefficient ring is computed coordinatewise.
18-/
20namespace FoxDifferential
22noncomputable section
24open ProCGroups.InverseSystems
25open ProCGroups.ProC
27universe u
29variable (ℓ : ℕ) [Fact (0 < ℓ)]
30variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
32attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffStage
33attribute [local instance] instAddCommGroupPrimePowerCompletedCoeffFamily
34attribute [local instance] instAddCommGroupPrimePowerCompletedCoeff
36/--
37The unit of the prime-power completed coefficient ring is the compatible family of finite-stage
38units.
39-/
40instance instOnePrimePowerCompletedCoeff : One (PrimePowerCompletedCoeff ℓ G) where
41 one := ⟨fun i => (1 : ZMod (ℓ ^ i.1)), by
42 intro i j hij
43 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
44 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
45 exact map_one
46 (modNCompletedCoeffMap
47 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
48 (primePow_dvd_primePow (ℓ := ℓ) hij.1))⟩
50/--
51Multiplication on the prime-power completed coefficient ring is defined coordinatewise through
52finite-stage coefficient rings.
53-/
54instance instMulPrimePowerCompletedCoeff : Mul (PrimePowerCompletedCoeff ℓ G) where
55 mul x y := ⟨fun i =>
56 (show ZMod (ℓ ^ i.1) from x.1 i) * (show ZMod (ℓ ^ i.1) from y.1 i), by
57 intro i j hij
58 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
59 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
60 change modNCompletedCoeffMap
61 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
62 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
63 ((show ZMod (ℓ ^ j.1) from x.1 j) * (show ZMod (ℓ ^ j.1) from y.1 j)) =
64 (show ZMod (ℓ ^ i.1) from x.1 i) * (show ZMod (ℓ ^ i.1) from y.1 i)
65 rw [map_mul]
66 exact congrArg₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩
68/--
69Natural number casts in the prime-power completed coefficient ring are computed coordinatewise
70from finite-stage natural number casts.
71-/
72instance instNatCastPrimePowerCompletedCoeff : NatCast (PrimePowerCompletedCoeff ℓ G) where
73 natCast n := ⟨fun i => (n : ZMod (ℓ ^ i.1)), by
74 intro i j hij
75 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
76 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
77 exact map_natCast
78 (modNCompletedCoeffMap
79 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
80 (primePow_dvd_primePow (ℓ := ℓ) hij.1)) n⟩
82/--
83Integer casts in the prime-power completed coefficient ring are computed coordinatewise from
84finite-stage integer casts.
85-/
86instance instIntCastPrimePowerCompletedCoeff : IntCast (PrimePowerCompletedCoeff ℓ G) where
87 intCast n := ⟨fun i => (n : ZMod (ℓ ^ i.1)), by
88 intro i j hij
89 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
90 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
91 exact map_intCast
92 (modNCompletedCoeffMap
93 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
94 (primePow_dvd_primePow (ℓ := ℓ) hij.1)) n⟩
96/-- Each finite prime-power coefficient stage is a commutative ring. -/
97@[reducible]
98private def instCommRingPrimePowerCompletedCoeffStage
99 (i : PrimePowerCompletedGroupAlgebraIndex G) :
100 CommRing ((primePowerCompletedCoeffSystem ℓ G).X i) := by
101 dsimp [primePowerCompletedCoeffSystem]
102 infer_instance
103attribute [local instance] instCommRingPrimePowerCompletedCoeffStage
105/--
106The family-level prime-power completed coefficient object is a commutative ring with operations
107computed coordinatewise.
108-/
109@[reducible]
110private def instCommRingPrimePowerCompletedCoeffFamily :
111 CommRing
112 ((i : PrimePowerCompletedGroupAlgebraIndex G) →
113 (primePowerCompletedCoeffSystem ℓ G).X i) :=
114 inferInstance
115attribute [local instance] instCommRingPrimePowerCompletedCoeffFamily
117/--
118Powers in the prime-power completed coefficient ring are computed at every finite coefficient
119stage.
120-/
121instance instPowPrimePowerCompletedCoeff : Pow (PrimePowerCompletedCoeff ℓ G) ℕ where
122 pow x n := ⟨fun i => (show ZMod (ℓ ^ i.1) from x.1 i) ^ n, by
123 intro i j hij
124 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
125 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
126 change modNCompletedCoeffMap
127 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
128 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
129 ((show ZMod (ℓ ^ j.1) from x.1 j) ^ n) =
130 (show ZMod (ℓ ^ i.1) from x.1 i) ^ n
131 rw [map_pow]
132 exact congrArg (fun t => t ^ n) (x.2 i j hij)⟩
134omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
135/--
136The multiplicative identity in the prime-power completed coefficient ring is computed
137coordinatewise.
138-/
139@[simp]
140theorem coe_one_primePowerCompletedCoeff :
141 ((1 : PrimePowerCompletedCoeff ℓ G) :
142 (i : PrimePowerCompletedGroupAlgebraIndex G) →
143 (primePowerCompletedCoeffSystem ℓ G).X i) =
144 (1 :
145 (i : PrimePowerCompletedGroupAlgebraIndex G) →
146 (primePowerCompletedCoeffSystem ℓ G).X i) := by
147 funext i
148 rfl
150omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
151/-- Multiplication in the prime-power completed coefficient ring is computed coordinatewise. -/
152@[simp]
153theorem coe_mul_primePowerCompletedCoeff
154 (x y : PrimePowerCompletedCoeff ℓ G) :
155 ((x * y : PrimePowerCompletedCoeff ℓ G) :
156 (i : PrimePowerCompletedGroupAlgebraIndex G) →
157 (primePowerCompletedCoeffSystem ℓ G).X i) =
158 (x * y :
159 (i : PrimePowerCompletedGroupAlgebraIndex G) →
160 (primePowerCompletedCoeffSystem ℓ G).X i) := by
161 funext i
162 rfl
164omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
165/--
166Natural number casts in the prime-power completed coefficient ring are computed coordinatewise.
167-/
168@[simp]
169theorem coe_natCast_primePowerCompletedCoeff
170 (n : ℕ) :
171 ((n : PrimePowerCompletedCoeff ℓ G) :
172 (i : PrimePowerCompletedGroupAlgebraIndex G) →
173 (primePowerCompletedCoeffSystem ℓ G).X i) =
174 (n :
175 (i : PrimePowerCompletedGroupAlgebraIndex G) →
176 (primePowerCompletedCoeffSystem ℓ G).X i) := by
177 funext i
178 rfl
180omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
181/-- Integer casts in the prime-power completed coefficient ring are computed coordinatewise. -/
182@[simp]
183theorem coe_intCast_primePowerCompletedCoeff
184 (n : ℤ) :
185 ((n : PrimePowerCompletedCoeff ℓ G) :
186 (i : PrimePowerCompletedGroupAlgebraIndex G) →
187 (primePowerCompletedCoeffSystem ℓ G).X i) =
188 (n :
189 (i : PrimePowerCompletedGroupAlgebraIndex G) →
190 (primePowerCompletedCoeffSystem ℓ G).X i) := by
191 funext i
192 rfl
194omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
195/-- Powers in the prime-power completed coefficient ring are computed coordinatewise. -/
196@[simp]
197theorem coe_pow_primePowerCompletedCoeff
198 (x : PrimePowerCompletedCoeff ℓ G) (n : ℕ) :
199 ((x ^ n : PrimePowerCompletedCoeff ℓ G) :
200 (i : PrimePowerCompletedGroupAlgebraIndex G) →
201 (primePowerCompletedCoeffSystem ℓ G).X i) =
202 (x ^ n :
203 (i : PrimePowerCompletedGroupAlgebraIndex G) →
204 (primePowerCompletedCoeffSystem ℓ G).X i) := by
205 funext i
206 rfl
208/--
209The prime-power completed coefficient object is a commutative ring with operations computed
210coordinatewise.
211-/
212instance instCommRingPrimePowerCompletedCoeff :
213 CommRing (PrimePowerCompletedCoeff ℓ G) :=
214 Function.Injective.commRing
215 (fun x : PrimePowerCompletedCoeff ℓ G =>
216 (x :
217 (i : PrimePowerCompletedGroupAlgebraIndex G) →
218 (primePowerCompletedCoeffSystem ℓ G).X i))
219 Subtype.val_injective
220 (coe_zero_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
221 (coe_one_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
222 (coe_add_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
223 (coe_mul_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
224 (coe_neg_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
225 (coe_sub_primePowerCompletedCoeff (ℓ := ℓ) (G := G))
226 (fun n x => coe_nsmul_primePowerCompletedCoeff (ℓ := ℓ) (G := G) n x)
227 (fun n x => coe_zsmul_primePowerCompletedCoeff (ℓ := ℓ) (G := G) n x)
228 (fun x n => coe_pow_primePowerCompletedCoeff (ℓ := ℓ) (G := G) x n)
229 (by
230 intro n
231 exact coe_natCast_primePowerCompletedCoeff (ℓ := ℓ) (G := G) n)
232 (by
233 intro z
234 exact coe_intCast_primePowerCompletedCoeff (ℓ := ℓ) (G := G) z)
236end
238end FoxDifferential