Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Augmentation
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Projection
3/-!
4# Fox differential: coefficient rings — prime-power completed group algebra — in class — augmentation
6The principal declarations in this module are:
8- `primePowerCompletedCoeffSystemInClass`
9 The class-restricted coefficient inverse system indexed by \(i = (a,U)\), whose coefficient stage
10 is \(\mathrm{ZMod}\,(\ell^a)\).
11- `PrimePowerCompletedCoeffCompatibleInClass`
12 Compatibility for the class-indexed coefficient tower; the finite quotient component is retained
13 only to match the surrounding pro-\(C\) index shape.
14- `primePowerCompletedCoeffProjectionInClass_zero`
15 The finite-stage projection sends \(0\) to \(0\).
16- `primePowerCompletedCoeffProjectionInClass_add`
17 The class-indexed prime-power coefficient projection preserves addition.
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]
32/--
33The class-restricted coefficient inverse system indexed by \(i = (a,U)\), whose coefficient
34stage is \(\mathrm{ZMod}\,(\ell^a)\).
35-/
36def primePowerCompletedCoeffSystemInClass
37 (C : ProCGroups.FiniteGroupClass.{u}) :
38 InverseSystem (I := PrimePowerCompletedGroupAlgebraIndexInClass G C) where
39 X := fun i => ModNCompletedCoeff (ℓ ^ i.1)
40 topologicalSpace := fun _ => ⊥
41 map := fun {i j} hij =>
42 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
43 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
44 modNCompletedCoeffMap
45 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
46 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
47 continuous_map := by
48 intro i j hij
49 letI : TopologicalSpace (ModNCompletedCoeff (ℓ ^ i.1)) := ⊥
50 letI : TopologicalSpace (ModNCompletedCoeff (ℓ ^ j.1)) := ⊥
51 letI : DiscreteTopology (ModNCompletedCoeff (ℓ ^ j.1)) := ⟨rfl⟩
52 exact continuous_of_discreteTopology
53 map_id := by
54 intro i
55 funext x
56 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
57 exact congrFun
58 (congrArg DFunLike.coe
59 (modNCompletedCoeffMap_rfl (n := ℓ ^ i.1))) x
60 map_comp := by
61 intro i j k hij hjk
62 funext x
63 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
64 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
65 letI : Fact (0 < ℓ ^ k.1) := ⟨primePower_pos ℓ k.1⟩
66 exact congrFun
67 (congrArg DFunLike.coe
68 (modNCompletedCoeffMap_comp
69 (n := ℓ ^ i.1) (m := ℓ ^ j.1) (k := ℓ ^ k.1)
70 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
71 (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) x
73/--
74Compatibility for the class-indexed coefficient tower; the finite quotient component is retained
75only to match the surrounding pro-\(C\) index shape.
76-/
77def PrimePowerCompletedCoeffCompatibleInClass
78 (C : ProCGroups.FiniteGroupClass.{u})
79 (x : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C,
80 ModNCompletedCoeff (ℓ ^ i.1)) : Prop :=
81 (primePowerCompletedCoeffSystemInClass ℓ G C).Compatible x
83/-- The pro-\(C\)-indexed prime-power completed coefficient inverse limit. -/
84abbrev PrimePowerCompletedCoeffInClass (C : ProCGroups.FiniteGroupClass.{u}) : Type _ :=
85 {x : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C,
86 ModNCompletedCoeff (ℓ ^ i.1) //
87 PrimePowerCompletedCoeffCompatibleInClass (ℓ := ℓ) (G := G) C x}
89/-- The projection from the pro-\(C\)-indexed coefficient limit to one finite stage. -/
90def primePowerCompletedCoeffProjectionInClass
91 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
92 PrimePowerCompletedCoeffInClass ℓ G C → ModNCompletedCoeff (ℓ ^ i.1) :=
93 (primePowerCompletedCoeffSystemInClass ℓ G C).projection i
95/--
96The zero element of the class-indexed prime-power completed coefficient ring is the compatible
97family of finite-stage zero elements.
98-/
99instance instZeroPrimePowerCompletedCoeffInClass
100 (C : ProCGroups.FiniteGroupClass.{u}) :
101 Zero (PrimePowerCompletedCoeffInClass ℓ G C) where
102 zero := ⟨fun _ => 0, by
103 dsimp [PrimePowerCompletedCoeffCompatibleInClass]
104 intro i j hij
105 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
106 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
107 exact map_zero
108 (modNCompletedCoeffMap
109 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
110 (primePow_dvd_primePow (ℓ := ℓ) hij.1))⟩
112/--
113Addition in the prime-power completed coefficient ring is defined coordinatewise through
114finite-stage coefficient additions.
115-/
116instance instAddPrimePowerCompletedCoeffInClass
117 (C : ProCGroups.FiniteGroupClass.{u}) :
118 Add (PrimePowerCompletedCoeffInClass ℓ G C) where
119 add x y := ⟨fun i =>
120 (show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i), by
121 dsimp [PrimePowerCompletedCoeffCompatibleInClass]
122 intro i j hij
123 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
124 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
125 change modNCompletedCoeffMap
126 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
127 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
128 ((show ZMod (ℓ ^ j.1) from x.1 j) + (show ZMod (ℓ ^ j.1) from y.1 j)) =
129 (show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i)
130 rw [map_add]
131 exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩
133/--
134Negation on the class-indexed prime-power completed coefficient ring is defined coordinatewise
135through finite-stage coefficient negations.
136-/
137instance instNegPrimePowerCompletedCoeffInClass
138 (C : ProCGroups.FiniteGroupClass.{u}) :
139 Neg (PrimePowerCompletedCoeffInClass ℓ G C) where
140 neg x := ⟨fun i => -(show ZMod (ℓ ^ i.1) from x.1 i), by
141 dsimp [PrimePowerCompletedCoeffCompatibleInClass]
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 (-(show ZMod (ℓ ^ j.1) from x.1 j)) =
149 -(show ZMod (ℓ ^ i.1) from x.1 i)
150 rw [map_neg]
151 exact congrArg Neg.neg (x.2 i j hij)⟩
153/--
154Subtraction in the class-indexed prime-power completed coefficient ring is defined
155coordinatewise through finite-stage coefficient-ring subtractions.
156-/
157instance instSubPrimePowerCompletedCoeffInClass
158 (C : ProCGroups.FiniteGroupClass.{u}) :
159 Sub (PrimePowerCompletedCoeffInClass ℓ G C) where
160 sub x y := ⟨fun i =>
161 (show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 i), by
162 dsimp [PrimePowerCompletedCoeffCompatibleInClass]
163 intro i j hij
164 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
165 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
166 change modNCompletedCoeffMap
167 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
168 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
169 ((show ZMod (ℓ ^ j.1) from x.1 j) - (show ZMod (ℓ ^ j.1) from y.1 j)) =
170 (show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 i)
171 rw [map_sub]
172 exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩
174omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
175/-- The finite-stage projection sends \(0\) to \(0\). -/
176@[simp]
177theorem primePowerCompletedCoeffProjectionInClass_zero
178 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
179 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i
180 (0 : PrimePowerCompletedCoeffInClass ℓ G C) = 0 := by
181 rfl
183omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
184/-- The class-indexed prime-power coefficient projection preserves addition. -/
185@[simp]
186theorem primePowerCompletedCoeffProjectionInClass_add
187 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
188 (x y : PrimePowerCompletedCoeffInClass ℓ G C) :
189 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i (x + y) =
190 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i x +
191 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i y := by
192 rfl
194omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
195/-- The class-indexed prime-power coefficient projection preserves negation. -/
196@[simp]
197theorem primePowerCompletedCoeffProjectionInClass_neg
198 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
199 (x : PrimePowerCompletedCoeffInClass ℓ G C) :
200 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i (-x) =
201 -primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i x := by
202 rfl
204omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
205/-- The class-indexed prime-power coefficient projection preserves subtraction. -/
206@[simp]
207theorem primePowerCompletedCoeffProjectionInClass_sub
208 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
209 (x y : PrimePowerCompletedCoeffInClass ℓ G C) :
210 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i (x - y) =
211 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i x -
212 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i y := by
213 rfl
215/--
216The class-restricted prime-power completed group algebra carries a canonical augmentation to the
217pro-\(C\)-indexed coefficient limit.
218-/
219def primePowerCompletedGroupAlgebraAugmentationInClass
220 (C : ProCGroups.FiniteGroupClass.{u}) :
221 PrimePowerCompletedGroupAlgebraInClass ℓ G C →
222 PrimePowerCompletedCoeffInClass ℓ G C := by
223 intro x
224 refine ⟨fun i => ?_, ?_⟩
225 · letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
226 exact modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2 (x.1 i)
227 · dsimp [PrimePowerCompletedCoeffCompatibleInClass]
228 intro i j hij
229 letI : Fact (0 < ℓ ^ i.1) := ⟨primePower_pos ℓ i.1⟩
230 letI : Fact (0 < ℓ ^ j.1) := ⟨primePower_pos ℓ j.1⟩
231 calc
232 modNCompletedCoeffMap
233 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
234 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
235 (modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ j.1) G C j.2 (x.1 j))
236 =
237 modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2
238 (primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij (x.1 j)) := by
239 symm
240 exact congrFun
241 (congrArg DFunLike.coe
242 (primePowerCompletedGroupAlgebraStageAugmentationInClass_comp_transition
243 (ℓ := ℓ) (G := G) C hij)) (x.1 j)
244 _ =
245 modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2 (x.1 i) := by
246 have hx :
247 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
248 (x.1 j) = x.1 i :=
249 x.2 i j hij
250 exact congrArg
251 (modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2) hx
253omit [Fact (0 < ℓ)] in
254/--
255Projecting the class-indexed prime-power completed augmentation to a coefficient stage agrees
256with the corresponding finite-stage augmentation.
257-/
258@[simp]
259theorem primePowerCompletedCoeffProjectionInClass_augmentation
260 (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
261 (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
262 primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i
263 (primePowerCompletedGroupAlgebraAugmentationInClass (ℓ := ℓ) (G := G) C x) =
264 modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2
265 (primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x) := rfl
267omit [Fact (0 < ℓ)] in
268/--
269The class-indexed completed group-algebra augmentation has a canonical section, obtained by
270placing each compatible coefficient system on the identity monomial at every finite stage.
271-/
272theorem primePowerCompletedGroupAlgebraAugmentationInClass_surjective
273 (C : ProCGroups.FiniteGroupClass.{u}) :
274 Function.Surjective
275 (primePowerCompletedGroupAlgebraAugmentationInClass (ℓ := ℓ) (G := G) C) := by
276 intro x
277 refine ⟨⟨fun i => ?_, ?_⟩, ?_⟩
278 · exact MonoidAlgebra.single
279 (1 : CompletedGroupAlgebraQuotientInClass G C i.2) (x.1 i)
280 · intro i j hij
281 change
282 primePowerCompletedGroupAlgebraTransitionInClass (ℓ := ℓ) (G := G) C hij
283 (MonoidAlgebra.single
284 (1 : CompletedGroupAlgebraQuotientInClass G C j.2) (x.1 j)) =
285 MonoidAlgebra.single
286 (1 : CompletedGroupAlgebraQuotientInClass G C i.2) (x.1 i)
287 rw [primePowerCompletedGroupAlgebraTransitionInClass_single]
288 have hmapone :
289 (OpenNormalSubgroupInClass.map
290 (C := C) (G := G)
291 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2)
292 (1 : CompletedGroupAlgebraQuotientInClass G C j.2) = 1 :=
293 (OpenNormalSubgroupInClass.map
294 (C := C) (G := G)
295 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2).map_one
296 rw [hmapone]
297 have hxcoeff :
298 modNCompletedCoeffMap
299 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
300 (primePow_dvd_primePow (ℓ := ℓ) hij.1) (x.1 j) = x.1 i := by
301 simpa [primePowerCompletedCoeffSystemInClass] using x.2 i j hij
302 exact congrArg
303 (fun a : ModNCompletedCoeff (ℓ ^ i.1) =>
304 MonoidAlgebra.single
305 (1 : CompletedGroupAlgebraQuotientInClass G C i.2) a)
306 hxcoeff
307 · apply Subtype.ext
308 funext i
309 change
310 modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2
311 (MonoidAlgebra.single
312 (1 : CompletedGroupAlgebraQuotientInClass G C i.2) (x.1 i)) =
313 x.1 i
314 simp only [modNCompletedGroupAlgebraStageAugmentationInClass_single]
317end
319end FoxDifferential