FoxDifferential/Completed/ProCIntegerCoefficients/Core.lean
1import FoxDifferential.Common.CrossedDifferentialModule
2import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.StageCoeffMap
3import ProCGroups.Completion.ProCInteger
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FoxDifferential/Completed/ProCIntegerCoefficients/Core.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Completed group algebra coefficients
16This module sets up the basic pro-\(C\) integer coefficient rings and scalar actions used in the completed Fox-differential layer.
17-/
18namespace FoxDifferential
20noncomputable section
22open scoped BigOperators
23open ProCGroups.Completion
24open ProCGroups.InverseSystems
25open ProCGroups.ProC
27universe u v
29/-- The pro-`C` integer coefficient ring. -/
33/-- The two-parameter finite stage index for `Z_C[[H]]`: a coefficient quotient of `Z_C` and a
36 (C : ProCGroups.FiniteGroupClass.{u})
37 (H : Type u) [Group H] [TopologicalSpace H] : Type u :=
38 ProCIntegerIndex C × CompletedGroupAlgebraIndexInClass H C
40/-- A finite stage `(Z/nZ)[H/U]` of the pro-`C` completed group algebra. -/
42 (C : ProCGroups.FiniteGroupClass.{u})
43 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
44 (i : ZCCompletedGroupAlgebraIndex C H) : Type u :=
45 ModNCompletedGroupAlgebraStageInClass i.1.modulus H C i.2
47/-- Transition maps for the true pro-`C` completed group algebra. The coefficient direction is
48divisibility of allowed pro-`C` integer moduli, and the group direction is refinement of
49`C`-quotients. -/
51 (C : ProCGroups.FiniteGroupClass.{u})
52 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
53 {i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j) :
54 ZCCompletedGroupAlgebraStage C H j →+* ZCCompletedGroupAlgebraStage C H i := by
55 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
56 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
57 exact
59 (n := i.1.modulus) (m := j.1.modulus) (G := H) C i.2 hij.1).comp
60 (modNCompletedGroupAlgebraTransitionInClass (n := j.1.modulus) (G := H) C hij.2)
62/-- Evaluation of a pro-`C` transition on a group-like basis element. -/
63@[simp]
65 (C : ProCGroups.FiniteGroupClass.{u})
66 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
67 {i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j)
68 (q : CompletedGroupAlgebraQuotientInClass H C j.2) :
69 zcCompletedGroupAlgebraTransition C H hij
70 (MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus) _ q) =
71 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus) _
72 ((OpenNormalSubgroupInClass.map
73 (C := C) (G := H)
74 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q) := by
75 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
76 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
77 rw [zcCompletedGroupAlgebraTransition, RingHom.comp_apply,
79 simpa using
81 (n := i.1.modulus) (m := j.1.modulus) (G := H) C i.2 hij.1
82 ((OpenNormalSubgroupInClass.map
83 (C := C) (G := H)
84 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q))
86/-- Evaluation of a pro-`C` transition on a single coefficient at one quotient element. -/
87@[simp]
89 (C : ProCGroups.FiniteGroupClass.{u})
90 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
91 {i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j)
92 (q : CompletedGroupAlgebraQuotientInClass H C j.2)
93 (a : ModNCompletedCoeff j.1.modulus) :
94 zcCompletedGroupAlgebraTransition C H hij (MonoidAlgebra.single q a) =
95 MonoidAlgebra.single
96 ((OpenNormalSubgroupInClass.map
97 (C := C) (G := H)
98 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)
99 (modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1 a) := by
100 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
101 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
102 rw [zcCompletedGroupAlgebraTransition, RingHom.comp_apply,
106/-- Identity transition for `Z_C[[H]]`. -/
107@[simp]
109 (C : ProCGroups.FiniteGroupClass.{u})
110 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
111 (i : ZCCompletedGroupAlgebraIndex C H) :
112 zcCompletedGroupAlgebraTransition C H (le_rfl : i ≤ i) = RingHom.id _ := by
113 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
117 simp only [RingHomCompTriple.comp_eq]
119/-- Composition of transition maps for `Z_C[[H]]`. -/
120@[simp 900]
122 (C : ProCGroups.FiniteGroupClass.{u})
123 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
124 {i j k : ZCCompletedGroupAlgebraIndex C H}
125 (hij : i ≤ j) (hjk : j ≤ k) :
126 (zcCompletedGroupAlgebraTransition C H hij).comp
127 (zcCompletedGroupAlgebraTransition C H hjk) =
128 zcCompletedGroupAlgebraTransition C H (hij.trans hjk) := by
129 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
130 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
131 letI : Fact (0 < k.1.modulus) := ⟨k.1.positive⟩
132 apply RingHom.ext
133 intro x
134 refine MonoidAlgebra.induction_on
135 (p := fun x =>
136 ((zcCompletedGroupAlgebraTransition C H hij).comp
137 (zcCompletedGroupAlgebraTransition C H hjk)) x =
138 zcCompletedGroupAlgebraTransition C H (hij.trans hjk) x)
139 x ?_ ?_ ?_
140 · intro q
141 rw [RingHom.comp_apply, zcCompletedGroupAlgebraTransition_of C H hjk,
142 zcCompletedGroupAlgebraTransition_of C H (hij.trans hjk)]
143 change
144 zcCompletedGroupAlgebraTransition C H hij
145 (MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
146 (CompletedGroupAlgebraQuotientInClass H C j.2)
147 ((OpenNormalSubgroupInClass.map
148 (C := C) (G := H)
149 (U := OrderDual.ofDual j.2) (V := OrderDual.ofDual k.2) hjk.2) q)) =
150 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
151 (CompletedGroupAlgebraQuotientInClass H C i.2)
152 ((OpenNormalSubgroupInClass.map
153 (C := C) (G := H)
154 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual k.2) (hij.2.trans hjk.2)) q)
155 rw [zcCompletedGroupAlgebraTransition_of C H hij]
156 congr 1
157 exact congrFun
158 (congrArg DFunLike.coe
159 (OpenNormalSubgroupInClass.map_comp
160 (C := C) (G := H)
161 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2)
162 (W := OrderDual.ofDual k.2) hij.2 hjk.2)) q
163 · intro x y hx hy
164 simp only [RingHom.map_add, hx, hy]
165 · intro a x hx
166 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
167 have hcoeff :
168 ((zcCompletedGroupAlgebraTransition C H hij).comp
169 (zcCompletedGroupAlgebraTransition C H hjk))
170 (algebraMap (ModNCompletedCoeff k.1.modulus)
171 (ZCCompletedGroupAlgebraStage C H k) a) =
172 zcCompletedGroupAlgebraTransition C H (hij.trans hjk)
173 (algebraMap (ModNCompletedCoeff k.1.modulus)
174 (ZCCompletedGroupAlgebraStage C H k) a) := by
175 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
177 modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe, modNCompletedGroupAlgebraTransitionInClass, map_intCast]
178 rw [hcoeff]
180/-- The inverse system defining the pro-`C` completed group algebra. -/
182 (C : ProCGroups.FiniteGroupClass.{u})
183 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
184 InverseSystem (I := ZCCompletedGroupAlgebraIndex C H) where
185 X := ZCCompletedGroupAlgebraStage C H
186 topologicalSpace := fun _ => ⊥
187 map := fun {i j} hij => zcCompletedGroupAlgebraTransition C H hij
188 continuous_map := by
189 intro i j hij
190 letI : TopologicalSpace (ZCCompletedGroupAlgebraStage C H i) := ⊥
191 letI : TopologicalSpace (ZCCompletedGroupAlgebraStage C H j) := ⊥
192 letI : DiscreteTopology (ZCCompletedGroupAlgebraStage C H j) := ⟨rfl⟩
193 exact continuous_of_discreteTopology
194 map_id := by
195 intro i
196 funext x
197 exact congrFun
198 (congrArg DFunLike.coe
199 (zcCompletedGroupAlgebraTransition_id C H i)) x
200 map_comp := by
201 intro i j k hij hjk
202 funext x
203 exact congrFun
204 (congrArg DFunLike.coe
205 (zcCompletedGroupAlgebraTransition_comp C H hij hjk)) x
207/-- Compatibility for a family of finite `Z_C[[H]]` stage elements. -/
209 (C : ProCGroups.FiniteGroupClass.{u})
210 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
211 (x : ∀ i : ZCCompletedGroupAlgebraIndex C H, ZCCompletedGroupAlgebraStage C H i) : Prop :=
212 ∀ i j, ∀ hij : i ≤ j, zcCompletedGroupAlgebraTransition C H hij (x j) = x i
214/-- The completed group algebra `Z_C[[H]]`. -/
215abbrev ZCCompletedGroupAlgebra
216 (C : ProCGroups.FiniteGroupClass.{u})
217 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] : Type u :=
218 {x : ∀ i : ZCCompletedGroupAlgebraIndex C H, ZCCompletedGroupAlgebraStage C H i //
221/-- Projection from `Z_C[[H]]` to a finite `C`-coefficient and `C`-quotient stage. -/
223 (C : ProCGroups.FiniteGroupClass.{u})
224 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
225 (i : ZCCompletedGroupAlgebraIndex C H) :
226 ZCCompletedGroupAlgebra C H → ZCCompletedGroupAlgebraStage C H i :=
227 fun x => x.1 i
229section Ring
231variable (C : ProCGroups.FiniteGroupClass.{u})
232variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
234instance instZeroZCCompletedGroupAlgebra : Zero (ZCCompletedGroupAlgebra C H) where
237instance instAddZCCompletedGroupAlgebra : Add (ZCCompletedGroupAlgebra C H) where
239 intro i j hij
241 exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩
243instance instNegZCCompletedGroupAlgebra : Neg (ZCCompletedGroupAlgebra C H) where
245 intro i j hij
246 rw [map_neg]
247 exact congrArg Neg.neg (x.2 i j hij)⟩
249instance instSubZCCompletedGroupAlgebra : Sub (ZCCompletedGroupAlgebra C H) where
251 intro i j hij
252 rw [map_sub]
253 exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩
255instance instSMulNatZCCompletedGroupAlgebra : SMul ℕ (ZCCompletedGroupAlgebra C H) where
256 smul n x := ⟨fun i => n • x.1 i, by
257 intro i j hij
258 rw [map_nsmul]
259 exact congrArg (n • ·) (x.2 i j hij)⟩
261instance instSMulIntZCCompletedGroupAlgebra : SMul ℤ (ZCCompletedGroupAlgebra C H) where
262 smul n x := ⟨fun i => n • x.1 i, by
263 intro i j hij
264 rw [map_zsmul]
265 exact congrArg (n • ·) (x.2 i j hij)⟩
267@[simp]
268theorem coe_zero_zcCompletedGroupAlgebra :
269 ((0 : ZCCompletedGroupAlgebra C H) :
270 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = 0 := by
271 funext i
272 rfl
274@[simp]
275theorem coe_add_zcCompletedGroupAlgebra (x y : ZCCompletedGroupAlgebra C H) :
276 ((x + y : ZCCompletedGroupAlgebra C H) :
277 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = x + y := by
278 funext i
279 rfl
281@[simp]
282theorem coe_neg_zcCompletedGroupAlgebra (x : ZCCompletedGroupAlgebra C H) :
283 ((-x : ZCCompletedGroupAlgebra C H) :
284 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = -x := by
285 funext i
286 rfl
288@[simp]
289theorem coe_sub_zcCompletedGroupAlgebra (x y : ZCCompletedGroupAlgebra C H) :
290 ((x - y : ZCCompletedGroupAlgebra C H) :
291 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = x - y := by
292 funext i
293 rfl
295@[simp]
296theorem coe_nsmul_zcCompletedGroupAlgebra (n : ℕ) (x : ZCCompletedGroupAlgebra C H) :
297 ((n • x : ZCCompletedGroupAlgebra C H) :
298 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = n • x := by
299 funext i
300 rfl
302@[simp]
303theorem coe_zsmul_zcCompletedGroupAlgebra (n : ℤ) (x : ZCCompletedGroupAlgebra C H) :
304 ((n • x : ZCCompletedGroupAlgebra C H) :
305 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = n • x := by
306 funext i
307 rfl
309instance instAddCommGroupZCCompletedGroupAlgebra : AddCommGroup (ZCCompletedGroupAlgebra C H) :=
310 Function.Injective.addCommGroup
311 (fun x : ZCCompletedGroupAlgebra C H =>
312 (x : (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i))
313 Subtype.val_injective
314 (coe_zero_zcCompletedGroupAlgebra (C := C) (H := H))
315 (coe_add_zcCompletedGroupAlgebra (C := C) (H := H))
316 (coe_neg_zcCompletedGroupAlgebra (C := C) (H := H))
317 (coe_sub_zcCompletedGroupAlgebra (C := C) (H := H))
318 (fun x n => coe_nsmul_zcCompletedGroupAlgebra (C := C) (H := H) n x)
319 (fun x n => coe_zsmul_zcCompletedGroupAlgebra (C := C) (H := H) n x)
321instance instOneZCCompletedGroupAlgebra : One (ZCCompletedGroupAlgebra C H) where
324instance instMulZCCompletedGroupAlgebra : Mul (ZCCompletedGroupAlgebra C H) where
325 mul x y := ⟨fun i => x.1 i * y.1 i, by
326 intro i j hij
328 exact congrArg₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩
330instance instNatCastZCCompletedGroupAlgebra : NatCast (ZCCompletedGroupAlgebra C H) where
331 natCast n := ⟨fun i => n, by intro i j hij; exact map_natCast _ _⟩
333instance instIntCastZCCompletedGroupAlgebra : IntCast (ZCCompletedGroupAlgebra C H) where
334 intCast n := ⟨fun i => n, by intro i j hij; exact map_intCast _ _⟩
336instance instPowZCCompletedGroupAlgebra : Pow (ZCCompletedGroupAlgebra C H) ℕ where
337 pow x n := ⟨fun i => x.1 i ^ n, by
338 intro i j hij
339 rw [map_pow]
340 exact congrArg (fun z => z ^ n) (x.2 i j hij)⟩
342@[simp]
343theorem coe_one_zcCompletedGroupAlgebra :
344 ((1 : ZCCompletedGroupAlgebra C H) :
345 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = 1 := by
346 funext i
347 rfl
349@[simp]
350theorem coe_mul_zcCompletedGroupAlgebra (x y : ZCCompletedGroupAlgebra C H) :
351 ((x * y : ZCCompletedGroupAlgebra C H) :
352 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = x * y := by
353 funext i
354 rfl
356@[simp]
357theorem coe_natCast_zcCompletedGroupAlgebra (n : ℕ) :
358 ((n : ZCCompletedGroupAlgebra C H) :
359 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = n := by
360 funext i
361 rfl
363@[simp]
364theorem coe_intCast_zcCompletedGroupAlgebra (n : ℤ) :
365 ((n : ZCCompletedGroupAlgebra C H) :
366 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = n := by
367 funext i
368 rfl
370@[simp]
371theorem coe_pow_zcCompletedGroupAlgebra (x : ZCCompletedGroupAlgebra C H) (n : ℕ) :
372 ((x ^ n : ZCCompletedGroupAlgebra C H) :
373 (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i) = x ^ n := by
374 funext i
375 rfl
377instance instRingZCCompletedGroupAlgebra : Ring (ZCCompletedGroupAlgebra C H) :=
378 Function.Injective.ring
379 (fun x : ZCCompletedGroupAlgebra C H =>
380 (x : (i : ZCCompletedGroupAlgebraIndex C H) → ZCCompletedGroupAlgebraStage C H i))
381 Subtype.val_injective
382 (coe_zero_zcCompletedGroupAlgebra (C := C) (H := H))
383 (coe_one_zcCompletedGroupAlgebra (C := C) (H := H))
384 (coe_add_zcCompletedGroupAlgebra (C := C) (H := H))
385 (coe_mul_zcCompletedGroupAlgebra (C := C) (H := H))
386 (coe_neg_zcCompletedGroupAlgebra (C := C) (H := H))
387 (coe_sub_zcCompletedGroupAlgebra (C := C) (H := H))
388 (fun n x => coe_nsmul_zcCompletedGroupAlgebra (C := C) (H := H) n x)
389 (fun n x => coe_zsmul_zcCompletedGroupAlgebra (C := C) (H := H) n x)
390 (fun x n => coe_pow_zcCompletedGroupAlgebra (C := C) (H := H) x n)
391 (by intro n; exact coe_natCast_zcCompletedGroupAlgebra (C := C) (H := H) n)
392 (by intro z; exact coe_intCast_zcCompletedGroupAlgebra (C := C) (H := H) z)
394@[simp]
396 (i : ZCCompletedGroupAlgebraIndex C H) :
397 zcCompletedGroupAlgebraProjection C H i (1 : ZCCompletedGroupAlgebra C H) = 1 :=
398 rfl
400@[simp]
402 (i : ZCCompletedGroupAlgebraIndex C H) (x y : ZCCompletedGroupAlgebra C H) :
403 zcCompletedGroupAlgebraProjection C H i (x * y) =
404 zcCompletedGroupAlgebraProjection C H i x *
405 zcCompletedGroupAlgebraProjection C H i y :=
406 rfl
408@[simp]
410 (i : ZCCompletedGroupAlgebraIndex C H) :
411 zcCompletedGroupAlgebraProjection C H i (0 : ZCCompletedGroupAlgebra C H) = 0 :=
412 rfl
414@[simp]
416 (i : ZCCompletedGroupAlgebraIndex C H) (x y : ZCCompletedGroupAlgebra C H) :
417 zcCompletedGroupAlgebraProjection C H i (x + y) =
418 zcCompletedGroupAlgebraProjection C H i x +
419 zcCompletedGroupAlgebraProjection C H i y :=
420 rfl
422@[simp]
424 (i : ZCCompletedGroupAlgebraIndex C H) (x : ZCCompletedGroupAlgebra C H) :
425 zcCompletedGroupAlgebraProjection C H i (-x) =
426 -zcCompletedGroupAlgebraProjection C H i x :=
427 rfl
429@[simp]
431 (i : ZCCompletedGroupAlgebraIndex C H) (x y : ZCCompletedGroupAlgebra C H) :
432 zcCompletedGroupAlgebraProjection C H i (x - y) =
433 zcCompletedGroupAlgebraProjection C H i x -
434 zcCompletedGroupAlgebraProjection C H i y :=
435 rfl
437/-- Projection from `Z_C[[H]]` to a finite stage as a ring homomorphism. -/
439 (i : ZCCompletedGroupAlgebraIndex C H) :
440 ZCCompletedGroupAlgebra C H →+* ZCCompletedGroupAlgebraStage C H i where
441 toFun := zcCompletedGroupAlgebraProjection C H i
442 map_zero' := zcCompletedGroupAlgebraProjection_zero C H i
443 map_one' := zcCompletedGroupAlgebraProjection_one C H i
444 map_add' := zcCompletedGroupAlgebraProjection_add C H i
445 map_mul' := zcCompletedGroupAlgebraProjection_mul C H i
447@[simp]
449 (i : ZCCompletedGroupAlgebraIndex C H) (x : ZCCompletedGroupAlgebra C H) :
450 zcCompletedGroupAlgebraProjectionRingHom C H i x =
451 zcCompletedGroupAlgebraProjection C H i x :=
452 rfl
454/-- A finite stage of `Z_C[[H]]` is a module over `Z_C[[H]]` by restriction of scalars
455along its projection. -/
457 (i : ZCCompletedGroupAlgebraIndex C H) :
458 Module (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebraStage C H i) :=
459 Module.compHom _ (zcCompletedGroupAlgebraProjectionRingHom C H i)
461/-- Finite stage projections separate points of `Z_C[[H]]`. -/
463 {x y : ZCCompletedGroupAlgebra C H}
464 (h : ∀ i : ZCCompletedGroupAlgebraIndex C H,
465 zcCompletedGroupAlgebraProjection C H i x =
466 zcCompletedGroupAlgebraProjection C H i y) :
467 x = y := by
468 apply Subtype.ext
469 funext i
470 exact h i
472/-- Finite projections from `Z_C[[H]]` commute with the finite transition maps. -/
473@[simp]
475 {i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j)
476 (x : ZCCompletedGroupAlgebra C H) :
477 zcCompletedGroupAlgebraTransition C H hij
478 (zcCompletedGroupAlgebraProjection C H j x) =
479 zcCompletedGroupAlgebraProjection C H i x :=
480 x.2 i j hij
482/-- A finite stage projection as a linear map over the completed group algebra. -/
484 (i : ZCCompletedGroupAlgebraIndex C H) :
485 ZCCompletedGroupAlgebra C H →ₗ[ZCCompletedGroupAlgebra C H]
486 ZCCompletedGroupAlgebraStage C H i where
487 toFun := zcCompletedGroupAlgebraProjection C H i
488 map_add' x y := zcCompletedGroupAlgebraProjection_add C H i x y
489 map_smul' r x := by
490 change zcCompletedGroupAlgebraProjection C H i (r * x) =
491 zcCompletedGroupAlgebraProjection C H i r *
492 zcCompletedGroupAlgebraProjection C H i x
493 exact zcCompletedGroupAlgebraProjection_mul C H i r x
495@[simp]
497 (i : ZCCompletedGroupAlgebraIndex C H) (x : ZCCompletedGroupAlgebra C H) :
499 zcCompletedGroupAlgebraProjection C H i x :=
500 rfl
502end Ring
504/-- Projection from `Z_C[[H]]` to a finite stage commutes with finite sums. -/
506 (C : ProCGroups.FiniteGroupClass.{u})
507 {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
508 {I : Type v} [Fintype I]
509 (j : ZCCompletedGroupAlgebraIndex C H)
510 (f : I → ZCCompletedGroupAlgebra C H) :
511 zcCompletedGroupAlgebraProjection C H j (∑ i : I, f i) =
512 ∑ i : I, zcCompletedGroupAlgebraProjection C H j (f i) := by
513 classical
514 refine Finset.induction_on (s := Finset.univ) ?_ ?_
515 · rfl
516 · intro a s has ih
517 rw [Finset.sum_insert has, Finset.sum_insert has]
518 rw [zcCompletedGroupAlgebraProjection_add, ih]
520/-- The coefficient element of `Z_C[[H]]` supported at the identity of `H`. -/
522 (C : ProCGroups.FiniteGroupClass.{u})
523 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
524 (a : ZCCoeff C) : ZCCompletedGroupAlgebra C H :=
525 ⟨fun i =>
526 MonoidAlgebra.single
527 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
528 (proCIntegerProj (C := C) i.1 a), by
529 intro i j hij
530 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
531 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
532 change zcCompletedGroupAlgebraTransition C H hij
533 (MonoidAlgebra.single
534 (1 : CompletedGroupAlgebraQuotientInClass H C j.2)
535 (proCIntegerProj (C := C) j.1 a)) =
536 MonoidAlgebra.single
537 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
538 (proCIntegerProj (C := C) i.1 a)
540 have ha : modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1
541 (proCIntegerProj (C := C) j.1 a) =
542 proCIntegerProj (C := C) i.1 a :=
543 proCIntegerProj_transition (C := C) hij.1 a
544 simpa using congrArg
545 (fun b : ProCIntegerStage C i.1 =>
546 MonoidAlgebra.single
547 (1 : CompletedGroupAlgebraQuotientInClass H C i.2) b)
548 ha⟩
550/-- The coefficient embedding `Z_C -> Z_C[[H]]`. -/
552 (C : ProCGroups.FiniteGroupClass.{u})
553 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
554 ZCCoeff C →+* ZCCompletedGroupAlgebra C H where
555 toFun := zcCompletedGroupAlgebraCoeff C H
556 map_zero' := by
557 apply Subtype.ext
558 funext i
559 simp only [zcCompletedGroupAlgebraCoeff, proCIntegerProj_zero, Finsupp.single_zero,
561 map_one' := by
562 apply Subtype.ext
563 funext i
564 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
565 simp only [zcCompletedGroupAlgebraCoeff, proCIntegerProj_one, zcCompletedGroupAlgebraProjection_one,
566 MonoidAlgebra.one_def]
567 map_add' a b := by
568 apply Subtype.ext
569 funext i
570 simp only [zcCompletedGroupAlgebraCoeff, proCIntegerProj_add, Finsupp.single_add,
572 map_mul' a b := by
573 apply Subtype.ext
574 funext i
575 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
576 change MonoidAlgebra.single
577 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
578 (proCIntegerProj (C := C) i.1 (a * b)) =
579 MonoidAlgebra.single
580 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
581 (proCIntegerProj (C := C) i.1 a) *
582 MonoidAlgebra.single
583 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
584 (proCIntegerProj (C := C) i.1 b)
585 simp only [proCIntegerProj_mul, MonoidAlgebra.single_mul_single, mul_one]
587@[simp]
589 (C : ProCGroups.FiniteGroupClass.{u})
590 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
591 (i : ZCCompletedGroupAlgebraIndex C H) (a : ZCCoeff C) :
593 (zcCompletedGroupAlgebraCoeffMap C H a) =
594 MonoidAlgebra.single
595 (1 : CompletedGroupAlgebraQuotientInClass H C i.2)
596 (proCIntegerProj (C := C) i.1 a) :=
597 rfl
599/-- The group-like map `H -> Z_C[[H]]`. -/
600def zcGroupLike
601 (C : ProCGroups.FiniteGroupClass.{u})
602 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
603 H →* ZCCompletedGroupAlgebra C H where
604 toFun h := ⟨fun i =>
605 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
606 (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h), by
607 intro i j hij
608 change
609 zcCompletedGroupAlgebraTransition C H hij
610 (MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
611 (CompletedGroupAlgebraQuotientInClass H C j.2) (QuotientGroup.mk h)) =
612 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
613 (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h)
614 rw [zcCompletedGroupAlgebraTransition_of C H hij]
615 rfl⟩
616 map_one' := by
617 apply Subtype.ext
618 funext i
619 simp only [MonoidAlgebra.of, MonoidAlgebra.single, QuotientGroup.mk_one, MonoidHom.coe_mk, OneHom.coe_mk,
620 zcCompletedGroupAlgebraProjection_one, MonoidAlgebra.one_def]
621 map_mul' h₁ h₂ := by
622 apply Subtype.ext
623 funext i
624 change
625 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
626 (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk (h₁ * h₂)) =
627 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
628 (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h₁) *
629 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
630 (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h₂)
631 simp only [MonoidAlgebra.of, QuotientGroup.mk_mul, MonoidHom.coe_mk, OneHom.coe_mk,
632 MonoidAlgebra.single_mul_single, mul_one]
634/-- Projection formula for a group-like element of `Z_C[[H]]`. -/
635@[simp]
637 (C : ProCGroups.FiniteGroupClass.{u})
638 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
639 (i : ZCCompletedGroupAlgebraIndex C H) (h : H) :
640 zcCompletedGroupAlgebraProjection C H i (zcGroupLike C H h) =
641 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
642 (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h) :=
643 rfl
645@[simp]
647 (C : ProCGroups.FiniteGroupClass.{u})
648 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
649 (i : ZCCompletedGroupAlgebraIndex C H) (h : H) :
650 zcCompletedGroupAlgebraProjectionRingHom C H i (zcGroupLike C H h) =
651 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
652 (CompletedGroupAlgebraQuotientInClass H C i.2) (QuotientGroup.mk h) :=
655/-- A completed group-algebra relation `(h - 1)y = 0` descends to every finite stage. -/
657 (C : ProCGroups.FiniteGroupClass.{u})
658 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
659 (h : H) (y : ZCCompletedGroupAlgebra C H)
660 (i : ZCCompletedGroupAlgebraIndex C H)
661 (hrel : (zcGroupLike C H h - 1) * y = 0) :
662 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
663 (CompletedGroupAlgebraQuotientInClass H C i.2)
664 (QuotientGroup.mk h) - 1) *
665 zcCompletedGroupAlgebraProjection C H i y = 0 := by
666 have hproj :=
667 congrArg (zcCompletedGroupAlgebraProjection C H i) hrel
668 simpa only [zcCompletedGroupAlgebraProjection_mul,
672 zcCompletedGroupAlgebraProjection_zero] using hproj
674/-- Integer-power version of finite-stage descent for `(h^n - 1)y = 0`. -/
676 (C : ProCGroups.FiniteGroupClass.{u})
677 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
678 (h : H) (n : ℤ) (y : ZCCompletedGroupAlgebra C H)
679 (i : ZCCompletedGroupAlgebraIndex C H)
680 (hrel : (zcGroupLike C H (h ^ n) - 1) * y = 0) :
681 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
682 (CompletedGroupAlgebraQuotientInClass H C i.2)
683 ((QuotientGroup.mk h : CompletedGroupAlgebraQuotientInClass H C i.2) ^ n) -
684 1) *
685 zcCompletedGroupAlgebraProjection C H i y = 0 := by
686 have hstage :=
688 C H (h ^ n) y i hrel
689 simpa only [map_zpow] using hstage
691/-- A `Z_C[[H]]` transition with unchanged coefficient modulus is just the quotient
694 (C : ProCGroups.FiniteGroupClass.{u})
695 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
696 (coeff : ProCIntegerIndex C)
697 {U V : OpenNormalSubgroupInClass C H}
698 (hUV : (V.1 : Subgroup H) ≤ (U.1 : Subgroup H)) :
700 (i := (coeff, OrderDual.toDual U))
701 (j := (coeff, OrderDual.toDual V))
702 (show (coeff, OrderDual.toDual U) ≤ (coeff, OrderDual.toDual V) from
703 ⟨dvd_rfl, hUV⟩) =
704 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff coeff.modulus)
705 (OpenNormalSubgroupInClass.map
706 (C := C) (G := H) (U := U) (V := V) hUV) := by
707 letI : Fact (0 < coeff.modulus) := ⟨coeff.positive⟩
708 apply MonoidAlgebra.ringHom_ext
709 · intro r
711 change
712 MonoidAlgebra.single
713 ((OpenNormalSubgroupInClass.map
714 (C := C) (G := H) (U := U) (V := V) hUV) 1)
715 ((modNCompletedCoeffMap (n := coeff.modulus)
716 (m := coeff.modulus) dvd_rfl) r) =
717 MonoidAlgebra.mapDomain
718 (OpenNormalSubgroupInClass.map
719 (C := C) (G := H) (U := U) (V := V) hUV)
720 (MonoidAlgebra.single 1 r)
721 rw [MonoidAlgebra.mapDomain_single]
722 simp only [map_one, modNCompletedCoeffMap, ZMod.castHom_self, RingHom.id_apply]
723 · intro q
725 change
726 MonoidAlgebra.single
727 ((OpenNormalSubgroupInClass.map
728 (C := C) (G := H) (U := U) (V := V) hUV) q)
729 ((modNCompletedCoeffMap (n := coeff.modulus)
730 (m := coeff.modulus) dvd_rfl) (1 : ModNCompletedCoeff coeff.modulus)) =
731 MonoidAlgebra.mapDomain
732 (OpenNormalSubgroupInClass.map
733 (C := C) (G := H) (U := U) (V := V) hUV)
734 (MonoidAlgebra.single q (1 : ModNCompletedCoeff coeff.modulus))
735 rw [MonoidAlgebra.mapDomain_single]
736 simp only [modNCompletedCoeffMap, ZMod.castHom_self, RingHom.id_apply]
738@[simp]
740 (C : ProCGroups.FiniteGroupClass.{u})
741 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
742 (i : ZCCompletedGroupAlgebraIndex C H) (a : ZCCoeff C) (h : H) :
744 (zcCompletedGroupAlgebraCoeffMap C H a * zcGroupLike C H h) =
745 MonoidAlgebra.single
746 (QuotientGroup.mk h : CompletedGroupAlgebraQuotientInClass H C i.2)
747 (proCIntegerProj (C := C) i.1 a) := by
748 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
751 simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.single_mul_single, one_mul,
752 mul_one]
754/-- Every finite-stage projection from the pro-`C` completed group algebra is surjective. -/
756 (C : ProCGroups.FiniteGroupClass.{u})
757 (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
758 (i : ZCCompletedGroupAlgebraIndex C H) :
759 Function.Surjective (zcCompletedGroupAlgebraProjection C H i) := by
760 classical
761 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
762 letI : DecidableEq (CompletedGroupAlgebraQuotientInClass H C i.2) := Classical.decEq _
763 intro x
764 induction x using Finsupp.induction with
766 exact ⟨0, by simp only [zcCompletedGroupAlgebraProjection_zero]⟩
767 | @single_add q a x hq hx ih =>
768 rcases ih with ⟨y, hy⟩
769 rcases QuotientGroup.mk'_surjective
770 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup H) : Subgroup H)) q with
771 ⟨h, rfl⟩
772 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
773 let aLift : ZCCoeff C := (t : ProCIntegerLimitCarrier C)
774 refine ⟨zcCompletedGroupAlgebraCoeffMap C H aLift * zcGroupLike C H h + y, ?_⟩
777 simp only [proCIntegerProj_intCast, QuotientGroup.mk'_apply, aLift]
779section Basic
781variable (C : ProCGroups.FiniteGroupClass.{v})
782variable {G : Type u} [Group G]
783variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
785/-- The completed coefficient homomorphism `G -> Z_C[[H]]` induced by `ψ : G ->* H`. -/
786def zcCompletedGroupAlgebraScalar (ψ : G →* H) :
787 G →* ZCCompletedGroupAlgebra C H :=
788 (zcGroupLike C H).comp ψ
790@[simp]
791theorem zcCompletedGroupAlgebraScalar_apply (ψ : G →* H) (g : G) :
792 zcCompletedGroupAlgebraScalar C ψ g = zcGroupLike C H (ψ g) :=
793 rfl
795@[simp]
796theorem zcCompletedGroupAlgebraScalar_subtype_ker (ψ : G →* H) (g : ψ.ker) :
797 zcCompletedGroupAlgebraScalar C ψ g = 1 := by
798 rw [zcCompletedGroupAlgebraScalar_apply, g.2, map_one]
800/-- The algebraic universal `Z_C[[H]]` differential module attached to `ψ : G ->* H`.
802It is the `Z_C[[H]]`-module generated by the symbols `dg`, subject to the Leibniz relations
803`d(g * h) = dg + [ψ g] dh`, i.e. the quotient by the raw crossed-differential relation
805`ZCSeparatedCompletedDifferentialModule`, not this algebraic quotient. -/
806abbrev ZCCompletedDifferentialModule (ψ : G →* H) : Type _ :=
809/-- The universal completed crossed differential. -/
810def zcUniversalDifferential (ψ : G →* H) (g : G) :
811 ZCCompletedDifferentialModule C ψ :=
814theorem zcUniversalDifferential_mul (ψ : G →* H) (g₁ g₂ : G) :
815 zcUniversalDifferential C ψ (g₁ * g₂) =
816 zcUniversalDifferential C ψ g₁ +
817 zcCompletedGroupAlgebraScalar C ψ g₁ • zcUniversalDifferential C ψ g₂ :=
820@[simp]
821theorem zcUniversalDifferential_one (ψ : G →* H) :
822 zcUniversalDifferential C ψ (1 : G) = 0 :=
825theorem zcUniversalDifferential_isCrossedDifferential (ψ : G →* H) :
827 (zcCompletedGroupAlgebraScalar C ψ) (zcUniversalDifferential C ψ) :=
830section KernelRestriction
832variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
834/-- A completed `Z_C[[H]]` crossed differential restricts to an ordinary additive homomorphism
837 (ψ : G →* H) (delta : G → A)
838 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta) :
839 Additive ψ.ker →+ A :=
840 IsCrossedDifferential.restrictTrivialSubgroupAddMonoidHom hdelta ψ.ker
841 (zcCompletedGroupAlgebraScalar_subtype_ker (C := C) (ψ := ψ))
843@[simp]
845 (ψ : G →* H) (delta : G → A)
846 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
847 (g : ψ.ker) :
848 zcCrossedDifferentialKernelAddMonoidHom C ψ delta hdelta (Additive.ofMul g) = delta g :=
849 rfl
851end KernelRestriction
853/-- The completed Fox boundary `g ↦ [ψ g] - 1` in `Z_C[[H]]`. -/
854def zcCompletedGroupAlgebraBoundary (ψ : G →* H) (g : G) :
855 ZCCompletedGroupAlgebra C H :=
856 zcGroupLike C H (ψ g) - 1
858@[simp]
859theorem zcCompletedGroupAlgebraBoundary_one (ψ : G →* H) :
860 zcCompletedGroupAlgebraBoundary C ψ (1 : G) = 0 := by
861 simp only [zcCompletedGroupAlgebraBoundary, map_one, sub_self]
863/-- The completed Fox boundary vanishes on elements in the kernel of the target map. -/
864@[simp]
866 (ψ : G →* H) {g : G} (hg : ψ g = 1) :
867 zcCompletedGroupAlgebraBoundary C ψ g = 0 := by
868 rw [zcCompletedGroupAlgebraBoundary, hg, map_one]
869 simp only [sub_self]
871/-- The completed Fox boundary restricted to the kernel subgroup is zero. -/
872@[simp]
874 (ψ : G →* H) (g : ψ.ker) :
875 zcCompletedGroupAlgebraBoundary C ψ g = 0 :=
876 zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker (C := C) (ψ := ψ) g.2
878theorem zcCompletedGroupAlgebraBoundary_isCrossedDifferential (ψ : G →* H) :
880 (zcCompletedGroupAlgebraScalar C ψ) (zcCompletedGroupAlgebraBoundary C ψ) := by
881 intro g h
882 simp only [zcCompletedGroupAlgebraBoundary, map_mul, sub_eq_add_neg, add_comm,
883 zcCompletedGroupAlgebraScalar_apply, smul_eq_mul, mul_add, mul_neg, mul_one, add_assoc, add_neg_cancel_comm_assoc]
885theorem zcCompletedGroupAlgebraBoundary_mul (ψ : G →* H) (g₁ g₂ : G) :
886 zcCompletedGroupAlgebraBoundary C ψ (g₁ * g₂) =
887 zcCompletedGroupAlgebraBoundary C ψ g₁ +
888 zcCompletedGroupAlgebraScalar C ψ g₁ •
889 zcCompletedGroupAlgebraBoundary C ψ g₂ :=
892theorem zcCompletedGroupAlgebraBoundary_inv (ψ : G →* H) (g : G) :
893 zcCompletedGroupAlgebraBoundary C ψ g⁻¹ =
894 -(zcCompletedGroupAlgebraScalar C ψ g⁻¹ •
895 zcCompletedGroupAlgebraBoundary C ψ g) :=
896 IsCrossedDifferential.inv
899theorem zcCompletedGroupAlgebraBoundary_pow (ψ : G →* H) (g : G) (m : ℕ) :
900 zcCompletedGroupAlgebraBoundary C ψ (g ^ m) =
901 (Finset.range m).sum
902 (fun k => zcCompletedGroupAlgebraScalar C ψ (g ^ k) •
903 zcCompletedGroupAlgebraBoundary C ψ g) :=
904 IsCrossedDifferential.pow
907section UniversalProperty
909variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
912 (ψ : G →* H) (delta : G → A)
913 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta) :
914 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A :=
915 crossedDifferentialModuleLift (A := A) (zcCompletedGroupAlgebraScalar C ψ) delta hdelta
917@[simp]
919 (ψ : G →* H) (delta : G → A)
920 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta) (g : G) :
921 zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta
922 (zcUniversalDifferential C ψ g) =
923 delta g :=
925 (A := A) (zcCompletedGroupAlgebraScalar C ψ) delta hdelta g
927@[ext]
929 (ψ : G →* H)
930 {f h : ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A}
931 (hfh : ∀ g, f (zcUniversalDifferential C ψ g) =
932 h (zcUniversalDifferential C ψ g)) :
933 f = h :=
934 crossedDifferentialModuleHom_ext (A := A) (zcCompletedGroupAlgebraScalar C ψ) hfh
937 (ψ : G →* H) (delta : G → A)
938 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
939 (f : ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A)
940 (hf : ∀ g, f (zcUniversalDifferential C ψ g) = delta g) :
941 f = zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta :=
943 (A := A) (zcCompletedGroupAlgebraScalar C ψ) delta hdelta f hf
946 (ψ : G →* H) (delta : G → A)
947 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta) :
948 ∃! f : ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A,
949 ∀ g, f (zcUniversalDifferential C ψ g) = delta g :=
951 (A := A) (zcCompletedGroupAlgebraScalar C ψ) delta hdelta
953def zcCompletedCrossedDifferentialEquivLinearMap (ψ : G →* H) :
954 {delta : G → A // IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta} ≃
955 (ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H] A) :=
958def zcToCompletedGroupAlgebra (ψ : G →* H) :
959 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
960 ZCCompletedGroupAlgebra C H :=
961 zcCompletedDifferentialModuleLift (A := ZCCompletedGroupAlgebra C H) C ψ
965@[simp]
966theorem zcToCompletedGroupAlgebra_universal (ψ : G →* H) (g : G) :
967 zcToCompletedGroupAlgebra C ψ (zcUniversalDifferential C ψ g) =
968 zcCompletedGroupAlgebraBoundary C ψ g :=
970 (A := ZCCompletedGroupAlgebra C H) C ψ
974theorem existsUnique_zcToCompletedGroupAlgebra (ψ : G →* H) :
975 ∃! f :
976 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
978 ∀ g, f (zcUniversalDifferential C ψ g) =
979 zcCompletedGroupAlgebraBoundary C ψ g :=
981 (A := ZCCompletedGroupAlgebra C H) C ψ
985end UniversalProperty
987section SourceNaturality
989variable {G' : Type u} [Group G']
991/-- Source functoriality of the completed universal differential module.
993For `f : G -> G'`, the universal crossed differential for `ψ' ∘ f` maps to the universal crossed
994differential for `ψ'` by sending `d g` to `d (f g)`. -/
996 (ψ' : G' →* H) (f : G →* G') :
997 ZCCompletedDifferentialModule C (ψ'.comp f) →ₗ[ZCCompletedGroupAlgebra C H]
998 ZCCompletedDifferentialModule C ψ' :=
1000 C (ψ'.comp f) (fun g => zcUniversalDifferential C ψ' (f g)) (by
1001 intro g h
1002 change zcUniversalDifferential C ψ' (f (g * h)) =
1003 zcUniversalDifferential C ψ' (f g) +
1004 zcCompletedGroupAlgebraScalar C (ψ'.comp f) g •
1005 zcUniversalDifferential C ψ' (f h)
1007 rfl)
1009@[simp]
1011 (ψ' : G' →* H) (f : G →* G') (g : G) :
1012 zcCompletedDifferentialModuleSourceMap (C := C) ψ' f
1013 (zcUniversalDifferential C (ψ'.comp f) g) =
1014 zcUniversalDifferential C ψ' (f g) :=
1016 (A := ZCCompletedDifferentialModule C ψ') C (ψ'.comp f)
1017 (fun g => zcUniversalDifferential C ψ' (f g))
1018 (by
1019 intro g h
1020 change zcUniversalDifferential C ψ' (f (g * h)) =
1021 zcUniversalDifferential C ψ' (f g) +
1022 zcCompletedGroupAlgebraScalar C (ψ'.comp f) g •
1023 zcUniversalDifferential C ψ' (f h)
1025 rfl)
1026 g
1028/-- Completed universal zero descends along a source homomorphism. -/
1030 (ψ' : G' →* H) (f : G →* G') {g : G}
1031 (hg : zcUniversalDifferential C (ψ'.comp f) g = 0) :
1032 zcUniversalDifferential C ψ' (f g) = 0 := by
1033 rw [← zcCompletedDifferentialModuleSourceMap_universal (C := C) ψ' f g, hg, map_zero]
1035end SourceNaturality
1037section UniversalZero
1039variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
1041/-- A zero universal differential is killed by every crossed differential represented by the
1042completed universal module. -/
1044 (ψ : G →* H) (D : G → A)
1045 (hD : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) D)
1046 {g : G} (hg : zcUniversalDifferential C ψ g = 0) :
1047 D g = 0 := by
1048 rw [← zcCompletedDifferentialModuleLift_universal (A := A) C ψ D hD g, hg, map_zero]
1050end UniversalZero
1052end Basic
1054end
1056end FoxDifferential