Source: ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Core
1import ProCGroups.FoxDifferential.Common.CrossedDifferentialModule
2import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.StageCoeffMap
3import ProCGroups.Completion.ProCInteger
5/-!
6# Fox differential: completed — \(\mathbb{Z}_C\) coefficients — core
8The principal declarations in this module are:
10- `ZCCoeff`
11 The pro-\(C\) integer coefficient ring.
12- `ZCCompletedGroupAlgebraIndex`
13 The two-parameter finite-stage index for \(\mathbb{Z}_C\llbracket H\rrbracket\): a coefficient
14 quotient of \(\mathbb{Z}_C\) and a finite \(C\)-quotient of \(H\).
15- `zcCompletedGroupAlgebraTransition_of`
16 Evaluation of a pro-\(C\) transition on a group-like basis element.
17- `zcCompletedGroupAlgebraTransition_single`
18 The transition map \(R[G/V] \to R[G/U]\) sends a singleton supported at a class of \(G/V\) to the
19 singleton supported at its image in \(G/U\), with the same coefficient.
20-/
22namespace FoxDifferential
24noncomputable section
26open scoped BigOperators
27open ProCGroups.Completion
28open ProCGroups.InverseSystems
29open ProCGroups.ProC
31universe u v
33/-- The pro-\(C\) integer coefficient ring. -/
34abbrev ZCCoeff (C : ProCGroups.FiniteGroupClass.{u}) : Type _ :=
35 ProCIntegerLimitCarrier C
37/--
38The two-parameter finite-stage index for \(\mathbb{Z}_C\llbracket H\rrbracket\): a coefficient
39quotient of \(\mathbb{Z}_C\) and a finite \(C\)-quotient of \(H\).
40-/
41abbrev ZCCompletedGroupAlgebraIndex
42 (C : ProCGroups.FiniteGroupClass.{u})
43 (H : Type u) [Group H] [TopologicalSpace H] : Type u :=
44 ProCIntegerIndex C × CompletedGroupAlgebraIndexInClass H C
46/-- A finite stage \((\mathbb{Z}/n\mathbb{Z})[H/U]\) of the pro-\(C\) completed group algebra. -/
47abbrev ZCCompletedGroupAlgebraStage
48 (C : ProCGroups.FiniteGroupClass.{u})
49 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
50 (i : ZCCompletedGroupAlgebraIndex C H) : Type u :=
51 ModNCompletedGroupAlgebraStageInClass i.1.modulus H C i.2
53/--
54Transition maps for the true pro-\(C\) completed group algebra. The coefficient direction is
55divisibility of allowed pro-\(C\) integer moduli, and the group direction is refinement of
56\(C\)-quotients.
57-/
58def zcCompletedGroupAlgebraTransition
59 (C : ProCGroups.FiniteGroupClass.{u})
60 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
61 {i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j) :
62 ZCCompletedGroupAlgebraStage C H j →+* ZCCompletedGroupAlgebraStage C H i := by
63 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
64 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
65 exact
66 (modNCompletedGroupAlgebraStageCoeffMapInClass
67 (n := i.1.modulus) (m := j.1.modulus) (G := H) C i.2 hij.1).comp
68 (modNCompletedGroupAlgebraTransitionInClass (n := j.1.modulus) (G := H) C hij.2)
70/-- Evaluation of a pro-\(C\) transition on a group-like basis element. -/
71@[simp]
72theorem zcCompletedGroupAlgebraTransition_of
73 (C : ProCGroups.FiniteGroupClass.{u})
74 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
75 {i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j)
76 (q : CompletedGroupAlgebraQuotientInClass H C j.2) :
77 zcCompletedGroupAlgebraTransition C H hij
78 (MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus) _ q) =
79 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus) _
80 ((OpenNormalSubgroupInClass.map
81 (C := C) (G := H)
82 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q) := by
83 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
84 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
85 rw [zcCompletedGroupAlgebraTransition, RingHom.comp_apply]
86 change
87 modNCompletedGroupAlgebraStageCoeffMapInClass
88 (n := i.1.modulus) (m := j.1.modulus) (G := H) C i.2 hij.1
89 (MonoidAlgebra.mapDomain
90 (OpenNormalSubgroupInClass.map
91 (C := C) (G := H)
92 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2)
93 (MonoidAlgebra.single q 1)) =
94 MonoidAlgebra.single
95 ((OpenNormalSubgroupInClass.map
96 (C := C) (G := H)
97 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q) 1
98 rw [MonoidAlgebra.mapDomain_single,
99 modNCompletedGroupAlgebraStageCoeffMapInClass_single_apply, map_one]
100 rfl
102/--
103The transition map \(R[G/V] \to R[G/U]\) sends a singleton supported at a class of \(G/V\) to
104the singleton supported at its image in \(G/U\), with the same coefficient.
105-/
106@[simp]
107theorem zcCompletedGroupAlgebraTransition_single
108 (C : ProCGroups.FiniteGroupClass.{u})
109 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
110 {i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j)
111 (q : CompletedGroupAlgebraQuotientInClass H C j.2)
112 (a : ModNCompletedCoeff j.1.modulus) :
113 zcCompletedGroupAlgebraTransition C H hij (MonoidAlgebra.single q a) =
114 MonoidAlgebra.single
115 ((OpenNormalSubgroupInClass.map
116 (C := C) (G := H)
117 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)
118 (modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1 a) := by
119 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
120 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
121 rw [zcCompletedGroupAlgebraTransition, RingHom.comp_apply]
122 change
123 modNCompletedGroupAlgebraStageCoeffMapInClass
124 (n := i.1.modulus) (m := j.1.modulus) (G := H) C i.2 hij.1
125 (MonoidAlgebra.mapDomain
126 (OpenNormalSubgroupInClass.map
127 (C := C) (G := H)
128 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2)
129 (MonoidAlgebra.single q a)) =
130 MonoidAlgebra.single
131 ((OpenNormalSubgroupInClass.map
132 (C := C) (G := H)
133 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)
134 (modNCompletedCoeffMap
135 (n := i.1.modulus) (m := j.1.modulus) hij.1 a)
136 rw [MonoidAlgebra.mapDomain_single,
137 modNCompletedGroupAlgebraStageCoeffMapInClass_single_apply]
138 rfl
140/--
141The \(\mathbb{Z}_C\)-completed group-algebra transition for a reflexive refinement is the identity
142ring homomorphism.
143-/
144@[simp]
145theorem zcCompletedGroupAlgebraTransition_id
146 (C : ProCGroups.FiniteGroupClass.{u})
147 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
148 (i : ZCCompletedGroupAlgebraIndex C H) :
149 zcCompletedGroupAlgebraTransition C H (le_rfl : i ≤ i) = RingHom.id _ := by
150 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
151 rw [zcCompletedGroupAlgebraTransition]
152 rw [modNCompletedGroupAlgebraTransitionInClass_id,
153 modNCompletedGroupAlgebraStageCoeffMapInClass_rfl]
154 simp only [RingHomCompTriple.comp_eq]
156/-- \(\mathbb{Z}_C\)-completed group-algebra transitions compose along quotient refinements. -/
157@[simp 900]
158theorem zcCompletedGroupAlgebraTransition_comp
159 (C : ProCGroups.FiniteGroupClass.{u})
160 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
161 {i j k : ZCCompletedGroupAlgebraIndex C H}
162 (hij : i ≤ j) (hjk : j ≤ k) :
163 (zcCompletedGroupAlgebraTransition C H hij).comp
164 (zcCompletedGroupAlgebraTransition C H hjk) =
165 zcCompletedGroupAlgebraTransition C H (hij.trans hjk) := by
166 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
167 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
168 letI : Fact (0 < k.1.modulus) := ⟨k.1.positive⟩
169 apply RingHom.ext
170 intro x
171 refine MonoidAlgebra.induction_on
172 (p := fun x =>
173 ((zcCompletedGroupAlgebraTransition C H hij).comp
174 (zcCompletedGroupAlgebraTransition C H hjk)) x =
175 zcCompletedGroupAlgebraTransition C H (hij.trans hjk) x)
176 x ?_ ?_ ?_
177 · intro q
178 rw [RingHom.comp_apply, zcCompletedGroupAlgebraTransition_of C H hjk,
179 zcCompletedGroupAlgebraTransition_of C H (hij.trans hjk)]
180 change
181 zcCompletedGroupAlgebraTransition C H hij
182 (MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
183 (CompletedGroupAlgebraQuotientInClass H C j.2)
184 ((OpenNormalSubgroupInClass.map
185 (C := C) (G := H)
186 (U := OrderDual.ofDual j.2) (V := OrderDual.ofDual k.2) hjk.2) q)) =
187 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
188 (CompletedGroupAlgebraQuotientInClass H C i.2)
189 ((OpenNormalSubgroupInClass.map
190 (C := C) (G := H)
191 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual k.2) (hij.2.trans hjk.2)) q)
192 rw [zcCompletedGroupAlgebraTransition_of C H hij]
193 congr 1
194 exact congrFun
195 (congrArg DFunLike.coe
196 (OpenNormalSubgroupInClass.map_comp
197 (C := C) (G := H)
198 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2)
199 (W := OrderDual.ofDual k.2) hij.2 hjk.2)) q
200 · intro x y hx hy
201 simp only [RingHom.map_add, hx, hy]
202 · intro a x hx
203 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
204 have hcoeff :
205 ((zcCompletedGroupAlgebraTransition C H hij).comp
206 (zcCompletedGroupAlgebraTransition C H hjk))
207 (algebraMap (ModNCompletedCoeff k.1.modulus)
208 (ZCCompletedGroupAlgebraStage C H k) a) =
209 zcCompletedGroupAlgebraTransition C H (hij.trans hjk)
210 (algebraMap (ModNCompletedCoeff k.1.modulus)
211 (ZCCompletedGroupAlgebraStage C H k) a) := by
212 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
213 simp only [zcCompletedGroupAlgebraTransition, modNCompletedGroupAlgebraStageCoeffMapInClass,
214 modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe,
215 modNCompletedGroupAlgebraTransitionInClass, map_intCast]
216 rw [hcoeff]
218/-- The inverse system defining the pro-\(C\) completed group algebra. -/
219def zcCompletedGroupAlgebraSystem
220 (C : ProCGroups.FiniteGroupClass.{u})
221 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
222 InverseSystem (I := ZCCompletedGroupAlgebraIndex C H) where
223 X := ZCCompletedGroupAlgebraStage C H
224 topologicalSpace := fun _ => ⊥
225 map := fun {i j} hij => zcCompletedGroupAlgebraTransition C H hij
226 continuous_map := by
227 intro i j hij
228 letI : TopologicalSpace (ZCCompletedGroupAlgebraStage C H i) := ⊥
229 letI : TopologicalSpace (ZCCompletedGroupAlgebraStage C H j) := ⊥
230 letI : DiscreteTopology (ZCCompletedGroupAlgebraStage C H j) := ⟨rfl⟩
231 exact continuous_of_discreteTopology
232 map_id := by
233 intro i
234 funext x
235 exact congrFun
236 (congrArg DFunLike.coe
237 (zcCompletedGroupAlgebraTransition_id C H i)) x
238 map_comp := by
239 intro i j k hij hjk
240 funext x
241 exact congrFun
242 (congrArg DFunLike.coe
243 (zcCompletedGroupAlgebraTransition_comp C H hij hjk)) x
245/-- Compatibility for a family of finite \(\mathbb{Z}_C\llbracket H\rrbracket\) stage elements. -/
246def ZCCompletedGroupAlgebraCompatible
247 (C : ProCGroups.FiniteGroupClass.{u})
248 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
249 (x : ∀ i : ZCCompletedGroupAlgebraIndex C H, ZCCompletedGroupAlgebraStage C H i) : Prop :=
250 ∀ i j, ∀ hij : i ≤ j, zcCompletedGroupAlgebraTransition C H hij (x j) = x i
252/-- The completed group algebra \(\mathbb{Z}_C\llbracket H\rrbracket\). -/
253abbrev ZCCompletedGroupAlgebra
254 (C : ProCGroups.FiniteGroupClass.{u})
255 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] : Type u :=
256 {x : ∀ i : ZCCompletedGroupAlgebraIndex C H, ZCCompletedGroupAlgebraStage C H i //
257 ZCCompletedGroupAlgebraCompatible C H x}
259/--
260The projection from \(\mathbb{Z}_C\llbracket H\rrbracket\) to a finite \(C\)-coefficient and
261\(C\)-quotient stage.
262-/
263abbrev zcCompletedGroupAlgebraProjection
264 (C : ProCGroups.FiniteGroupClass.{u})
265 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
266 (i : ZCCompletedGroupAlgebraIndex C H) :
267 ZCCompletedGroupAlgebra C H → ZCCompletedGroupAlgebraStage C H i :=
268 fun x => x.1 i
270section Ring
272variable (C : ProCGroups.FiniteGroupClass.{u})
273variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
275/--
276The zero element is defined coordinatewise as the compatible family of zero elements at all
277finite stages.
278-/
279instance instZeroZCCompletedGroupAlgebra : Zero (ZCCompletedGroupAlgebra C H) where
280 zero := ⟨fun i => 0, by intro i j hij; exact map_zero _⟩
282/--
283Addition on \(\mathbb{Z}_C\llbracket H\rrbracket\) is defined coordinatewise through
284finite-stage group-algebra additions.
285-/
286instance instAddZCCompletedGroupAlgebra : Add (ZCCompletedGroupAlgebra C H) where
287 add x y := ⟨fun i => x.1 i + y.1 i, by
288 intro i j hij
289 rw [map_add]
290 exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩
292/--
293Negation on the \(\mathbb{Z}_C\)-completed group algebra is defined coordinatewise through
294finite-stage group-algebra negations.
295-/
296instance instNegZCCompletedGroupAlgebra : Neg (ZCCompletedGroupAlgebra C H) where
297 neg x := ⟨fun i => -x.1 i, by
298 intro i j hij
299 rw [map_neg]
300 exact congrArg Neg.neg (x.2 i j hij)⟩
302/--
303Subtraction on the completed group algebra is defined coordinatewise through the finite-stage
304group-algebra subtractions.
305-/
306instance instSubZCCompletedGroupAlgebra : Sub (ZCCompletedGroupAlgebra C H) where
307 sub x y := ⟨fun i => x.1 i - y.1 i, by
308 intro i j hij
309 rw [map_sub]
310 exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩
312/--
313The completed group algebra carries coefficient-ring scalar multiplication by applying the
314scalar action at every finite quotient stage.
315-/
316instance instSMulNatZCCompletedGroupAlgebra : SMul ℕ (ZCCompletedGroupAlgebra C H) where
317 smul n x := ⟨fun i => n • x.1 i, by
318 intro i j hij
319 rw [map_nsmul]
320 exact congrArg (n • ·) (x.2 i j hij)⟩
322/--
323The completed group algebra carries coefficient-ring scalar multiplication by applying the
324scalar action at every finite quotient stage.
325-/
326instance instSMulIntZCCompletedGroupAlgebra : SMul ℤ (ZCCompletedGroupAlgebra C H) where
327 smul n x := ⟨fun i => n • x.1 i, by
328 intro i j hij
329 rw [map_zsmul]
330 exact congrArg (n • ·) (x.2 i j hij)⟩
332/--
333The zero element of \(\mathbb{Z}_C\llbracket H\rrbracket\) is represented by the compatible
334family of finite-stage zero elements.
335-/
336@[simp]
337theorem coe_zero_zcCompletedGroupAlgebra :
338 ((0 : ZCCompletedGroupAlgebra C H) :
339 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = 0 := by
340 funext i
341 rfl
343/--
344The underlying finite-stage family of a sum in \(\mathbb{Z}_C\llbracket H\rrbracket\) is the sum
345of the underlying finite-stage families.
346-/
347@[simp]
348theorem coe_add_zcCompletedGroupAlgebra (x y : ZCCompletedGroupAlgebra C H) :
349 ((x + y : ZCCompletedGroupAlgebra C H) :
350 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = x + y := by
351 funext i
352 rfl
354/--
355The underlying finite-stage family of a negation in \(\mathbb{Z}_C\llbracket H\rrbracket\) is
356the negation of the underlying finite-stage family.
357-/
358@[simp]
359theorem coe_neg_zcCompletedGroupAlgebra (x : ZCCompletedGroupAlgebra C H) :
360 ((-x : ZCCompletedGroupAlgebra C H) :
361 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = -x := by
362 funext i
363 rfl
365/--
366The underlying finite-stage family of a difference in \(\mathbb{Z}_C\llbracket H\rrbracket\) is
367the difference of the underlying finite-stage families.
368-/
369@[simp]
370theorem coe_sub_zcCompletedGroupAlgebra (x y : ZCCompletedGroupAlgebra C H) :
371 ((x - y : ZCCompletedGroupAlgebra C H) :
372 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = x - y := by
373 funext i
374 rfl
376/--
377Natural-number scalar multiplication in \(\mathbb{Z}_C\llbracket H\rrbracket\) is computed
378coordinatewise at every finite stage.
379-/
380@[simp]
381theorem coe_nsmul_zcCompletedGroupAlgebra (n : ℕ) (x : ZCCompletedGroupAlgebra C H) :
382 ((n • x : ZCCompletedGroupAlgebra C H) :
383 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = n • x := by
384 funext i
385 rfl
387/--
388Integer scalar multiplication in \(\mathbb{Z}_C\llbracket H\rrbracket\) is computed
389coordinatewise at every finite stage.
390-/
391@[simp]
392theorem coe_zsmul_zcCompletedGroupAlgebra (n : ℤ) (x : ZCCompletedGroupAlgebra C H) :
393 ((n • x : ZCCompletedGroupAlgebra C H) :
394 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = n • x := by
395 funext i
396 rfl
398/-- A temporary additive-group structure used while constructing the stronger ring instance. -/
399local instance instAddCommGroupZCCompletedGroupAlgebra :
400 AddCommGroup (ZCCompletedGroupAlgebra C H) :=
401 Function.Injective.addCommGroup
402 (fun x : ZCCompletedGroupAlgebra C H =>
403 (x : (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i))
404 Subtype.val_injective
405 (coe_zero_zcCompletedGroupAlgebra (C := C) (H := H))
406 (coe_add_zcCompletedGroupAlgebra (C := C) (H := H))
407 (coe_neg_zcCompletedGroupAlgebra (C := C) (H := H))
408 (coe_sub_zcCompletedGroupAlgebra (C := C) (H := H))
409 (fun x n => coe_nsmul_zcCompletedGroupAlgebra (C := C) (H := H) n x)
410 (fun x n => coe_zsmul_zcCompletedGroupAlgebra (C := C) (H := H) n x)
412/--
413The unit of \(\mathbb{Z}_C\llbracket H\rrbracket\) is the compatible family of finite-stage
414units.
415-/
416instance instOneZCCompletedGroupAlgebra : One (ZCCompletedGroupAlgebra C H) where
417 one := ⟨fun i => 1, by intro i j hij; exact map_one _⟩
419/--
420Multiplication on the completed group algebra is defined coordinatewise through the finite-stage
421group-algebra products.
422-/
423instance instMulZCCompletedGroupAlgebra : Mul (ZCCompletedGroupAlgebra C H) where
424 mul x y := ⟨fun i => x.1 i * y.1 i, by
425 intro i j hij
426 rw [map_mul]
427 exact congrArg₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩
429/--
430Natural number casts in \(\mathbb{Z}_C\llbracket H\rrbracket\) are computed coordinatewise from
431finite-stage natural number casts.
432-/
433instance instNatCastZCCompletedGroupAlgebra : NatCast (ZCCompletedGroupAlgebra C H) where
434 natCast n := ⟨fun i => n, by intro i j hij; exact map_natCast _ _⟩
436/--
437Integer casts in \(\mathbb{Z}_C\llbracket H\rrbracket\) are computed coordinatewise from
438finite-stage integer casts.
439-/
440instance instIntCastZCCompletedGroupAlgebra : IntCast (ZCCompletedGroupAlgebra C H) where
441 intCast n := ⟨fun i => n, by intro i j hij; exact map_intCast _ _⟩
443/-- The completed group algebra has powers computed at every finite-stage coordinate. -/
444instance instPowZCCompletedGroupAlgebra : Pow (ZCCompletedGroupAlgebra C H) ℕ where
445 pow x n := ⟨fun i => x.1 i ^ n, by
446 intro i j hij
447 rw [map_pow]
448 exact congrArg (fun z => z ^ n) (x.2 i j hij)⟩
450/--
451The unit of \(\mathbb{Z}_C\llbracket H\rrbracket\) is represented by the compatible family of
452finite-stage units.
453-/
454@[simp]
455theorem coe_one_zcCompletedGroupAlgebra :
456 ((1 : ZCCompletedGroupAlgebra C H) :
457 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = 1 := by
458 funext i
459 rfl
461/--
462The underlying finite-stage family of a product in \(\mathbb{Z}_C\llbracket H\rrbracket\) is the
463product of the underlying finite-stage families.
464-/
465@[simp]
466theorem coe_mul_zcCompletedGroupAlgebra (x y : ZCCompletedGroupAlgebra C H) :
467 ((x * y : ZCCompletedGroupAlgebra C H) :
468 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = x * y := by
469 funext i
470 rfl
472/--
473Natural number casts in the completed group algebra are computed coefficientwise after
474projection to every completed finite quotient stage.
475-/
476@[simp]
477theorem coe_natCast_zcCompletedGroupAlgebra (n : ℕ) :
478 ((n : ZCCompletedGroupAlgebra C H) :
479 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = n := by
480 funext i
481 rfl
483/--
484Integer casts in the completed group algebra are computed coefficientwise after projection to
485every completed finite quotient stage.
486-/
487@[simp]
488theorem coe_intCast_zcCompletedGroupAlgebra (n : ℤ) :
489 ((n : ZCCompletedGroupAlgebra C H) :
490 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = n := by
491 funext i
492 rfl
494/--
495Powers in \(\mathbb{Z}_C\llbracket H\rrbracket\) are computed coordinatewise at every finite
496stage.
497-/
498@[simp]
499theorem coe_pow_zcCompletedGroupAlgebra (x : ZCCompletedGroupAlgebra C H) (n : ℕ) :
500 ((x ^ n : ZCCompletedGroupAlgebra C H) :
501 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = x ^ n := by
502 funext i
503 rfl
505/--
506The completed group algebra is a ring because all ring operations and ring axioms are inherited
507coordinatewise from the finite-stage group algebras.
508-/
509instance instRingZCCompletedGroupAlgebra : Ring (ZCCompletedGroupAlgebra C H) :=
510 Function.Injective.ring
511 (fun x : ZCCompletedGroupAlgebra C H =>
512 (x : (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i))
513 Subtype.val_injective
514 (coe_zero_zcCompletedGroupAlgebra (C := C) (H := H))
515 (coe_one_zcCompletedGroupAlgebra (C := C) (H := H))
516 (coe_add_zcCompletedGroupAlgebra (C := C) (H := H))
517 (coe_mul_zcCompletedGroupAlgebra (C := C) (H := H))
518 (coe_neg_zcCompletedGroupAlgebra (C := C) (H := H))
519 (coe_sub_zcCompletedGroupAlgebra (C := C) (H := H))
520 (fun n x => coe_nsmul_zcCompletedGroupAlgebra (C := C) (H := H) n x)
521 (fun n x => coe_zsmul_zcCompletedGroupAlgebra (C := C) (H := H) n x)
522 (fun x n => coe_pow_zcCompletedGroupAlgebra (C := C) (H := H) x n)
523 (by intro n; exact coe_natCast_zcCompletedGroupAlgebra (C := C) (H := H) n)
524 (by intro z; exact coe_intCast_zcCompletedGroupAlgebra (C := C) (H := H) z)
526/-- The finite-stage projection sends \(1\) to \(1\). -/
527@[simp]
528theorem zcCompletedGroupAlgebraProjection_one
529 (i : ZCCompletedGroupAlgebraIndex C H) :
530 zcCompletedGroupAlgebraProjection C H i (1 : ZCCompletedGroupAlgebra C H) = 1 :=
531 rfl
533/-- The finite-stage projection preserves multiplication. -/
534@[simp]
535theorem zcCompletedGroupAlgebraProjection_mul
536 (i : ZCCompletedGroupAlgebraIndex C H) (x y : ZCCompletedGroupAlgebra C H) :
537 zcCompletedGroupAlgebraProjection C H i (x * y) =
538 zcCompletedGroupAlgebraProjection C H i x *
539 zcCompletedGroupAlgebraProjection C H i y :=
540 rfl
542/-- The finite-stage projection sends \(0\) to \(0\). -/
543@[simp]
544theorem zcCompletedGroupAlgebraProjection_zero
545 (i : ZCCompletedGroupAlgebraIndex C H) :
546 zcCompletedGroupAlgebraProjection C H i (0 : ZCCompletedGroupAlgebra C H) = 0 :=
547 rfl
549/-- The finite-stage projection preserves addition. -/
550@[simp]
551theorem zcCompletedGroupAlgebraProjection_add
552 (i : ZCCompletedGroupAlgebraIndex C H) (x y : ZCCompletedGroupAlgebra C H) :
553 zcCompletedGroupAlgebraProjection C H i (x + y) =
554 zcCompletedGroupAlgebraProjection C H i x +
555 zcCompletedGroupAlgebraProjection C H i y :=
556 rfl
558/-- The finite-stage projection preserves negation. -/
559@[simp]
560theorem zcCompletedGroupAlgebraProjection_neg
561 (i : ZCCompletedGroupAlgebraIndex C H) (x : ZCCompletedGroupAlgebra C H) :
562 zcCompletedGroupAlgebraProjection C H i (-x) =
563 -zcCompletedGroupAlgebraProjection C H i x :=
564 rfl
566/-- The finite-stage projection preserves subtraction. -/
567@[simp]
568theorem zcCompletedGroupAlgebraProjection_sub
569 (i : ZCCompletedGroupAlgebraIndex C H) (x y : ZCCompletedGroupAlgebra C H) :
570 zcCompletedGroupAlgebraProjection C H i (x - y) =
571 zcCompletedGroupAlgebraProjection C H i x -
572 zcCompletedGroupAlgebraProjection C H i y :=
573 rfl
575/--
576The projection from \(\mathbb{Z}_C\llbracket H\rrbracket\) to a finite stage is bundled as a
577ring homomorphism.
578-/
579def zcCompletedGroupAlgebraProjectionRingHom
580 (i : ZCCompletedGroupAlgebraIndex C H) :
581 ZCCompletedGroupAlgebra C H →+* ZCCompletedGroupAlgebraStage C H i where
582 toFun := zcCompletedGroupAlgebraProjection C H i
583 map_zero' := zcCompletedGroupAlgebraProjection_zero C H i
584 map_one' := zcCompletedGroupAlgebraProjection_one C H i
585 map_add' := zcCompletedGroupAlgebraProjection_add C H i
586 map_mul' := zcCompletedGroupAlgebraProjection_mul C H i
588/--
589The ring-homomorphism projection has the same underlying coordinate map as the finite-stage
590projection.
591-/
592@[simp]
593theorem zcCompletedGroupAlgebraProjectionRingHom_apply
594 (i : ZCCompletedGroupAlgebraIndex C H) (x : ZCCompletedGroupAlgebra C H) :
595 zcCompletedGroupAlgebraProjectionRingHom C H i x =
596 zcCompletedGroupAlgebraProjection C H i x :=
597 rfl
599/-- The \(\mathbb{Z}_C\)-completed group algebra stage is a module over its coefficient ring. -/
600instance instModuleZCCompletedGroupAlgebraStage
601 (i : ZCCompletedGroupAlgebraIndex C H) :
602 Module (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebraStage C H i) :=
603 Module.compHom _ (zcCompletedGroupAlgebraProjectionRingHom C H i)
605/-- Finite-stage projections separate points of \(\mathbb{Z}_C\llbracket H\rrbracket\). -/
606theorem zcCompletedGroupAlgebraProjection_ext
607 {x y : ZCCompletedGroupAlgebra C H}
608 (h : ∀ i : ZCCompletedGroupAlgebraIndex C H,
609 zcCompletedGroupAlgebraProjection C H i x =
610 zcCompletedGroupAlgebraProjection C H i y) :
611 x = y := by
612 apply Subtype.ext
613 funext i
614 exact h i
616/--
617Finite projections from \(\mathbb{Z}_C\llbracket H\rrbracket\) commute with the finite
618transition maps.
619-/
620@[simp]
621theorem zcCompletedGroupAlgebraTransition_projection
622 {i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j)
623 (x : ZCCompletedGroupAlgebra C H) :
624 zcCompletedGroupAlgebraTransition C H hij
625 (zcCompletedGroupAlgebraProjection C H j x) =
626 zcCompletedGroupAlgebraProjection C H i x :=
627 x.2 i j hij
629/-- A finite stage projection as a linear map over the completed group algebra. -/
630def zcCompletedGroupAlgebraProjectionLinearMap
631 (i : ZCCompletedGroupAlgebraIndex C H) :
632 ZCCompletedGroupAlgebra C H →ₗ[ZCCompletedGroupAlgebra C H]
633 ZCCompletedGroupAlgebraStage C H i where
634 toFun := zcCompletedGroupAlgebraProjection C H i
635 map_add' x y := zcCompletedGroupAlgebraProjection_add C H i x y
636 map_smul' r x := by
637 change zcCompletedGroupAlgebraProjection C H i (r * x) =
638 zcCompletedGroupAlgebraProjection C H i r *
639 zcCompletedGroupAlgebraProjection C H i x
640 exact zcCompletedGroupAlgebraProjection_mul C H i r x
642/--
643The \(\mathbb{Z}_C\)-completed group-algebra projection, bundled as a linear map, acts by its
644defining finite-stage coordinate formula.
645-/
646@[simp]
647theorem zcCompletedGroupAlgebraProjectionLinearMap_apply
648 (i : ZCCompletedGroupAlgebraIndex C H) (x : ZCCompletedGroupAlgebra C H) :
649 zcCompletedGroupAlgebraProjectionLinearMap C H i x =
650 zcCompletedGroupAlgebraProjection C H i x :=
651 rfl
653end Ring
655/--
656The projection from \(\mathbb{Z}_C\llbracket H\rrbracket\) to a finite stage commutes with
657finite sums.
658-/
659theorem zcCompletedGroupAlgebraProjection_sum
660 (C : ProCGroups.FiniteGroupClass.{u})
661 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
662 {I : Type v} [Fintype I]
663 (j : ZCCompletedGroupAlgebraIndex C H)
664 (f : I → ZCCompletedGroupAlgebra C H) :
665 zcCompletedGroupAlgebraProjection C H j (∑ i : I, f i) =
666 ∑ i : I, zcCompletedGroupAlgebraProjection C H j (f i) := by
667 classical
668 refine Finset.induction_on (s := Finset.univ) ?_ ?_
669 · rfl
670 · intro a s has ih
671 rw [Finset.sum_insert has, Finset.sum_insert has]
672 rw [zcCompletedGroupAlgebraProjection_add, ih]
674/--
675The coefficient element of \(\mathbb{Z}_C\llbracket H\rrbracket\) supported at the identity of
676\(H\).
677-/
678def zcCompletedGroupAlgebraCoeff
679 (C : ProCGroups.FiniteGroupClass.{u})
680 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
681 (a : ZCCoeff C) : ZCCompletedGroupAlgebra C H :=
682 ⟨fun i =>
683 MonoidAlgebra.single
684 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
685 (proCIntegerProj (C := C) i.1 a), by
686 intro i j hij
687 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
688 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
689 rw [zcCompletedGroupAlgebraTransition, RingHom.comp_apply]
690 change
691 modNCompletedGroupAlgebraStageCoeffMapInClass
692 (n := i.1.modulus) (m := j.1.modulus) (G := H) C i.2 hij.1
693 (MonoidAlgebra.mapDomain
694 (OpenNormalSubgroupInClass.map
695 (C := C) (G := H)
696 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2)
697 (MonoidAlgebra.single
698 (1 : CompletedGroupAlgebraQuotientInClass H C j.2)
699 (proCIntegerProj (C := C) j.1 a))) =
700 MonoidAlgebra.single
701 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
702 (proCIntegerProj (C := C) i.1 a)
703 rw [MonoidAlgebra.mapDomain_single,
704 modNCompletedGroupAlgebraStageCoeffMapInClass_single_apply]
705 have ha : modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1
706 (proCIntegerProj (C := C) j.1 a) =
707 proCIntegerProj (C := C) i.1 a :=
708 proCIntegerProj_transition (C := C) hij.1 a
709 have hmap :
710 (OpenNormalSubgroupInClass.map
711 (C := C) (G := H)
712 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2)
713 (1 : CompletedGroupAlgebraQuotientInClass H C j.2) =
714 (1 : CompletedGroupAlgebraQuotientInClass H C i.2) :=
715 map_one _
716 rw [hmap, ha]⟩
718/--
719Coefficient change is performed stagewise: supports are unchanged and coefficients are
720transported by the given ring homomorphism.
721-/
722def zcCompletedGroupAlgebraCoeffMap
723 (C : ProCGroups.FiniteGroupClass.{u})
724 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
725 ZCCoeff C →+* ZCCompletedGroupAlgebra C H where
726 toFun := zcCompletedGroupAlgebraCoeff C H
727 map_zero' := by
728 apply Subtype.ext
729 funext i
730 change
731 MonoidAlgebra.single
732 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
733 (proCIntegerProj (C := C) i.1 0) = 0
734 rw [proCIntegerProj_zero, MonoidAlgebra.single_zero]
735 map_one' := by
736 apply Subtype.ext
737 funext i
738 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
739 change
740 MonoidAlgebra.single
741 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
742 (proCIntegerProj (C := C) i.1 1) = 1
743 rw [proCIntegerProj_one, ← MonoidAlgebra.one_def]
744 map_add' a b := by
745 apply Subtype.ext
746 funext i
747 change
748 MonoidAlgebra.single
749 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
750 (proCIntegerProj (C := C) i.1 (a + b)) =
751 MonoidAlgebra.single
752 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
753 (proCIntegerProj (C := C) i.1 a) +
754 MonoidAlgebra.single
755 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
756 (proCIntegerProj (C := C) i.1 b)
757 rw [proCIntegerProj_add, MonoidAlgebra.single_add]
758 map_mul' a b := by
759 apply Subtype.ext
760 funext i
761 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
762 change MonoidAlgebra.single
763 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
764 (proCIntegerProj (C := C) i.1 (a * b)) =
765 MonoidAlgebra.single
766 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
767 (proCIntegerProj (C := C) i.1 a) *
768 MonoidAlgebra.single
769 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
770 (proCIntegerProj (C := C) i.1 b)
771 simp only [proCIntegerProj_mul, MonoidAlgebra.single_mul_single, mul_one]
773/--
774The completed group-algebra projection commutes with the coefficient-change map at the
775corresponding finite stage.
776-/
777@[simp]
778theorem zcCompletedGroupAlgebraProjection_coeffMap
779 (C : ProCGroups.FiniteGroupClass.{u})
780 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
781 (i : ZCCompletedGroupAlgebraIndex C H) (a : ZCCoeff C) :
782 zcCompletedGroupAlgebraProjection C H i
783 (zcCompletedGroupAlgebraCoeffMap C H a) =
784 MonoidAlgebra.single
785 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
786 (proCIntegerProj (C := C) i.1 a) :=
787 rfl
789/-- The group-like map \(H \to \mathbb{Z}_C\llbracket H\rrbracket\). -/
790def zcGroupLike
791 (C : ProCGroups.FiniteGroupClass.{u})
792 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
793 H →* ZCCompletedGroupAlgebra C H where
794 toFun h := ⟨fun i =>
795 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
796 (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h), by
797 intro i j hij
798 change
799 zcCompletedGroupAlgebraTransition C H hij
800 (MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
801 (CompletedGroupAlgebraQuotientInClass H C j.2) (QuotientGroup.mk h)) =
802 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
803 (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h)
804 rw [zcCompletedGroupAlgebraTransition_of C H hij]
805 rfl⟩
806 map_one' := by
807 apply Subtype.ext
808 funext i
809 change
810 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
811 (CompletedGroupAlgebraQuotientInClass H C i.2)
812 (1 : CompletedGroupAlgebraQuotientInClass H C i.2) = 1
813 exact map_one
814 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
815 (CompletedGroupAlgebraQuotientInClass H C i.2))
816 map_mul' h₁ h₂ := by
817 apply Subtype.ext
818 funext i
819 change
820 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
821 (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk (h₁ * h₂)) =
822 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
823 (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h₁) *
824 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
825 (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h₂)
826 change
827 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
828 (CompletedGroupAlgebraQuotientInClass H C i.2)
829 ((QuotientGroup.mk h₁ :
830 CompletedGroupAlgebraQuotientInClass H C i.2) *
831 (QuotientGroup.mk h₂ :
832 CompletedGroupAlgebraQuotientInClass H C i.2)) =
833 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
834 (CompletedGroupAlgebraQuotientInClass H C i.2)
835 (QuotientGroup.mk h₁) *
836 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
837 (CompletedGroupAlgebraQuotientInClass H C i.2)
838 (QuotientGroup.mk h₂)
839 exact map_mul
840 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
841 (CompletedGroupAlgebraQuotientInClass H C i.2)) _ _
843/--
844Projecting a group-like element of \(\mathbb{Z}_C\llbracket H\rrbracket\) gives its finite-stage
845group-like image.
846-/
847@[simp]
848theorem zcCompletedGroupAlgebraProjection_groupLike
849 (C : ProCGroups.FiniteGroupClass.{u})
850 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
851 (i : ZCCompletedGroupAlgebraIndex C H) (h : H) :
852 zcCompletedGroupAlgebraProjection C H i (zcGroupLike C H h) =
853 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
854 (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h) :=
855 rfl
857/--
858The projection ring homomorphism sends a group-like element to its image in the corresponding
859finite group-algebra stage.
860-/
861@[simp]
862theorem zcCompletedGroupAlgebraProjectionRingHom_groupLike
863 (C : ProCGroups.FiniteGroupClass.{u})
864 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
865 (i : ZCCompletedGroupAlgebraIndex C H) (h : H) :
866 zcCompletedGroupAlgebraProjectionRingHom C H i (zcGroupLike C H h) =
867 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
868 (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h) :=
869 zcCompletedGroupAlgebraProjection_groupLike C H i h
871/-- A completed group-algebra relation \((h - 1)y = 0\) descends to every finite stage. -/
872theorem zcCompletedGroupAlgebra_projection_sub_one_mul_eq_zero
873 (C : ProCGroups.FiniteGroupClass.{u})
874 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
875 (h : H) (y : ZCCompletedGroupAlgebra C H)
876 (i : ZCCompletedGroupAlgebraIndex C H)
877 (hrel : (zcGroupLike C H h - 1) * y = 0) :
878 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
879 (CompletedGroupAlgebraQuotientInClass H C i.2)
880 (QuotientGroup.mk h) - 1) *
881 zcCompletedGroupAlgebraProjection C H i y = 0 := by
882 have hproj :=
883 congrArg (zcCompletedGroupAlgebraProjection C H i) hrel
884 simpa only [zcCompletedGroupAlgebraProjection_mul,
885 zcCompletedGroupAlgebraProjection_sub,
886 zcCompletedGroupAlgebraProjection_groupLike,
887 zcCompletedGroupAlgebraProjection_one,
888 zcCompletedGroupAlgebraProjection_zero] using hproj
890/-- Integer-power version of finite-stage descent for \((h^n - 1)y = 0\). -/
891theorem zcCompletedGroupAlgebra_projection_zpow_sub_one_mul_eq_zero
892 (C : ProCGroups.FiniteGroupClass.{u})
893 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
894 (h : H) (n : ℤ) (y : ZCCompletedGroupAlgebra C H)
895 (i : ZCCompletedGroupAlgebraIndex C H)
896 (hrel : (zcGroupLike C H (h ^ n) - 1) * y = 0) :
897 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
898 (CompletedGroupAlgebraQuotientInClass H C i.2)
899 ((QuotientGroup.mk h : CompletedGroupAlgebraQuotientInClass H C i.2) ^ n) -
900 1) *
901 zcCompletedGroupAlgebraProjection C H i y = 0 := by
902 have hstage :=
903 zcCompletedGroupAlgebra_projection_sub_one_mul_eq_zero
904 C H (h ^ n) y i hrel
905 rw [QuotientGroup.mk_zpow] at hstage
906 exact hstage
908/--
909A \(\mathbb{Z}_C\llbracket H\rrbracket\) transition with unchanged coefficient modulus is just
910the quotient map on the finite group-algebra domain.
911-/
912theorem zcCompletedGroupAlgebraTransition_sameCoeff
913 (C : ProCGroups.FiniteGroupClass.{u})
914 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
915 (coeff : ProCIntegerIndex C)
916 {U V : OpenNormalSubgroupInClass C H}
917 (hUV : (V.1 : Subgroup H) ≤ (U.1 : Subgroup H)) :
918 zcCompletedGroupAlgebraTransition C H
919 (i := (coeff, OrderDual.toDual U))
920 (j := (coeff, OrderDual.toDual V))
921 (show (coeff, OrderDual.toDual U) ≤ (coeff, OrderDual.toDual V) from
922 ⟨dvd_rfl, hUV⟩) =
923 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff coeff.modulus)
924 (OpenNormalSubgroupInClass.map
925 (C := C) (G := H) (U := U) (V := V) hUV) := by
926 letI : Fact (0 < coeff.modulus) := ⟨coeff.positive⟩
927 apply MonoidAlgebra.ringHom_ext
928 · intro r
929 rw [zcCompletedGroupAlgebraTransition_single]
930 change
931 MonoidAlgebra.single
932 ((OpenNormalSubgroupInClass.map
933 (C := C) (G := H) (U := U) (V := V) hUV) 1)
934 ((modNCompletedCoeffMap (n := coeff.modulus)
935 (m := coeff.modulus) dvd_rfl) r) =
936 MonoidAlgebra.mapDomain
937 (OpenNormalSubgroupInClass.map
938 (C := C) (G := H) (U := U) (V := V) hUV)
939 (MonoidAlgebra.single 1 r)
940 rw [MonoidAlgebra.mapDomain_single]
941 simp only [map_one, modNCompletedCoeffMap, ZMod.castHom_self, RingHom.id_apply]
942 · intro q
943 rw [zcCompletedGroupAlgebraTransition_single]
944 change
945 MonoidAlgebra.single
946 ((OpenNormalSubgroupInClass.map
947 (C := C) (G := H) (U := U) (V := V) hUV) q)
948 ((modNCompletedCoeffMap (n := coeff.modulus)
949 (m := coeff.modulus) dvd_rfl) (1 : ModNCompletedCoeff coeff.modulus)) =
950 MonoidAlgebra.mapDomain
951 (OpenNormalSubgroupInClass.map
952 (C := C) (G := H) (U := U) (V := V) hUV)
953 (MonoidAlgebra.single q (1 : ModNCompletedCoeff coeff.modulus))
954 rw [MonoidAlgebra.mapDomain_single]
955 simp only [modNCompletedCoeffMap, ZMod.castHom_self, RingHom.id_apply]
957/--
958After coefficient change, projection of multiplication by a group-like element is computed in
959the corresponding finite group-algebra stage.
960-/
961@[simp]
962theorem zcCompletedGroupAlgebraProjection_coeffMap_mul_groupLike
963 (C : ProCGroups.FiniteGroupClass.{u})
964 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
965 (i : ZCCompletedGroupAlgebraIndex C H) (a : ZCCoeff C) (h : H) :
966 zcCompletedGroupAlgebraProjection C H i
967 (zcCompletedGroupAlgebraCoeffMap C H a * zcGroupLike C H h) =
968 MonoidAlgebra.single
969 (QuotientGroup.mk h : CompletedGroupAlgebraQuotientInClass H C i.2)
970 (proCIntegerProj (C := C) i.1 a) := by
971 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
972 rw [zcCompletedGroupAlgebraProjection_mul, zcCompletedGroupAlgebraProjection_coeffMap,
973 zcCompletedGroupAlgebraProjection_groupLike]
974 rw [MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, one_mul, mul_one]
975 rfl
977/-- Every finite-stage projection from the pro-\(C\) completed group algebra is surjective. -/
978theorem zcCompletedGroupAlgebraProjection_surjective
979 (C : ProCGroups.FiniteGroupClass.{u})
980 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
981 (i : ZCCompletedGroupAlgebraIndex C H) :
982 Function.Surjective (zcCompletedGroupAlgebraProjection C H i) := by
983 classical
984 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
985 letI : DecidableEq (CompletedGroupAlgebraQuotientInClass H C i.2) := Classical.decEq _
986 intro x
987 induction x using MonoidAlgebra.induction with
988 | zero =>
989 exact ⟨0, by simp only [zcCompletedGroupAlgebraProjection_zero]⟩
990 | @single_add q a x hq hx ih =>
991 rcases ih with ⟨y, hy⟩
992 rcases QuotientGroup.mk'_surjective
993 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup H) : Subgroup H)) q with
994 ⟨h, rfl⟩
995 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
996 let aLift : ZCCoeff C := (t : ProCIntegerLimitCarrier C)
997 refine ⟨zcCompletedGroupAlgebraCoeffMap C H aLift * zcGroupLike C H h + y, ?_⟩
998 rw [zcCompletedGroupAlgebraProjection_add,
999 zcCompletedGroupAlgebraProjection_coeffMap_mul_groupLike, hy]
1000 simp only [proCIntegerProj_intCast, QuotientGroup.mk'_apply, aLift]
1001 rfl
1003section Basic
1005variable (C : ProCGroups.FiniteGroupClass.{v})
1006variable {G : Type u} [Group G]
1007variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
1009/--
1010The completed coefficient homomorphism \(G \to \mathbb{Z}_C\llbracket H\rrbracket\) induced by
1011\(\psi: G \to H\).
1012-/
1013def zcCompletedGroupAlgebraScalar (ψ : G →* H) :
1014 G →* ZCCompletedGroupAlgebra C H :=
1015 (zcGroupLike C H).comp ψ
1017/--
1018The completed group-algebra scalar associated to `g` is the group-like element determined by `ψ g`.
1019-/
1020@[simp]
1021theorem zcCompletedGroupAlgebraScalar_apply (ψ : G →* H) (g : G) :
1022 zcCompletedGroupAlgebraScalar C ψ g = zcGroupLike C H (ψ g) :=
1023 rfl
1025/--
1026If \(g\in\ker \psi\), then the completed coefficient homomorphism induced by \(\psi\) sends
1027\(g\) to the unit element.
1028-/
1029@[simp]
1030theorem zcCompletedGroupAlgebraScalar_subtype_ker (ψ : G →* H) (g : ψ.ker) :
1031 zcCompletedGroupAlgebraScalar C ψ g = 1 := by
1032 rw [zcCompletedGroupAlgebraScalar_apply, g.2, map_one]
1034/--
1035The algebraic universal \(\mathbb{Z}_C\llbracket H\rrbracket\) differential module attached to
1036\(\psi : G \to H\). It is the \(\mathbb{Z}_C\llbracket H\rrbracket\)-module generated by the
1037symbols dg, subject to the Leibniz relations \(d(gh)=dg+\) \([\psi(g)]\) dh, i.e. the quotient
1038by the raw crossed-differential relation submodule. The final profinite Crowell middle term is
1039the separated finite-stage quotient \(\mathbb{Z}_C\)-separated completed differential module,
1040not this algebraic quotient.
1041-/
1042abbrev ZCCompletedDifferentialModule (ψ : G →* H) : Type _ :=
1043 CrossedDifferentialModule (zcCompletedGroupAlgebraScalar C ψ)
1045/-- The universal completed crossed differential, bundled with its Fox--Leibniz law. -/
1046def zcUniversalDifferential (ψ : G →* H) :
1047 ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
1048 (ZCCompletedDifferentialModule C ψ) :=
1049 universalCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
1051/-- The completed Fox boundary \(g \mapsto [\psi(g)] - 1\), bundled with its
1052Fox--Leibniz law. -/
1053def zcCompletedGroupAlgebraBoundary (ψ : G →* H) :
1054 ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
1055 (ZCCompletedGroupAlgebra C H) where
1056 toFun g := zcGroupLike C H (ψ g) - 1
1057 map_mul' g h := by
1058 simp only [scalarCrossedAction_apply, map_mul, sub_eq_add_neg, add_comm,
1059 zcCompletedGroupAlgebraScalar_apply, smul_eq_mul, mul_add, mul_neg,
1060 mul_one, add_assoc, add_neg_cancel_comm_assoc]
1062/-- The completed Fox boundary vanishes on elements in the kernel of the target map. -/
1063@[simp]
1064theorem zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker
1065 (ψ : G →* H) {g : G} (hg : ψ g = 1) :
1066 zcCompletedGroupAlgebraBoundary C ψ g = 0 := by
1067 change zcGroupLike C H (ψ g) - 1 = 0
1068 rw [hg, map_one]
1069 simp only [sub_self]
1071/-- The completed Fox boundary restricted to the kernel subgroup is zero. -/
1072@[simp]
1073theorem zcCompletedGroupAlgebraBoundary_subtype_ker
1074 (ψ : G →* H) (g : ψ.ker) :
1075 zcCompletedGroupAlgebraBoundary C ψ g = 0 :=
1076 zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker (C := C) (ψ := ψ) g.2
1078section UniversalProperty
1080variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
1082/--
1083The universal \(\mathbb{Z}_C\llbracket H\rrbracket\)-linear map from the completed
1084crossed-differential module to the completed group algebra is induced by the completed Fox
1085boundary \(g\mapsto [\psi(g)]-1\).
1086-/
1087def zcToCompletedGroupAlgebra (ψ : G →* H) :
1088 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
1089 ZCCompletedGroupAlgebra C H :=
1090 crossedHomModuleLift (A := ZCCompletedGroupAlgebra C H)
1091 (zcCompletedGroupAlgebraScalar C ψ) (zcCompletedGroupAlgebraBoundary C ψ)
1093/--
1094The universal map to the completed group algebra sends the universal differential of \(g\) to
1095the completed Fox boundary \([\psi(g)]-1\).
1096-/
1097@[simp]
1098theorem zcToCompletedGroupAlgebra_universal (ψ : G →* H) (g : G) :
1099 zcToCompletedGroupAlgebra C ψ (zcUniversalDifferential C ψ g) =
1100 zcCompletedGroupAlgebraBoundary C ψ g :=
1101 crossedHomModuleLift_universal
1102 (A := ZCCompletedGroupAlgebra C H) (zcCompletedGroupAlgebraScalar C ψ)
1103 (zcCompletedGroupAlgebraBoundary C ψ) g
1105/--
1106There is a unique \(\mathbb{Z}_C\llbracket H\rrbracket\)-linear map from the completed
1107crossed-differential module to the completed group algebra that sends every universal
1108differential to the corresponding completed Fox boundary.
1109-/
1110theorem existsUnique_zcToCompletedGroupAlgebra (ψ : G →* H) :
1111 ∃! f :
1112 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
1113 ZCCompletedGroupAlgebra C H,
1114 ∀ g, f (zcUniversalDifferential C ψ g) =
1115 zcCompletedGroupAlgebraBoundary C ψ g :=
1116 existsUnique_crossedHomModuleLift
1117 (A := ZCCompletedGroupAlgebra C H) (zcCompletedGroupAlgebraScalar C ψ)
1118 (zcCompletedGroupAlgebraBoundary C ψ)
1120end UniversalProperty
1122section SourceNaturality
1124variable {G' : Type u} [Group G']
1126/--
1127Source functoriality for the completed universal differential module. For a homomorphism \(f:G
1128\to G'\), the universal crossed differential attached to \(\psi'\circ f\) maps to the one
1129attached to \(\psi'\) by sending \(dg\) to \(d(f(g))\).
1130-/
1131def zcCompletedDifferentialModuleSourceMap
1132 (ψ' : G' →* H) (f : G →* G') :
1133 ZCCompletedDifferentialModule C (ψ'.comp f) →ₗ[ZCCompletedGroupAlgebra C H]
1134 ZCCompletedDifferentialModule C ψ' :=
1135 crossedHomModuleLift (A := ZCCompletedDifferentialModule C ψ')
1136 (zcCompletedGroupAlgebraScalar C (ψ'.comp f))
1137 { toFun := fun g => zcUniversalDifferential C ψ' (f g)
1138 map_mul' := by
1139 intro g h
1140 change zcUniversalDifferential C ψ' (f (g * h)) =
1141 zcUniversalDifferential C ψ' (f g) +
1142 zcCompletedGroupAlgebraScalar C (ψ'.comp f) g •
1143 zcUniversalDifferential C ψ' (f h)
1144 rw [map_mul, ScalarCrossedHom.map_mul (zcUniversalDifferential C ψ')]
1145 rfl }
1147/--
1148The universal source map on the completed differential module is determined by the source
1149quotient maps at finite stages.
1150-/
1151@[simp]
1152theorem zcCompletedDifferentialModuleSourceMap_universal
1153 (ψ' : G' →* H) (f : G →* G') (g : G) :
1154 zcCompletedDifferentialModuleSourceMap (C := C) ψ' f
1155 (zcUniversalDifferential C (ψ'.comp f) g) =
1156 zcUniversalDifferential C ψ' (f g) :=
1157 crossedHomModuleLift_universal
1158 (A := ZCCompletedDifferentialModule C ψ')
1159 (zcCompletedGroupAlgebraScalar C (ψ'.comp f))
1160 { toFun := fun g => zcUniversalDifferential C ψ' (f g)
1161 map_mul' := by
1162 intro g h
1163 change zcUniversalDifferential C ψ' (f (g * h)) =
1164 zcUniversalDifferential C ψ' (f g) +
1165 zcCompletedGroupAlgebraScalar C (ψ'.comp f) g •
1166 zcUniversalDifferential C ψ' (f h)
1167 rw [map_mul, ScalarCrossedHom.map_mul (zcUniversalDifferential C ψ')]
1168 rfl } g
1170/-- Completed universal zero descends along a source homomorphism. -/
1171theorem zcUniversalDifferential_eq_zero_of_source
1172 (ψ' : G' →* H) (f : G →* G') {g : G}
1173 (hg : zcUniversalDifferential C (ψ'.comp f) g = 0) :
1174 zcUniversalDifferential C ψ' (f g) = 0 := by
1175 rw [← zcCompletedDifferentialModuleSourceMap_universal (C := C) ψ' f g, hg, map_zero]
1177end SourceNaturality
1179section UniversalZero
1181variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
1183/--
1184A zero universal differential is killed by every crossed differential represented by the
1185completed universal module.
1186-/
1187theorem crossedDifferential_eq_zero_of_zcUniversalDifferential_eq_zero
1188 (ψ : G →* H)
1189 (D : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
1190 {g : G} (hg : zcUniversalDifferential C ψ g = 0) :
1191 D g = 0 := by
1192 change
1193 universalCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) g = 0 at hg
1194 rw [← crossedHomModuleLift_universal
1195 (A := A) (zcCompletedGroupAlgebraScalar C ψ) D g, hg, map_zero]
1197end UniversalZero
1199end Basic
1201end
1203end FoxDifferential