Yamaguchi Lean 4 Library
FoxDifferential/Completed/ProCIntegerCoefficients/Naturality.lean
FoxDifferential/Completed/ProCIntegerCoefficients/Naturality/Source

FoxDifferential/Completed/ProCIntegerCoefficients/Naturality.lean

1import FoxDifferential.Completed.ProCIntegerCoefficients.Augmentation
2import FoxDifferential.Completed.ProCIntegerCoefficients.Core
3import FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Fundamental
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FoxDifferential/Completed/ProCIntegerCoefficients/Naturality.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 records naturality of pro-\(C\) integer coefficient maps for completed Fox differentials and completed group-algebra morphisms.
17-/
18namespace FoxDifferential
20noncomputable section
22open scoped BigOperators
23open ProCGroups.ProC
25universe u v
27section CompletedGroupAlgebraMap
29variable (C : ProCGroups.FiniteGroupClass.{u})
31variable {H K : Type u}
32variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
33variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
35/-- The finite-stage component of the target map on `Z_C[[H]]`. -/
37 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
39 (i.1, completedGroupAlgebraComapIndexInClass
40 (G := H) (H := K) C hC φ i.2) →+*
42 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.1.modulus)
43 (completedGroupAlgebraComapQuotientMapInClass (G := H) (H := K) C hC φ i.2)
45@[simp]
47 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
48 (q : CompletedGroupAlgebraQuotientInClass H C
49 (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2)) :
51 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus) _ q) =
52 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus) _
53 (completedGroupAlgebraComapQuotientMapInClass (G := H) (H := K) C hC φ i.2 q) := by
54 simp only [zcCompletedGroupAlgebraMapStage, MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk,
55 OneHom.coe_mk, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
58 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
59 (q : CompletedGroupAlgebraQuotientInClass H C
60 (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2))
61 (a : ModNCompletedCoeff i.1.modulus) :
62 zcCompletedGroupAlgebraMapStage C hC φ i (MonoidAlgebra.single q a) =
63 MonoidAlgebra.single
64 (completedGroupAlgebraComapQuotientMapInClass (G := H) (H := K) C hC φ i.2 q) a := by
65 simp only [zcCompletedGroupAlgebraMapStage, MonoidAlgebra.single, MonoidAlgebra.mapDomainRingHom_apply,
66 Finsupp.mapDomain_single]
68/-- A surjective target homomorphism induces a surjective map on every finite
69`Z_C`-coefficient, `C`-quotient stage of the completed group algebra. -/
71 (φ : H →ₜ* K) (hφ : Function.Surjective φ)
73 Function.Surjective (zcCompletedGroupAlgebraMapStage C hC φ i) := by
74 simpa [zcCompletedGroupAlgebraMapStage, MonoidAlgebra.mapDomainRingHom_apply] using
75 (Finsupp.mapDomain_surjective (M := ModNCompletedCoeff i.1.modulus)
76 (completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
77 (G := H) (H := K) C hC φ hφ i.2))
79/-- A finite-stage target map is linear over the common residue coefficient ring. -/
81 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
82 (a : ModNCompletedCoeff i.1.modulus)
83 (x :
85 (i.1, completedGroupAlgebraComapIndexInClass
86 (G := H) (H := K) C hC φ i.2)) :
87 zcCompletedGroupAlgebraMapStage C hC φ i (a • x) =
88 a • zcCompletedGroupAlgebraMapStage C hC φ i x := by
89 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
90 rw [Algebra.smul_def, Algebra.smul_def, RingHom.map_mul]
91 simp only [zcCompletedGroupAlgebraMapStage, map_intCast, MonoidAlgebra.mapDomainRingHom_apply]
93/-- The kernel ideal of a finite-stage target map on completed group algebras. -/
95 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
96 Ideal
98 (i.1, completedGroupAlgebraComapIndexInClass
99 (G := H) (H := K) C hC φ i.2)) :=
100 RingHom.ker (zcCompletedGroupAlgebraMapStage C hC φ i)
102@[simp]
104 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
105 {x :
107 (i.1, completedGroupAlgebraComapIndexInClass
108 (G := H) (H := K) C hC φ i.2)} :
110 zcCompletedGroupAlgebraMapStage C hC φ i x = 0 := by
113/-- The finite-stage relation augmentation generator attached to an element of the quotient kernel.
114-/
116 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
117 (q :
118 (completedGroupAlgebraComapQuotientMapInClass
119 (G := H) (H := K) C hC φ i.2).ker) :
121 (i.1, completedGroupAlgebraComapIndexInClass
122 (G := H) (H := K) C hC φ i.2) :=
123 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
124 (CompletedGroupAlgebraQuotientInClass H C
125 (completedGroupAlgebraComapIndexInClass
126 (G := H) (H := K) C hC φ i.2)) q.1 - 1
128/-- The finite-stage relation augmentation ideal for a target map. -/
130 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
131 Ideal
133 (i.1, completedGroupAlgebraComapIndexInClass
134 (G := H) (H := K) C hC φ i.2)) :=
135 Ideal.span
136 (Set.range
139/-- A finite-stage relation augmentation generator lies in the kernel ideal. -/
141 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
142 (q :
143 (completedGroupAlgebraComapQuotientMapInClass
144 (G := H) (H := K) C hC φ i.2).ker) :
149 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
150 (CompletedGroupAlgebraQuotientInClass H C
151 (completedGroupAlgebraComapIndexInClass
152 (G := H) (H := K) C hC φ i.2)) q.1 - 1) = 0
154 have hq :
155 completedGroupAlgebraComapQuotientMapInClass
156 (G := H) (H := K) C hC φ i.2 q.1 = 1 := by
157 exact MonoidHom.mem_ker.mp
158 (show (q : CompletedGroupAlgebraQuotientInClass H C
159 (completedGroupAlgebraComapIndexInClass
160 (G := H) (H := K) C hC φ i.2)) ∈
161 (completedGroupAlgebraComapQuotientMapInClass
162 (G := H) (H := K) C hC φ i.2).ker from q.2)
163 rw [hq]
164 simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.one_def, sub_self]
166/-- The finite-stage relation augmentation ideal is contained in the finite-stage kernel ideal. -/
168 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
171 refine Ideal.span_le.2 ?_
172 rintro x ⟨q, rfl⟩
174 C hC φ i q
176/-- A linear section of a surjective finite-stage target map, obtained by choosing a source
177quotient lift for each target quotient basis element. -/
179 (φ : H →ₜ* K) (hφ : Function.Surjective φ)
183 (i.1, completedGroupAlgebraComapIndexInClass
184 (G := H) (H := K) C hC φ i.2) :=
185 Finsupp.linearCombination (ModNCompletedCoeff i.1.modulus)
186 (fun q : CompletedGroupAlgebraQuotientInClass K C i.2 =>
187 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
188 (CompletedGroupAlgebraQuotientInClass H C
189 (completedGroupAlgebraComapIndexInClass
190 (G := H) (H := K) C hC φ i.2))
191 (Function.surjInv
192 (completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
193 (G := H) (H := K) C hC φ hφ i.2) q))
195@[simp 900]
197 (φ : H →ₜ* K) (hφ : Function.Surjective φ)
199 (q : CompletedGroupAlgebraQuotientInClass K C i.2) :
201 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
202 (CompletedGroupAlgebraQuotientInClass K C i.2) q) =
203 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
204 (CompletedGroupAlgebraQuotientInClass H C
205 (completedGroupAlgebraComapIndexInClass
206 (G := H) (H := K) C hC φ i.2))
207 (Function.surjInv
208 (completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
209 (G := H) (H := K) C hC φ hφ i.2) q) := by
210 change
211 (Finsupp.linearCombination (ModNCompletedCoeff i.1.modulus)
212 (fun q : CompletedGroupAlgebraQuotientInClass K C i.2 =>
213 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
214 (CompletedGroupAlgebraQuotientInClass H C
215 (completedGroupAlgebraComapIndexInClass
216 (G := H) (H := K) C hC φ i.2))
217 (Function.surjInv
218 (completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
219 (G := H) (H := K) C hC φ hφ i.2) q)))
220 (Finsupp.single q (1 : ModNCompletedCoeff i.1.modulus)) = _
221 rw [Finsupp.linearCombination_single, one_smul]
223/-- The chosen finite-stage section is a right inverse to the finite-stage target map. -/
225 (φ : H →ₜ* K) (hφ : Function.Surjective φ)
230 classical
231 refine MonoidAlgebra.induction_on
232 (p := fun y : ZCCompletedGroupAlgebraStage C K i =>
235 y ?single ?add ?smul
236 · intro q
239 exact congrArg
240 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
241 (CompletedGroupAlgebraQuotientInClass K C i.2))
242 (Function.surjInv_eq
243 (completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
244 (G := H) (H := K) C hC φ hφ i.2) q)
245 · intro x y hx hy
246 rw [map_add, map_add, hx, hy]
247 · intro a y hy
250/-- A source basis element differs from the chosen lift of its target image by a finite-stage
251relation-augmentation element. -/
253 (φ : H →ₜ* K) (hφ : Function.Surjective φ)
255 (s :
256 CompletedGroupAlgebraQuotientInClass H C
257 (completedGroupAlgebraComapIndexInClass
258 (G := H) (H := K) C hC φ i.2)) :
259 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
260 (CompletedGroupAlgebraQuotientInClass H C
261 (completedGroupAlgebraComapIndexInClass
262 (G := H) (H := K) C hC φ i.2)) s -
265 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
266 (CompletedGroupAlgebraQuotientInClass H C
267 (completedGroupAlgebraComapIndexInClass
268 (G := H) (H := K) C hC φ i.2)) s)) ∈
270 let f :=
271 completedGroupAlgebraComapQuotientMapInClass
272 (G := H) (H := K) C hC φ i.2
273 let hfsurj :
274 Function.Surjective f :=
275 completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
276 (G := H) (H := K) C hC φ hφ i.2
277 let t : CompletedGroupAlgebraQuotientInClass K C i.2 := f s
278 let lift :
279 CompletedGroupAlgebraQuotientInClass H C
280 (completedGroupAlgebraComapIndexInClass
281 (G := H) (H := K) C hC φ i.2) :=
282 Function.surjInv hfsurj t
283 let q : f.ker :=
284 ⟨lift⁻¹ * s, by
285 change f (lift⁻¹ * s) = 1
286 rw [map_mul, map_inv]
287 have hlift : f lift = t := Function.surjInv_eq hfsurj t
288 rw [hlift]
289 simp only [inv_mul_cancel, t]⟩
290 have hsection :
293 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
294 (CompletedGroupAlgebraQuotientInClass H C
295 (completedGroupAlgebraComapIndexInClass
296 (G := H) (H := K) C hC φ i.2)) s)) =
297 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
298 (CompletedGroupAlgebraQuotientInClass H C
299 (completedGroupAlgebraComapIndexInClass
300 (G := H) (H := K) C hC φ i.2)) lift := by
303 rw [hsection]
304 have hmul :
305 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
306 (CompletedGroupAlgebraQuotientInClass H C
307 (completedGroupAlgebraComapIndexInClass
308 (G := H) (H := K) C hC φ i.2)) lift *
310 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
311 (CompletedGroupAlgebraQuotientInClass H C
312 (completedGroupAlgebraComapIndexInClass
313 (G := H) (H := K) C hC φ i.2)) s -
314 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
315 (CompletedGroupAlgebraQuotientInClass H C
316 (completedGroupAlgebraComapIndexInClass
317 (G := H) (H := K) C hC φ i.2)) lift := by
319 MonoidAlgebra.of_apply]
320 rw [mul_sub, MonoidAlgebra.single_mul_single, mul_one]
321 simp only [mul_inv_cancel_left, mul_one]
322 rw [← hmul]
323 exact
325 (Ideal.subset_span ⟨q, rfl⟩)
327/-- Every finite-stage source group-algebra element differs from the chosen lift of its target
328image by a relation-augmentation element. -/
330 (φ : H →ₜ* K) (hφ : Function.Surjective φ)
332 (x :
334 (i.1, completedGroupAlgebraComapIndexInClass
335 (G := H) (H := K) C hC φ i.2)) :
339 classical
340 refine MonoidAlgebra.induction_on
341 (p := fun x :
343 (i.1, completedGroupAlgebraComapIndexInClass
344 (G := H) (H := K) C hC φ i.2) =>
348 x ?single ?add ?smul
349 · intro s
350 exact
352 C hC φ hφ i s
353 · intro x y hx hy
354 have hcalc :
356 (zcCompletedGroupAlgebraMapStage C hC φ i (x + y)) =
362 abel
363 rw [hcalc]
364 exact
366 · intro a x hx
367 have hmap_smul :
368 zcCompletedGroupAlgebraMapStage C hC φ i (a • x) =
371 have hcalc :
373 (zcCompletedGroupAlgebraMapStage C hC φ i (a • x)) =
376 rw [hmap_smul, map_smul, smul_sub]
377 rw [hcalc]
378 rw [Algebra.smul_def]
379 exact
382/-- In each finite stage, the kernel of a surjective target map is exactly the relation
383augmentation ideal generated by the kernel of the finite quotient map. -/
385 (φ : H →ₜ* K) (hφ : Function.Surjective φ)
389 apply le_antisymm
390 · intro x hx
391 have hxmap :
394 (C := C) (hC := hC) φ i).1 hx
395 have hdiff :=
397 C hC φ hφ i x
398 rw [hxmap, map_zero, sub_zero] at hdiff
399 exact hdiff
402/-- Target finite-stage maps commute with the pro-`C` transition maps. -/
404 (φ : H →ₜ* K)
405 {i j : ZCCompletedGroupAlgebraIndex C K} (hij : i ≤ j) :
410 (show
411 (i.1, completedGroupAlgebraComapIndexInClass
412 (G := H) (H := K) C hC φ i.2) ≤
413 (j.1, completedGroupAlgebraComapIndexInClass
414 (G := H) (H := K) C hC φ j.2) from
415 ⟨hij.1,
416 completedGroupAlgebraComapIndexInClass_mono
417 (G := H) (H := K) C hC φ hij.2⟩)) := by
418 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
419 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
420 apply RingHom.ext
421 intro x
422 refine MonoidAlgebra.induction_on
423 (p := fun x =>
428 (show
429 (i.1, completedGroupAlgebraComapIndexInClass
430 (G := H) (H := K) C hC φ i.2) ≤
431 (j.1, completedGroupAlgebraComapIndexInClass
432 (G := H) (H := K) C hC φ j.2) from
433 ⟨hij.1,
434 completedGroupAlgebraComapIndexInClass_mono
435 (G := H) (H := K) C hC φ hij.2⟩))) x)
436 x ?_ ?_ ?_
437 · intro q
438 rw [RingHom.comp_apply, RingHom.comp_apply,
441 change
442 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
443 (CompletedGroupAlgebraQuotientInClass K C i.2)
444 ((OpenNormalSubgroupInClass.map
445 (C := C) (G := K)
446 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2)
447 (completedGroupAlgebraComapQuotientMapInClass
448 (G := H) (H := K) C hC φ j.2 q)) =
450 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
451 (CompletedGroupAlgebraQuotientInClass H C
452 (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2))
453 ((OpenNormalSubgroupInClass.map
454 (C := C) (G := H)
455 (U := OrderDual.ofDual
456 (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2))
457 (V := OrderDual.ofDual
458 (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2))
459 (completedGroupAlgebraComapIndexInClass_mono
460 (G := H) (H := K) C hC φ hij.2)) q))
462 exact congrArg (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
463 (CompletedGroupAlgebraQuotientInClass K C i.2))
464 (congrFun
465 (congrArg DFunLike.coe
466 (completedGroupAlgebraComapQuotientMapInClass_compatible
467 (G := H) (H := K) C hC φ hij.2)) q)
468 · intro x y hx hy
469 rw [map_add, map_add, hx, hy]
470 · intro a x hx
471 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
472 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
475 RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, MonoidAlgebra.mapDomainRingHom_apply]
477/-- The completed group-algebra map `Z_C[[H]] -> Z_C[[K]]` induced by a continuous homomorphism
478`H -> K`. -/
479def zcCompletedGroupAlgebraMap (φ : H →ₜ* K) :
481 toFun x := ⟨fun i =>
484 (i.1, completedGroupAlgebraComapIndexInClass
485 (G := H) (H := K) C hC φ i.2) x), by
486 intro i j hij
487 let hsource :
488 (i.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2) ≤
489 (j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2) :=
490 ⟨hij.1, completedGroupAlgebraComapIndexInClass_mono
491 (G := H) (H := K) C hC φ hij.2⟩
492 have hx := x.2
493 (i.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2)
494 (j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2)
495 hsource
496 have hcompat := congrFun
497 (congrArg DFunLike.coe
500 (j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2) x)
501 rw [RingHom.comp_apply, RingHom.comp_apply] at hcompat
502 rw [hx] at hcompat
503 simpa using hcompat⟩
504 map_zero' := by
505 apply Subtype.ext
506 funext i
508 MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_zero]
509 map_add' := by
510 intro x y
511 apply Subtype.ext
512 funext i
514 map_one' := by
515 apply Subtype.ext
516 funext i
518 MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_one]
519 map_mul' := by
520 intro x y
521 apply Subtype.ext
522 funext i
525@[simp]
527 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
532 (i.1, completedGroupAlgebraComapIndexInClass
533 (G := H) (H := K) C hC φ i.2) x) :=
534 rfl
536/-- Membership in the kernel of the completed target map is exactly membership in the kernel of
537every target-indexed finite stage. -/
539 (φ : H →ₜ* K) (x : ZCCompletedGroupAlgebra C H) :
540 x ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC φ) ↔
543 (i.1, completedGroupAlgebraComapIndexInClass
544 (G := H) (H := K) C hC φ i.2) x ∈
546 constructor
547 · intro hx i
549 have hmap : zcCompletedGroupAlgebraMap C hC φ x = 0 :=
550 (RingHom.mem_ker).1 hx
551 have hi := congrArg (zcCompletedGroupAlgebraProjection C K i) hmap
553 · intro hstage
554 rw [RingHom.mem_ker]
555 apply Subtype.ext
556 funext i
560 have hi :
563 (i.1, completedGroupAlgebraComapIndexInClass
564 (G := H) (H := K) C hC φ i.2) x) = 0 :=
566 (C := C) (hC := hC) φ i).1 (hstage i)
567 simpa using hi
569/-- For a surjective target map, membership in the completed kernel is equivalently membership
570in the explicit relation-augmentation ideal at every target-indexed finite stage. -/
572 (φ : H →ₜ* K) (hφ : Function.Surjective φ)
574 x ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC φ) ↔
577 (i.1, completedGroupAlgebraComapIndexInClass
578 (G := H) (H := K) C hC φ i.2) x ∈
580 constructor
581 · intro hx i
583 C hC φ x).1 hx i
585 C hC φ hφ i] at hi
586 · intro hstage
588 (fun i => by
590 C hC φ hφ i]
591 exact hstage i)
593@[simp]
595 (φ : H →ₜ* K) (h : H) :
597 zcGroupLike C K (φ h) := by
598 apply Subtype.ext
599 funext i
600 change
608 exact congrArg
609 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
610 (CompletedGroupAlgebraQuotientInClass K C i.2))
611 (completedGroupAlgebraComapQuotientMapInClass_mk
612 (G := H) (H := K) C hC φ i.2 h)
614@[simp]
616 {G : Type v} [Group G] (φ : H →ₜ* K) (ψ : G →* H) (g : G) :
618 zcCompletedGroupAlgebraScalar C (φ.toMonoidHom.comp ψ) g := by
619 simp only [zcCompletedGroupAlgebraScalar, MonoidHom.coe_comp, Function.comp_apply,
620 zcCompletedGroupAlgebraMap_groupLike, ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.coe_coe]
622@[simp]
624 {G : Type v} [Group G] (φ : H →ₜ* K) (ψ : G →* H) (g : G) :
626 zcCompletedGroupAlgebraBoundary C (φ.toMonoidHom.comp ψ) g := by
628 ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply]
630/-- A finite-stage target map preserves the finite augmentation. -/
632 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
636 (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2) := by
637 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
638 apply RingHom.ext
639 intro y
640 let U := i.2
641 let V := completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ U
642 let P := fun y =>
646 change P y
647 refine MonoidAlgebra.induction_on (p := P) y ?_ ?_ ?_
648 · intro q
649 dsimp [P]
652 · intro a b ha hb
653 dsimp [P] at ha hb ⊢
654 rw [RingHom.map_add, map_add, ha, hb, map_add]
655 · intro a y hy
656 dsimp [P] at hy ⊢
657 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hy]
658 have hcoeff :
661 (algebraMap (ModNCompletedCoeff i.1.modulus)
662 (ZCCompletedGroupAlgebraStage C H (i.1, V)) a) =
664 (algebraMap (ModNCompletedCoeff i.1.modulus)
665 (ZCCompletedGroupAlgebraStage C H (i.1, V)) a) := by
666 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
668 V]
669 have hcoeff' :
672 (algebraMap (ModNCompletedCoeff i.1.modulus)
673 (ZCCompletedGroupAlgebraStage C H (i.1, V)) a)) =
675 (algebraMap (ModNCompletedCoeff i.1.modulus)
676 (ZCCompletedGroupAlgebraStage C H (i.1, V)) a) := by
677 simpa [RingHom.comp_apply] using hcoeff
678 rw [hcoeff', map_mul]
680/-- Completed augmentation is natural for target maps. -/
681@[simp 900]
684 (φ : H →ₜ* K) (x : ZCCompletedGroupAlgebra C H) :
687 ext i
691 let U : CompletedGroupAlgebraIndexInClass K C := zcCompletedGroupAlgebraTopIndex C K
692 let V : CompletedGroupAlgebraIndexInClass H C := zcCompletedGroupAlgebraTopIndex C H
693 have hV :
694 completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ U = V := by
697 change
704 cases hV
706 (i, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ U) x
707 change
711 (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ U)) y
712 exact congrFun
713 (congrArg DFunLike.coe
716/-- The target map on completed `Z_C` group algebras induced by the identity homomorphism is
717the identity ring homomorphism. -/
718@[simp 900]
720 zcCompletedGroupAlgebraMap C hC (ContinuousMonoidHom.id H) =
721 RingHom.id (ZCCompletedGroupAlgebra C H) := by
722 apply RingHom.ext
723 intro x
724 apply Subtype.ext
725 funext i
727 (zcCompletedGroupAlgebraMap C hC (ContinuousMonoidHom.id H) x) =
730 have hfull :
731 (i.1, completedGroupAlgebraComapIndexInClass (G := H) (H := H) C hC
732 (ContinuousMonoidHom.id H) i.2) = i := by
733 cases i
735 cases hfull
736 change zcCompletedGroupAlgebraMapStage C hC (ContinuousMonoidHom.id H) i (x.1 i) =
737 x.1 i
738 refine MonoidAlgebra.induction_on
739 (p := fun y => zcCompletedGroupAlgebraMapStage C hC (ContinuousMonoidHom.id H) i y = y)
740 (x.1 i) ?_ ?_ ?_
741 · intro q
742 rcases QuotientGroup.mk'_surjective
743 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup H) : Subgroup H)) q with
744 ⟨g, rfl⟩
746 rfl
747 · intro a b ha hb
748 rw [map_add, ha, hb]
749 · intro a y hy
750 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
751 rw [Algebra.smul_def, RingHom.map_mul, hy]
752 simp only [zcCompletedGroupAlgebraMapStage, map_intCast]
754/-- Target maps on completed `Z_C` group algebras compose functorially.
756The proof uses the index-level composition law to bridge the non-defeq inverse-limit source
757stage produced by the composite target homomorphism. -/
758@[simp 900]
760 {L : Type u} [Group L] [TopologicalSpace L] [IsTopologicalGroup L]
761 (φ : H →ₜ* K) (ψ : K →ₜ* L) :
762 zcCompletedGroupAlgebraMap C hC (ψ.comp φ) =
765 apply RingHom.ext
766 intro x
767 apply Subtype.ext
768 funext i
770 (zcCompletedGroupAlgebraMap C hC (ψ.comp φ) x) =
776 (i.1, completedGroupAlgebraComapIndexInClass (G := K) (H := L) C hC ψ i.2)
777 change zcCompletedGroupAlgebraMapStage C hC (ψ.comp φ) i
779 (i.1, completedGroupAlgebraComapIndexInClass
780 (G := H) (H := L) C hC (ψ.comp φ) i.2) x) =
785 have hidx :
786 (i.1, completedGroupAlgebraComapIndexInClass
787 (G := H) (H := L) C hC (ψ.comp φ) i.2) =
788 (j.1, completedGroupAlgebraComapIndexInClass
789 (G := H) (H := K) C hC φ j.2) := by
790 subst j
792 cases hidx
793 change zcCompletedGroupAlgebraMapStage C hC (ψ.comp φ) i
795 (j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2) x) =
799 (j.1, completedGroupAlgebraComapIndexInClass
800 (G := H) (H := K) C hC φ j.2) x))
801 let P := fun y =>
802 zcCompletedGroupAlgebraMapStage C hC (ψ.comp φ) i y =
806 (j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2) x)
807 refine MonoidAlgebra.induction_on
808 (p := P)
810 (j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2) x)
811 ?_ ?_ ?_
812 · intro q
813 refine QuotientGroup.induction_on q ?_
814 intro g
815 dsimp [P]
819 rfl
820 · intro a b ha hb
821 dsimp [P] at ha hb
822 dsimp [P]
823 rw [map_add, map_add, map_add, ha, hb]
824 · intro a y hy
825 dsimp [P] at hy
826 dsimp [P]
827 let t : ℤ := Classical.choose (ZMod.intCast_surjective a)
828 have ht : (t : ModNCompletedCoeff j.1.modulus) = a :=
829 Classical.choose_spec (ZMod.intCast_surjective a)
830 rw [← ht, Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, RingHom.map_mul, hy]
831 simp only [zcCompletedGroupAlgebraMapStage, map_intCast, MonoidAlgebra.mapDomainRingHom_apply]
833end CompletedGroupAlgebraMap
835section UniversalTarget
837variable (C : ProCGroups.FiniteGroupClass.{v})
839variable {G : Type u} [Group G]
840variable {H K : Type v}
841variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
842variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
844/-- Target functoriality of the completed universal differential module.
846The codomain is viewed as a `Z_C[[H]]`-module by restricting scalars along the completed
847group-algebra map induced by `φ : H -> K`. On universal differentials this sends
848`d_ψ g` to `d_{φ ∘ ψ} g`. -/
850 (ψ : G →* H) (φ : H →ₜ* K) :
851 letI : Module (ZCCompletedGroupAlgebra C H)
852 (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
853 Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
855 ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ) := by
856 letI : Module (ZCCompletedGroupAlgebra C H)
857 (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
858 Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
859 exact
861 (A := ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ))
862 C ψ (fun g => zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g) (by
863 intro g h
864 change zcUniversalDifferential C (φ.toMonoidHom.comp ψ) (g * h) =
865 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
867 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h
869 change zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
870 zcCompletedGroupAlgebraScalar C (φ.toMonoidHom.comp ψ) g •
871 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h =
872 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
874 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h
877@[simp 900]
879 (ψ : G →* H) (φ : H →ₜ* K) (g : G) :
880 letI : Module (ZCCompletedGroupAlgebra C H)
881 (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
882 Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
885 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g := by
886 letI : Module (ZCCompletedGroupAlgebra C H)
887 (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
888 Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
889 exact
891 (A := ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ))
892 C ψ (fun g => zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g) (by
893 intro g h
894 change zcUniversalDifferential C (φ.toMonoidHom.comp ψ) (g * h) =
895 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
897 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h
899 change zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
900 zcCompletedGroupAlgebraScalar C (φ.toMonoidHom.comp ψ) g •
901 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h =
902 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
904 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h
906 g
908include hC
910/-- Completed universal zero descends along a target homomorphism. -/
912 (ψ : G →* H) (φ : H →ₜ* K) {g : G}
913 (hg : zcUniversalDifferential C ψ g = 0) :
914 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g = 0 := by
915 letI : Module (ZCCompletedGroupAlgebra C H)
916 (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
917 Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
920variable {G' : Type u} [Group G']
922/-- Completed universal zero descends along a commuting source/target square.
924This is the finite-quotient form used by Magnus arguments: if
925`ψ' ∘ f = φ ∘ ψ`, then zero for `d_ψ g` implies zero for `d_{ψ'} (f g)`. -/
927 (ψ : G →* H) (ψ' : G' →* K) (f : G →* G') (φ : H →ₜ* K)
928 (hcomm : ψ'.comp f = φ.toMonoidHom.comp ψ) {g : G}
929 (hg : zcUniversalDifferential C ψ g = 0) :
930 zcUniversalDifferential C ψ' (f g) = 0 := by
931 have ht :
932 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g = 0 :=
934 have hs :
935 zcUniversalDifferential C (ψ'.comp f) g = 0 := by
936 rw [hcomm]
937 exact ht
940end UniversalTarget
942section FreeGroup
944variable (C : ProCGroups.FiniteGroupClass.{v})
946variable {X : Type u} [DecidableEq X]
947variable {H K : Type v}
948variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
949variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
951/-- Push completed Fox-coordinate vectors forward along a continuous homomorphism of target
952groups. -/
953def zcFreeFoxCoordinatesMap (φ : H →ₜ* K) :
954 ZCFreeFoxCoordinates C (X := X) (H := H) →
955 ZCFreeFoxCoordinates C (X := X) (H := K) :=
956 fun a x => zcCompletedGroupAlgebraMap C hC φ (a x)
958omit [DecidableEq X] in
959@[simp]
961 (φ : H →ₜ* K) (a : ZCFreeFoxCoordinates C (X := X) (H := H)) (x : X) :
962 zcFreeFoxCoordinatesMap (X := X) C hC φ a x =
964 rfl
966omit [DecidableEq X] in
967/-- The coordinatewise target map induced by the identity homomorphism is the identity map. -/
968@[simp]
970 (a : ZCFreeFoxCoordinates C (X := X) (H := H)) :
971 zcFreeFoxCoordinatesMap (X := X) C hC (ContinuousMonoidHom.id H) a = a := by
972 funext x
975omit [DecidableEq X] in
976/-- Coordinatewise target maps on completed Fox-coordinate vectors compose functorially. -/
977@[simp]
979 {L : Type v} [Group L] [TopologicalSpace L] [IsTopologicalGroup L]
980 (φ : H →ₜ* K) (ψ : K →ₜ* L)
981 (a : ZCFreeFoxCoordinates C (X := X) (H := H)) :
982 zcFreeFoxCoordinatesMap (X := X) C hC (ψ.comp φ) a =
983 zcFreeFoxCoordinatesMap (X := X) C hC ψ
984 (zcFreeFoxCoordinatesMap (X := X) C hC φ a) := by
985 funext x
986 simp only [zcFreeFoxCoordinatesMap, zcCompletedGroupAlgebraMap_comp, RingHom.coe_comp, Function.comp_apply]
988/-- Completed free-group Fox derivatives are natural under target push-forward. -/
990 (ψ : FreeGroup X →* H) (φ : H →ₜ* K) (w : FreeGroup X) :
991 zcFreeGroupFoxDerivativeVector C (φ.toMonoidHom.comp ψ) w =
993 let delta : FreeGroup X → ZCFreeFoxCoordinates C (X := X) (H := K) :=
995 have hdelta :
997 (zcCompletedGroupAlgebraScalar C (φ.toMonoidHom.comp ψ)) delta := by
998 intro u v
999 funext x
1001 zcCompletedGroupAlgebraScalar_apply, Pi.add_apply, Pi.smul_apply, smul_eq_mul, map_add, map_mul,
1002 zcCompletedGroupAlgebraMap_groupLike, ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.coe_comp, MonoidHom.coe_coe,
1003 Function.comp_apply, delta]
1004 have hbasis :
1005 ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : ZCCompletedGroupAlgebra C K) := by
1006 intro x
1007 funext y
1008 by_cases hxy : x = y
1009 · subst y
1011 delta]
1012 · simp only [zcFreeFoxCoordinatesMap_apply, zcFreeGroupFoxDerivativeVector_of, ne_eq, hxy, not_false_eq_true,
1013 Pi.single_eq_of_ne', map_zero, delta]
1014 have hdelta_eq :
1015 delta = zcFreeGroupFoxDerivativeVector C (φ.toMonoidHom.comp ψ) :=
1016 zcFreeGroupFoxDerivativeVector_unique C (φ.toMonoidHom.comp ψ) delta hdelta hbasis
1017 rw [← congrFun hdelta_eq w]
1020 (ψ : FreeGroup X →* H) (φ : H →ₜ* K) (w : FreeGroup X) (x : X) :
1021 zcFreeGroupFoxDerivative C (φ.toMonoidHom.comp ψ) x w =
1023 have h := congrFun (zcFreeGroupFoxDerivativeVector_mapTarget C hC ψ φ w) x
1026section FiniteBasis
1028variable [Fintype X]
1030omit [DecidableEq X] in
1032 (ψ : FreeGroup X →* H) (φ : H →ₜ* K)
1033 (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
1035 zcFreeGroupFoxBoundary C (φ.toMonoidHom.comp ψ)
1036 (zcFreeFoxCoordinatesMap (X := X) C hC φ v) := by
1038 map_one, ContinuousMonoidHom.coe_toMonoidHom, zcFreeFoxCoordinatesMap, MonoidHom.coe_comp, MonoidHom.coe_coe,
1039 Function.comp_apply]
1042 (ψ : FreeGroup X →* H) (φ : H →ₜ* K) (w : FreeGroup X) :
1045 zcFreeGroupFoxBoundary C (φ.toMonoidHom.comp ψ)
1046 (zcFreeGroupFoxDerivativeVector C (φ.toMonoidHom.comp ψ) w) := by
1050 (ψ : FreeGroup X →* H) (φ : H →ₜ* K) (w : FreeGroup X) :
1051 zcCompletedGroupAlgebraMap C hC φ (zcGroupLike C H (ψ w) - 1) =
1052 ∑ i : X,
1053 zcFreeGroupFoxDerivative C (φ.toMonoidHom.comp ψ) i w *
1054 (zcGroupLike C K ((φ.toMonoidHom.comp ψ) (FreeGroup.of i)) - 1) := by
1058end FiniteBasis
1060end FreeGroup
1062end
1064end FoxDifferential