Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Naturality
ProCGroups/FoxDifferential/Completed/ProCIntegerCoefficients/Naturality/Source

Source: ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Naturality

1import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Augmentation
2import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Core
3import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Fundamental
5/-!
6# Fox differential: completed — \(\mathbb{Z}_C\) coefficients — naturality
8The principal declarations in this module are:
10- `zcCompletedGroupAlgebraMapStage`
11 The finite-stage component of the target map on \(\mathbb{Z}_C\llbracket H\rrbracket\).
12- `zcCompletedGroupAlgebraMapStageKernelIdeal`
13 The kernel ideal of a finite-stage target map on completed group algebras.
14- `zcCompletedGroupAlgebraMapStage_of`
15 The finite stage of the \(\mathbb{Z}_C\)-completed group-algebra map sends a group-like basis
16 element to the basis element supported at its image.
17- `zcCompletedGroupAlgebraMapStage_single`
18 The finite stage of the \(\mathbb{Z}_C\)-completed group-algebra map transports a singleton to the
19 singleton at its quotient image.
20-/
22namespace FoxDifferential
24noncomputable section
26open scoped BigOperators
27open ProCGroups.ProC
29universe u v
31section CompletedGroupAlgebraMap
33variable (C : ProCGroups.FiniteGroupClass.{u})
35variable {H K : Type u}
36variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
37variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
39/-- The finite-stage component of the target map on \(\mathbb{Z}_C\llbracket H\rrbracket\). -/
40def zcCompletedGroupAlgebraMapStage
41 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
42 ZCCompletedGroupAlgebraStage C H
43 (i.1, completedGroupAlgebraComapIndexInClass
44 (G := H) (H := K) C hC φ i.2) →+*
45 ZCCompletedGroupAlgebraStage C K i :=
46 MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.1.modulus)
47 (completedGroupAlgebraComapQuotientMapInClass (G := H) (H := K) C hC φ i.2)
49/--
50The finite stage of the \(\mathbb{Z}_C\)-completed group-algebra map sends a group-like basis
51element to the basis element supported at its image.
52-/
53@[simp]
54theorem zcCompletedGroupAlgebraMapStage_of
55 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
56 (q : CompletedGroupAlgebraQuotientInClass H C
57 (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2)) :
58 zcCompletedGroupAlgebraMapStage C hC φ i
59 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus) _ q) =
60 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus) _
61 (completedGroupAlgebraComapQuotientMapInClass (G := H) (H := K) C hC φ i.2 q) := by
62 simp only [zcCompletedGroupAlgebraMapStage, MonoidAlgebra.of_apply,
63 MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_single]
65/--
66The finite stage of the \(\mathbb{Z}_C\)-completed group-algebra map transports a singleton to the
67singleton at its quotient image.
68-/
69theorem zcCompletedGroupAlgebraMapStage_single
70 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
71 (q : CompletedGroupAlgebraQuotientInClass H C
72 (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2))
73 (a : ModNCompletedCoeff i.1.modulus) :
74 zcCompletedGroupAlgebraMapStage C hC φ i (MonoidAlgebra.single q a) =
75 MonoidAlgebra.single
76 (completedGroupAlgebraComapQuotientMapInClass (G := H) (H := K) C hC φ i.2 q) a := by
77 simp only [zcCompletedGroupAlgebraMapStage, MonoidAlgebra.mapDomainRingHom_apply,
78 MonoidAlgebra.mapDomain_single]
80/--
81A surjective target homomorphism induces a surjective map on every finite
82\(\mathbb{Z}_C\)-coefficient, \(C\)-quotient stage of the completed group algebra.
83-/
84theorem zcCompletedGroupAlgebraMapStage_surjective_of_surjective
85 (φ : H →ₜ* K) (hφ : Function.Surjective φ)
86 (i : ZCCompletedGroupAlgebraIndex C K) :
87 Function.Surjective (zcCompletedGroupAlgebraMapStage C hC φ i) := by
88 intro y
89 obtain ⟨x, hx⟩ :=
90 Finsupp.mapDomain_surjective (M := ModNCompletedCoeff i.1.modulus)
91 (completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
92 (G := H) (H := K) C hC φ hφ i.2) y.coeff
93 refine ⟨MonoidAlgebra.ofCoeff x, ?_⟩
94 apply MonoidAlgebra.coeff_injective
95 exact hx
97/-- A finite-stage target map is linear over the common residue coefficient ring. -/
98theorem zcCompletedGroupAlgebraMapStage_smul
99 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
100 (a : ModNCompletedCoeff i.1.modulus)
101 (x :
102 ZCCompletedGroupAlgebraStage C H
103 (i.1, completedGroupAlgebraComapIndexInClass
104 (G := H) (H := K) C hC φ i.2)) :
105 zcCompletedGroupAlgebraMapStage C hC φ i (a • x) =
106 a • zcCompletedGroupAlgebraMapStage C hC φ i x := by
107 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
108 rw [Algebra.smul_def, Algebra.smul_def, RingHom.map_mul]
109 simp only [zcCompletedGroupAlgebraMapStage, map_intCast, MonoidAlgebra.mapDomainRingHom_apply]
111/-- The kernel ideal of a finite-stage target map on completed group algebras. -/
112def zcCompletedGroupAlgebraMapStageKernelIdeal
113 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
114 Ideal
115 (ZCCompletedGroupAlgebraStage C H
116 (i.1, completedGroupAlgebraComapIndexInClass
117 (G := H) (H := K) C hC φ i.2)) :=
118 RingHom.ker (zcCompletedGroupAlgebraMapStage C hC φ i)
120/--
121Membership in the completed group-algebra stage-map kernel ideal is equivalent to vanishing of
122the corresponding finite-stage coordinate.
123-/
124@[simp]
125theorem mem_zcCompletedGroupAlgebraMapStageKernelIdeal_iff
126 {C : ProCGroups.FiniteGroupClass.{u}} {hC : C.Hereditary}
127 {φ : H →ₜ* K} {i : ZCCompletedGroupAlgebraIndex C K}
128 {x :
129 ZCCompletedGroupAlgebraStage C H
130 (i.1, completedGroupAlgebraComapIndexInClass
131 (G := H) (H := K) C hC φ i.2)} :
132 x ∈ zcCompletedGroupAlgebraMapStageKernelIdeal C hC φ i ↔
133 zcCompletedGroupAlgebraMapStage C hC φ i x = 0 := by
134 rw [zcCompletedGroupAlgebraMapStageKernelIdeal, RingHom.mem_ker]
136/--
137The finite-stage relation augmentation generator attached to an element of the quotient kernel.
138-/
139def zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator
140 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
141 (q :
142 (completedGroupAlgebraComapQuotientMapInClass
143 (G := H) (H := K) C hC φ i.2).ker) :
144 ZCCompletedGroupAlgebraStage C H
145 (i.1, completedGroupAlgebraComapIndexInClass
146 (G := H) (H := K) C hC φ i.2) :=
147 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
148 (CompletedGroupAlgebraQuotientInClass H C
149 (completedGroupAlgebraComapIndexInClass
150 (G := H) (H := K) C hC φ i.2)) q.1 - 1
152/-- The finite-stage relation augmentation ideal for a target map. -/
153def zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal
154 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
155 Ideal
156 (ZCCompletedGroupAlgebraStage C H
157 (i.1, completedGroupAlgebraComapIndexInClass
158 (G := H) (H := K) C hC φ i.2)) :=
159 Ideal.span
160 (Set.range
161 (zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator C hC φ i))
163/-- A finite-stage relation augmentation generator lies in the kernel ideal. -/
164theorem zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator_mem_kernelIdeal
165 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
166 (q :
167 (completedGroupAlgebraComapQuotientMapInClass
168 (G := H) (H := K) C hC φ i.2).ker) :
169 zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator C hC φ i q ∈
170 zcCompletedGroupAlgebraMapStageKernelIdeal C hC φ i := by
171 rw [mem_zcCompletedGroupAlgebraMapStageKernelIdeal_iff]
172 change zcCompletedGroupAlgebraMapStage C hC φ i
173 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
174 (CompletedGroupAlgebraQuotientInClass H C
175 (completedGroupAlgebraComapIndexInClass
176 (G := H) (H := K) C hC φ i.2)) q.1 - 1) = 0
177 rw [map_sub, map_one, zcCompletedGroupAlgebraMapStage_of]
178 have hq :
179 completedGroupAlgebraComapQuotientMapInClass
180 (G := H) (H := K) C hC φ i.2 q.1 = 1 := by
181 exact MonoidHom.mem_ker.mp
182 (show (q : CompletedGroupAlgebraQuotientInClass H C
183 (completedGroupAlgebraComapIndexInClass
184 (G := H) (H := K) C hC φ i.2)) ∈
185 (completedGroupAlgebraComapQuotientMapInClass
186 (G := H) (H := K) C hC φ i.2).ker from q.2)
187 rw [hq]
188 simp only [MonoidAlgebra.of_apply, MonoidAlgebra.one_def, sub_self]
190/-- The finite-stage relation augmentation ideal is contained in the finite-stage kernel ideal. -/
191theorem zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal_le_kernelIdeal
192 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
193 zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i ≤
194 zcCompletedGroupAlgebraMapStageKernelIdeal C hC φ i := by
195 refine Ideal.span_le.2 ?_
196 rintro x ⟨q, rfl⟩
197 exact zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator_mem_kernelIdeal
198 C hC φ i q
200/--
201A linear section of a surjective finite-stage target map, obtained by choosing a source quotient
202lift for each target quotient basis element.
203-/
204def zcCompletedGroupAlgebraMapStageTargetSection
205 (φ : H →ₜ* K) (hφ : Function.Surjective φ)
206 (i : ZCCompletedGroupAlgebraIndex C K) :
207 ZCCompletedGroupAlgebraStage C K i →ₗ[ModNCompletedCoeff i.1.modulus]
208 ZCCompletedGroupAlgebraStage C H
209 (i.1, completedGroupAlgebraComapIndexInClass
210 (G := H) (H := K) C hC φ i.2) :=
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))).comp
220 (MonoidAlgebra.coeffLinearEquiv
221 (ModNCompletedCoeff i.1.modulus)).toLinearMap
223/--
224The chosen target section sends a group-like basis element to a group-like basis element over its
225selected source representative.
226-/
227@[simp 900]
228theorem zcCompletedGroupAlgebraMapStageTargetSection_of
229 (φ : H →ₜ* K) (hφ : Function.Surjective φ)
230 (i : ZCCompletedGroupAlgebraIndex C K)
231 (q : CompletedGroupAlgebraQuotientInClass K C i.2) :
232 zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
233 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
234 (CompletedGroupAlgebraQuotientInClass K C i.2) q) =
235 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
236 (CompletedGroupAlgebraQuotientInClass H C
237 (completedGroupAlgebraComapIndexInClass
238 (G := H) (H := K) C hC φ i.2))
239 (Function.surjInv
240 (completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
241 (G := H) (H := K) C hC φ hφ i.2) q) := by
242 change
243 (Finsupp.linearCombination (ModNCompletedCoeff i.1.modulus)
244 (fun q : CompletedGroupAlgebraQuotientInClass K C i.2 =>
245 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
246 (CompletedGroupAlgebraQuotientInClass H C
247 (completedGroupAlgebraComapIndexInClass
248 (G := H) (H := K) C hC φ i.2))
249 (Function.surjInv
250 (completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
251 (G := H) (H := K) C hC φ hφ i.2) q)))
252 (Finsupp.single q (1 : ModNCompletedCoeff i.1.modulus)) = _
253 rw [Finsupp.linearCombination_single, one_smul]
255/-- The chosen finite-stage section is a right inverse to the finite-stage target map. -/
256theorem zcCompletedGroupAlgebraMapStage_targetSection
257 (φ : H →ₜ* K) (hφ : Function.Surjective φ)
258 (i : ZCCompletedGroupAlgebraIndex C K)
259 (y : ZCCompletedGroupAlgebraStage C K i) :
260 zcCompletedGroupAlgebraMapStage C hC φ i
261 (zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i y) = y := by
262 classical
263 refine MonoidAlgebra.induction_on
264 (p := fun y : ZCCompletedGroupAlgebraStage C K i =>
265 zcCompletedGroupAlgebraMapStage C hC φ i
266 (zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i y) = y)
267 y ?single ?add ?smul
268 · intro q
269 rw [zcCompletedGroupAlgebraMapStageTargetSection_of,
270 zcCompletedGroupAlgebraMapStage_of]
271 exact congrArg
272 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
273 (CompletedGroupAlgebraQuotientInClass K C i.2))
274 (Function.surjInv_eq
275 (completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
276 (G := H) (H := K) C hC φ hφ i.2) q)
277 · intro x y hx hy
278 rw [map_add, map_add, hx, hy]
279 · intro a y hy
280 rw [map_smul, zcCompletedGroupAlgebraMapStage_smul, hy]
282/--
283At a finite completed group-algebra stage, a source basis element minus the chosen lift of its
284target image lies in the relation augmentation ideal.
285-/
286theorem zcCompletedGAMapStage_sourceBasis_sub_targetSection_mem_relationAugmentationIdeal
287 (φ : H →ₜ* K) (hφ : Function.Surjective φ)
288 (i : ZCCompletedGroupAlgebraIndex C K)
289 (s :
290 CompletedGroupAlgebraQuotientInClass H C
291 (completedGroupAlgebraComapIndexInClass
292 (G := H) (H := K) C hC φ i.2)) :
293 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
294 (CompletedGroupAlgebraQuotientInClass H C
295 (completedGroupAlgebraComapIndexInClass
296 (G := H) (H := K) C hC φ i.2)) s -
297 zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
298 (zcCompletedGroupAlgebraMapStage C hC φ i
299 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
300 (CompletedGroupAlgebraQuotientInClass H C
301 (completedGroupAlgebraComapIndexInClass
302 (G := H) (H := K) C hC φ i.2)) s)) ∈
303 zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i := by
304 let f :=
305 completedGroupAlgebraComapQuotientMapInClass
306 (G := H) (H := K) C hC φ i.2
307 let hfsurj :
308 Function.Surjective f :=
309 completedGroupAlgebraComapQuotientMapInClass_surjective_of_surjective
310 (G := H) (H := K) C hC φ hφ i.2
311 let t : CompletedGroupAlgebraQuotientInClass K C i.2 := f s
312 let lift :
313 CompletedGroupAlgebraQuotientInClass H C
314 (completedGroupAlgebraComapIndexInClass
315 (G := H) (H := K) C hC φ i.2) :=
316 Function.surjInv hfsurj t
317 let q : f.ker :=
318 ⟨lift⁻¹ * s, by
319 change f (lift⁻¹ * s) = 1
320 rw [map_mul, map_inv]
321 have hlift : f lift = t := Function.surjInv_eq hfsurj t
322 rw [hlift]
323 simp only [inv_mul_cancel, t]⟩
324 have hsection :
325 zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
326 (zcCompletedGroupAlgebraMapStage C hC φ i
327 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
328 (CompletedGroupAlgebraQuotientInClass H C
329 (completedGroupAlgebraComapIndexInClass
330 (G := H) (H := K) C hC φ i.2)) s)) =
331 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
332 (CompletedGroupAlgebraQuotientInClass H C
333 (completedGroupAlgebraComapIndexInClass
334 (G := H) (H := K) C hC φ i.2)) lift := by
335 rw [zcCompletedGroupAlgebraMapStage_of,
336 zcCompletedGroupAlgebraMapStageTargetSection_of]
337 rw [hsection]
338 have hmul :
339 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
340 (CompletedGroupAlgebraQuotientInClass H C
341 (completedGroupAlgebraComapIndexInClass
342 (G := H) (H := K) C hC φ i.2)) lift *
343 zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator C hC φ i q =
344 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
345 (CompletedGroupAlgebraQuotientInClass H C
346 (completedGroupAlgebraComapIndexInClass
347 (G := H) (H := K) C hC φ i.2)) s -
348 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
349 (CompletedGroupAlgebraQuotientInClass H C
350 (completedGroupAlgebraComapIndexInClass
351 (G := H) (H := K) C hC φ i.2)) lift := by
352 simp only [zcCompletedGroupAlgebraMapStageRelationAugmentationGenerator, q,
353 MonoidAlgebra.of_apply]
354 rw [mul_sub, MonoidAlgebra.single_mul_single, mul_one]
355 simp only [mul_inv_cancel_left, mul_one]
356 rw [← hmul]
357 exact
358 (zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i).mul_mem_left _
359 (Ideal.subset_span ⟨q, rfl⟩)
361/--
362At a finite completed group-algebra stage, every source element minus the chosen lift of its
363target image lies in the relation augmentation ideal.
364-/
365theorem zcCompletedGAMapStage_sub_targetSection_map_mem_relationAugmentationIdeal
366 (φ : H →ₜ* K) (hφ : Function.Surjective φ)
367 (i : ZCCompletedGroupAlgebraIndex C K)
368 (x :
369 ZCCompletedGroupAlgebraStage C H
370 (i.1, completedGroupAlgebraComapIndexInClass
371 (G := H) (H := K) C hC φ i.2)) :
372 x - zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
373 (zcCompletedGroupAlgebraMapStage C hC φ i x) ∈
374 zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i := by
375 classical
376 refine MonoidAlgebra.induction_on
377 (p := fun x :
378 ZCCompletedGroupAlgebraStage C H
379 (i.1, completedGroupAlgebraComapIndexInClass
380 (G := H) (H := K) C hC φ i.2) =>
381 x - zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
382 (zcCompletedGroupAlgebraMapStage C hC φ i x) ∈
383 zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i)
384 x ?single ?add ?smul
385 · intro s
386 exact
387 zcCompletedGAMapStage_sourceBasis_sub_targetSection_mem_relationAugmentationIdeal
388 C hC φ hφ i s
389 · intro x y hx hy
390 have hcalc :
391 x + y - zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
392 (zcCompletedGroupAlgebraMapStage C hC φ i (x + y)) =
393 (x - zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
394 (zcCompletedGroupAlgebraMapStage C hC φ i x)) +
395 (y - zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
396 (zcCompletedGroupAlgebraMapStage C hC φ i y)) := by
397 rw [map_add, map_add]
398 abel
399 rw [hcalc]
400 exact
401 (zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i).add_mem hx hy
402 · intro a x hx
403 have hmap_smul :
404 zcCompletedGroupAlgebraMapStage C hC φ i (a • x) =
405 a • zcCompletedGroupAlgebraMapStage C hC φ i x :=
406 zcCompletedGroupAlgebraMapStage_smul C hC φ i a x
407 have hcalc :
408 a • x - zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
409 (zcCompletedGroupAlgebraMapStage C hC φ i (a • x)) =
410 a • (x - zcCompletedGroupAlgebraMapStageTargetSection C hC φ hφ i
411 (zcCompletedGroupAlgebraMapStage C hC φ i x)) := by
412 rw [hmap_smul, map_smul, smul_sub]
413 rw [hcalc]
414 rw [Algebra.smul_def]
415 exact
416 (zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i).mul_mem_left _ hx
418/--
419In each finite stage, the kernel of a surjective target map is exactly the relation augmentation
420ideal generated by the kernel of the finite quotient map.
421-/
422theorem zcCompletedGAMapStageKernelIdeal_eq_relationAugmentationIdeal_of_surj
423 (φ : H →ₜ* K) (hφ : Function.Surjective φ)
424 (i : ZCCompletedGroupAlgebraIndex C K) :
425 zcCompletedGroupAlgebraMapStageKernelIdeal C hC φ i =
426 zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i := by
427 apply le_antisymm
428 · intro x hx
429 have hxmap :
430 zcCompletedGroupAlgebraMapStage C hC φ i x = 0 :=
431 (mem_zcCompletedGroupAlgebraMapStageKernelIdeal_iff
432 (C := C) (hC := hC) (φ := φ) (i := i)).1 hx
433 have hdiff :=
434 zcCompletedGAMapStage_sub_targetSection_map_mem_relationAugmentationIdeal
435 C hC φ hφ i x
436 rw [hxmap, map_zero, sub_zero] at hdiff
437 exact hdiff
438 · exact zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal_le_kernelIdeal C hC φ i
440/-- Target finite-stage maps commute with the pro-\(C\) transition maps. -/
441theorem zcCompletedGroupAlgebraMapStage_compatible
442 (φ : H →ₜ* K)
443 {i j : ZCCompletedGroupAlgebraIndex C K} (hij : i ≤ j) :
444 (zcCompletedGroupAlgebraTransition C K hij).comp
445 (zcCompletedGroupAlgebraMapStage C hC φ j) =
446 (zcCompletedGroupAlgebraMapStage C hC φ i).comp
447 (zcCompletedGroupAlgebraTransition C H
448 (show
449 (i.1, completedGroupAlgebraComapIndexInClass
450 (G := H) (H := K) C hC φ i.2) ≤
451 (j.1, completedGroupAlgebraComapIndexInClass
452 (G := H) (H := K) C hC φ j.2) from
453 ⟨hij.1,
454 completedGroupAlgebraComapIndexInClass_mono
455 (G := H) (H := K) C hC φ hij.2⟩)) := by
456 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
457 letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
458 apply RingHom.ext
459 intro x
460 refine MonoidAlgebra.induction_on
461 (p := fun x =>
462 ((zcCompletedGroupAlgebraTransition C K hij).comp
463 (zcCompletedGroupAlgebraMapStage C hC φ j)) x =
464 ((zcCompletedGroupAlgebraMapStage C hC φ i).comp
465 (zcCompletedGroupAlgebraTransition C H
466 (show
467 (i.1, completedGroupAlgebraComapIndexInClass
468 (G := H) (H := K) C hC φ i.2) ≤
469 (j.1, completedGroupAlgebraComapIndexInClass
470 (G := H) (H := K) C hC φ j.2) from
471 ⟨hij.1,
472 completedGroupAlgebraComapIndexInClass_mono
473 (G := H) (H := K) C hC φ hij.2⟩))) x)
474 x ?_ ?_ ?_
475 · intro q
476 rw [RingHom.comp_apply, RingHom.comp_apply,
477 zcCompletedGroupAlgebraMapStage_of, zcCompletedGroupAlgebraTransition_of,
478 zcCompletedGroupAlgebraTransition_of]
479 change
480 MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
481 (CompletedGroupAlgebraQuotientInClass K C i.2)
482 ((OpenNormalSubgroupInClass.map
483 (C := C) (G := K)
484 (U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2)
485 (completedGroupAlgebraComapQuotientMapInClass
486 (G := H) (H := K) C hC φ j.2 q)) =
487 zcCompletedGroupAlgebraMapStage C hC φ i
488 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
489 (CompletedGroupAlgebraQuotientInClass H C
490 (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2))
491 ((OpenNormalSubgroupInClass.map
492 (C := C) (G := H)
493 (U := OrderDual.ofDual
494 (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2))
495 (V := OrderDual.ofDual
496 (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2))
497 (completedGroupAlgebraComapIndexInClass_mono
498 (G := H) (H := K) C hC φ hij.2)) q))
499 rw [zcCompletedGroupAlgebraMapStage_of]
500 exact congrArg (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
501 (CompletedGroupAlgebraQuotientInClass K C i.2))
502 (congrFun
503 (congrArg DFunLike.coe
504 (completedGroupAlgebraComapQuotientMapInClass_compatible
505 (G := H) (H := K) C hC φ hij.2)) q)
506 · intro x y hx hy
507 rw [map_add, map_add, hx, hy]
508 · intro a x hx
509 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
510 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]
511 simp only [zcCompletedGroupAlgebraTransition, modNCompletedGroupAlgebraStageCoeffMapInClass,
512 modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe, zcCompletedGroupAlgebraMapStage,
513 map_intCast,
514 RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, MonoidAlgebra.mapDomainRingHom_apply]
516/--
517The completed group-algebra map \(\mathbb{Z}_C\llbracket H\rrbracket\) \(\to\)
518\(\mathbb{Z}_C\llbracket K\rrbracket\) induced by a continuous homomorphism \(H \to K\).
519-/
520def zcCompletedGroupAlgebraMap (φ : H →ₜ* K) :
521 ZCCompletedGroupAlgebra C H →+* ZCCompletedGroupAlgebra C K where
522 toFun x := ⟨fun i =>
523 zcCompletedGroupAlgebraMapStage C hC φ i
524 (zcCompletedGroupAlgebraProjection C H
525 (i.1, completedGroupAlgebraComapIndexInClass
526 (G := H) (H := K) C hC φ i.2) x), by
527 intro i j hij
528 let hsource :
529 (i.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2) ≤
530 (j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2) :=
531 ⟨hij.1, completedGroupAlgebraComapIndexInClass_mono
532 (G := H) (H := K) C hC φ hij.2⟩
533 have hx := x.2
534 (i.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2)
535 (j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2)
536 hsource
537 have hcompat := congrFun
538 (congrArg DFunLike.coe
539 (zcCompletedGroupAlgebraMapStage_compatible C hC φ hij))
540 (zcCompletedGroupAlgebraProjection C H
541 (j.1, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ j.2) x)
542 rw [RingHom.comp_apply, RingHom.comp_apply] at hcompat
543 rw [hx] at hcompat
544 simpa using hcompat⟩
545 map_zero' := by
546 apply Subtype.ext
547 funext i
548 simp only [zcCompletedGroupAlgebraMapStage, zcCompletedGroupAlgebraProjection_zero,
549 MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_zero]
550 map_add' := by
551 intro x y
552 apply Subtype.ext
553 funext i
554 simp only [zcCompletedGroupAlgebraProjection_add, map_add]
555 map_one' := by
556 apply Subtype.ext
557 funext i
558 simp only [zcCompletedGroupAlgebraMapStage, zcCompletedGroupAlgebraProjection_one,
559 MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_one]
560 map_mul' := by
561 intro x y
562 apply Subtype.ext
563 funext i
564 simp only [zcCompletedGroupAlgebraProjection_mul, map_mul]
566/--
567The \(\mathbb{Z}_C\)-completed group-algebra projection is computed by the corresponding
568finite-stage coordinate map.
569-/
570@[simp]
571theorem zcCompletedGroupAlgebraProjection_map
572 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K)
573 (x : ZCCompletedGroupAlgebra C H) :
574 zcCompletedGroupAlgebraProjection C K i (zcCompletedGroupAlgebraMap C hC φ x) =
575 zcCompletedGroupAlgebraMapStage C hC φ i
576 (zcCompletedGroupAlgebraProjection C H
577 (i.1, completedGroupAlgebraComapIndexInClass
578 (G := H) (H := K) C hC φ i.2) x) :=
579 rfl
581/--
582Membership in the kernel of the completed target map is exactly membership in the kernel of
583every target-indexed finite stage.
584-/
585theorem mem_zcCompletedGroupAlgebraMap_ker_iff_stageKernelIdeal
586 {C : ProCGroups.FiniteGroupClass.{u}} {hC : C.Hereditary}
587 {φ : H →ₜ* K} {x : ZCCompletedGroupAlgebra C H} :
588 x ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC φ) ↔
589 ∀ i : ZCCompletedGroupAlgebraIndex C K,
590 zcCompletedGroupAlgebraProjection C H
591 (i.1, completedGroupAlgebraComapIndexInClass
592 (G := H) (H := K) C hC φ i.2) x ∈
593 zcCompletedGroupAlgebraMapStageKernelIdeal C hC φ i := by
594 constructor
595 · intro hx i
596 rw [mem_zcCompletedGroupAlgebraMapStageKernelIdeal_iff]
597 have hmap : zcCompletedGroupAlgebraMap C hC φ x = 0 :=
598 (RingHom.mem_ker).1 hx
599 have hi := congrArg (zcCompletedGroupAlgebraProjection C K i) hmap
600 simpa [zcCompletedGroupAlgebraProjection_map] using hi
601 · intro hstage
602 rw [RingHom.mem_ker]
603 apply Subtype.ext
604 funext i
605 change zcCompletedGroupAlgebraProjection C K i (zcCompletedGroupAlgebraMap C hC φ x) =
606 zcCompletedGroupAlgebraProjection C K i (0 : ZCCompletedGroupAlgebra C K)
607 rw [zcCompletedGroupAlgebraProjection_map]
608 have hi :
609 zcCompletedGroupAlgebraMapStage C hC φ i
610 (zcCompletedGroupAlgebraProjection C H
611 (i.1, completedGroupAlgebraComapIndexInClass
612 (G := H) (H := K) C hC φ i.2) x) = 0 :=
613 (mem_zcCompletedGroupAlgebraMapStageKernelIdeal_iff
614 (C := C) (hC := hC) (φ := φ) (i := i)).1 (hstage i)
615 simpa using hi
617/--
618For a surjective target map, membership in the completed kernel is equivalently membership in
619the explicit relation-augmentation ideal at every target-indexed finite stage.
620-/
621theorem mem_zcCompletedGAMap_ker_iff_stageRelationAugmentationIdeal_of_surj
622 {C : ProCGroups.FiniteGroupClass.{u}} {hC : C.Hereditary}
623 {φ : H →ₜ* K} (hφ : Function.Surjective φ)
624 {x : ZCCompletedGroupAlgebra C H} :
625 x ∈ RingHom.ker (zcCompletedGroupAlgebraMap C hC φ) ↔
626 ∀ i : ZCCompletedGroupAlgebraIndex C K,
627 zcCompletedGroupAlgebraProjection C H
628 (i.1, completedGroupAlgebraComapIndexInClass
629 (G := H) (H := K) C hC φ i.2) x ∈
630 zcCompletedGroupAlgebraMapStageRelationAugmentationIdeal C hC φ i := by
631 constructor
632 · intro hx i
633 have hi := (mem_zcCompletedGroupAlgebraMap_ker_iff_stageKernelIdeal
634 (C := C) (hC := hC) (φ := φ) (x := x)).1 hx i
635 rwa [zcCompletedGAMapStageKernelIdeal_eq_relationAugmentationIdeal_of_surj
636 C hC φ hφ i] at hi
637 · intro hstage
638 exact (mem_zcCompletedGroupAlgebraMap_ker_iff_stageKernelIdeal
639 (C := C) (hC := hC) (φ := φ) (x := x)).2
640 (fun i => by
641 rw [zcCompletedGAMapStageKernelIdeal_eq_relationAugmentationIdeal_of_surj
642 C hC φ hφ i]
643 exact hstage i)
645/--
646The completed target map sends a group-like element to the group-like element represented by its
647image under the target homomorphism.
648-/
649@[simp]
650theorem zcCompletedGroupAlgebraMap_groupLike
651 (φ : H →ₜ* K) (h : H) :
652 zcCompletedGroupAlgebraMap C hC φ (zcGroupLike C H h) =
653 zcGroupLike C K (φ h) := by
654 apply Subtype.ext
655 funext i
656 change
657 zcCompletedGroupAlgebraProjection C K i
658 (zcCompletedGroupAlgebraMap C hC φ (zcGroupLike C H h)) =
659 zcCompletedGroupAlgebraProjection C K i (zcGroupLike C K (φ h))
660 rw [zcCompletedGroupAlgebraProjection_map,
661 zcCompletedGroupAlgebraProjection_groupLike,
662 zcCompletedGroupAlgebraProjection_groupLike,
663 zcCompletedGroupAlgebraMapStage_of]
664 exact congrArg
665 (MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
666 (CompletedGroupAlgebraQuotientInClass K C i.2))
667 (completedGroupAlgebraComapQuotientMapInClass_mk
668 (G := H) (H := K) C hC φ i.2 h)
670/-- The completed target map is linear over the induced map on coefficient group algebras. -/
671@[simp]
672theorem zcCompletedGroupAlgebraMap_scalar
673 {G : Type v} [Group G] (φ : H →ₜ* K) (ψ : G →* H) (g : G) :
674 zcCompletedGroupAlgebraMap C hC φ (zcCompletedGroupAlgebraScalar C ψ g) =
675 zcCompletedGroupAlgebraScalar C (φ.toMonoidHom.comp ψ) g := by
676 simp only [zcCompletedGroupAlgebraScalar, MonoidHom.coe_comp, Function.comp_apply,
677 zcCompletedGroupAlgebraMap_groupLike, ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.coe_coe]
679/-- The completed target map is compatible with the corresponding boundary map. -/
680@[simp]
681theorem zcCompletedGroupAlgebraMap_boundary
682 {G : Type v} [Group G] (φ : H →ₜ* K) (ψ : G →* H) (g : G) :
683 zcCompletedGroupAlgebraMap C hC φ (zcCompletedGroupAlgebraBoundary C ψ g) =
684 zcCompletedGroupAlgebraBoundary C (φ.toMonoidHom.comp ψ) g := by
685 change zcCompletedGroupAlgebraMap C hC φ (zcGroupLike C H (ψ g) - 1) =
686 zcGroupLike C K (φ (ψ g)) - 1
687 simp only [map_sub, zcCompletedGroupAlgebraMap_groupLike, map_one]
689/-- A finite-stage target map preserves the finite augmentation. -/
690theorem zcCompletedGroupAlgebraMapStage_augmentation
691 (φ : H →ₜ* K) (i : ZCCompletedGroupAlgebraIndex C K) :
692 (modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus K C i.2).comp
693 (zcCompletedGroupAlgebraMapStage C hC φ i) =
694 modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C
695 (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ i.2) := by
696 letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
697 apply RingHom.ext
698 intro y
699 let U := i.2
700 let V := completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ U
701 let P := fun y =>
702 ((modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus K C U).comp
703 (zcCompletedGroupAlgebraMapStage C hC φ i)) y =
704 (modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C V) y
705 change P y
706 refine MonoidAlgebra.induction_on (p := P) y ?_ ?_ ?_
707 · intro q
708 dsimp [P]
709 rw [zcCompletedGroupAlgebraMapStage_of]
710 simp only [U, V, modNCompletedGroupAlgebraStageAugmentationInClass_of]
711 · intro a b ha hb
712 dsimp [P] at ha hb ⊢
713 rw [RingHom.map_add, map_add, ha, hb, map_add]
714 · intro a y hy
715 dsimp [P] at hy ⊢
716 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hy]
717 have hcoeff :
718 ((modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus K C U).comp
719 (zcCompletedGroupAlgebraMapStage C hC φ i))
720 (algebraMap (ModNCompletedCoeff i.1.modulus)
721 (ZCCompletedGroupAlgebraStage C H (i.1, V)) a) =
722 (modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C V)
723 (algebraMap (ModNCompletedCoeff i.1.modulus)
724 (ZCCompletedGroupAlgebraStage C H (i.1, V)) a) := by
725 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
726 simp only [modNCompletedGroupAlgebraStageAugmentationInClass,
727 zcCompletedGroupAlgebraMapStage, map_intCast, U,
728 V]
729 have hcoeff' :
730 (modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus K C U)
731 ((zcCompletedGroupAlgebraMapStage C hC φ i)
732 (algebraMap (ModNCompletedCoeff i.1.modulus)
733 (ZCCompletedGroupAlgebraStage C H (i.1, V)) a)) =
734 (modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C V)
735 (algebraMap (ModNCompletedCoeff i.1.modulus)
736 (ZCCompletedGroupAlgebraStage C H (i.1, V)) a) := by
737 simpa [RingHom.comp_apply] using hcoeff
738 rw [hcoeff', map_mul]
740/-- Completed augmentation is natural for target maps. -/
741@[simp 900]
742theorem zcCompletedGroupAlgebraAugmentation_map
744 (φ : H →ₜ* K) (x : ZCCompletedGroupAlgebra C H) :
745 zcCompletedGroupAlgebraAugmentation C K (zcCompletedGroupAlgebraMap C hC φ x) =
746 zcCompletedGroupAlgebraAugmentation C H x := by
747 ext i
748 change zcCompletedGroupAlgebraAugmentationFamily C K
749 (zcCompletedGroupAlgebraMap C hC φ x) i =
750 zcCompletedGroupAlgebraAugmentationFamily C H x i
751 let U : CompletedGroupAlgebraIndexInClass K C := zcCompletedGroupAlgebraTopIndex C K
752 let V : CompletedGroupAlgebraIndexInClass H C := zcCompletedGroupAlgebraTopIndex C H
753 have hV :
754 completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ U = V := by
755 simp only [zcCompletedGroupAlgebraTopIndex, completedGroupAlgebraComapIndexInClass_top, U, V]
756 dsimp [zcCompletedGroupAlgebraAugmentationFamily]
757 change
758 (modNCompletedGroupAlgebraStageAugmentationInClass i.modulus K C U)
759 (zcCompletedGroupAlgebraProjection C K (i, U)
760 (zcCompletedGroupAlgebraMap C hC φ x)) =
761 (modNCompletedGroupAlgebraStageAugmentationInClass i.modulus H C V)
762 (zcCompletedGroupAlgebraProjection C H (i, V) x)
763 rw [zcCompletedGroupAlgebraProjection_map]
764 cases hV
765 let y := zcCompletedGroupAlgebraProjection C H
766 (i, completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ U) x
767 change
768 (modNCompletedGroupAlgebraStageAugmentationInClass i.modulus K C U)
769 (zcCompletedGroupAlgebraMapStage C hC φ (i, U) y) =
770 (modNCompletedGroupAlgebraStageAugmentationInClass i.modulus H C
771 (completedGroupAlgebraComapIndexInClass (G := H) (H := K) C hC φ U)) y
772 exact congrFun
773 (congrArg DFunLike.coe
774 (zcCompletedGroupAlgebraMapStage_augmentation C hC φ (i, U))) y
776/--
777The target map on completed \(\mathbb{Z}_C\) group algebras induced by the identity homomorphism
778is the identity ring homomorphism.
779-/
780@[simp 900]
781theorem zcCompletedGroupAlgebraMap_id :
782 zcCompletedGroupAlgebraMap C hC (ContinuousMonoidHom.id H) =
783 RingHom.id (ZCCompletedGroupAlgebra C H) := by
784 apply RingHom.ext
785 intro x
786 apply Subtype.ext
787 funext i
788 change zcCompletedGroupAlgebraProjection C H i
789 (zcCompletedGroupAlgebraMap C hC (ContinuousMonoidHom.id H) x) =
790 zcCompletedGroupAlgebraProjection C H i x
791 rw [zcCompletedGroupAlgebraProjection_map]
792 have hfull :
793 (i.1, completedGroupAlgebraComapIndexInClass (G := H) (H := H) C hC
794 (ContinuousMonoidHom.id H) i.2) = i := by
795 cases i
796 simp only [completedGroupAlgebraComapIndexInClass_id]
797 cases hfull
798 change zcCompletedGroupAlgebraMapStage C hC (ContinuousMonoidHom.id H) i (x.1 i) =
799 x.1 i
800 refine MonoidAlgebra.induction_on
801 (p := fun y => zcCompletedGroupAlgebraMapStage C hC (ContinuousMonoidHom.id H) i y = y)
802 (x.1 i) ?_ ?_ ?_
803 · intro q
804 rcases QuotientGroup.mk'_surjective
805 ((((OrderDual.ofDual i.2).1 : OpenNormalSubgroup H) : Subgroup H)) q with
806 ⟨g, rfl⟩
807 rw [zcCompletedGroupAlgebraMapStage_of]
808 rfl
809 · intro a b ha hb
810 rw [map_add, ha, hb]
811 rfl
812 · intro a y hy
813 rcases ZMod.intCast_surjective a with ⟨t, rfl⟩
814 rw [Algebra.smul_def, RingHom.map_mul, hy]
815 simp only [zcCompletedGroupAlgebraMapStage, map_intCast]
816 rfl
818/-- Target maps on completed \(\mathbb{Z}_C\) group algebras compose functorially. -/
819@[simp 900]
820theorem zcCompletedGroupAlgebraMap_comp
821 {L : Type u} [Group L] [TopologicalSpace L] [IsTopologicalGroup L]
822 (φ : H →ₜ* K) (ψ : K →ₜ* L) :
823 zcCompletedGroupAlgebraMap C hC (ψ.comp φ) =
824 (zcCompletedGroupAlgebraMap C hC ψ).comp
825 (zcCompletedGroupAlgebraMap C hC φ) := by
826 apply RingHom.ext
827 intro x
828 apply Subtype.ext
829 funext i
830 change zcCompletedGroupAlgebraProjection C L i
831 (zcCompletedGroupAlgebraMap C hC (ψ.comp φ) x) =
832 zcCompletedGroupAlgebraProjection C L i
833 (zcCompletedGroupAlgebraMap C hC ψ (zcCompletedGroupAlgebraMap C hC φ x))
834 rw [zcCompletedGroupAlgebraProjection_map]
835 rw [zcCompletedGroupAlgebraProjection_map]
836 let j : ZCCompletedGroupAlgebraIndex C K :=
837 (i.1, completedGroupAlgebraComapIndexInClass (G := K) (H := L) C hC ψ i.2)
838 change zcCompletedGroupAlgebraMapStage C hC (ψ.comp φ) i
839 (zcCompletedGroupAlgebraProjection C H
840 (i.1, completedGroupAlgebraComapIndexInClass
841 (G := H) (H := L) C hC (ψ.comp φ) i.2) x) =
842 zcCompletedGroupAlgebraMapStage C hC ψ i
843 (zcCompletedGroupAlgebraProjection C K j
844 (zcCompletedGroupAlgebraMap C hC φ x))
845 rw [zcCompletedGroupAlgebraProjection_map]
846 have hidx :
847 (i.1, completedGroupAlgebraComapIndexInClass
848 (G := H) (H := L) C hC (ψ.comp φ) i.2) =
849 (j.1, completedGroupAlgebraComapIndexInClass
850 (G := H) (H := K) C hC φ j.2) := by
851 subst j
852 simp only [completedGroupAlgebraComapIndexInClass_comp]
853 cases hidx
854 have hstage :
855 zcCompletedGroupAlgebraMapStage C hC (ψ.comp φ) i =
856 (zcCompletedGroupAlgebraMapStage C hC ψ i).comp
857 (zcCompletedGroupAlgebraMapStage C hC φ j) := by
858 unfold zcCompletedGroupAlgebraMapStage
859 rw [← MonoidAlgebra.mapDomainRingHom_comp]
860 congr 1
861 ext q
862 refine QuotientGroup.induction_on q ?_
863 intro g
864 rfl
865 exact congrFun (congrArg DFunLike.coe hstage)
866 (zcCompletedGroupAlgebraProjection C H
867 (j.1, completedGroupAlgebraComapIndexInClass
868 (G := H) (H := K) C hC φ j.2) x)
870end CompletedGroupAlgebraMap
872section UniversalTarget
874variable (C : ProCGroups.FiniteGroupClass.{v})
876variable {G : Type u} [Group G]
877variable {H K : Type v}
878variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
879variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
881/-- The target-pushed universal differential, bundled for the source
882completed group-algebra scalar action. -/
883def zcUniversalDifferentialTargetCrossedHom
884 (ψ : G →* H) (φ : H →ₜ* K) :
885 letI : Module (ZCCompletedGroupAlgebra C H)
886 (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
887 Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
888 ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
889 (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) := by
890 letI : Module (ZCCompletedGroupAlgebra C H)
891 (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
892 Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
893 exact
894 { toFun := fun g => zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g
895 map_mul' := by
896 intro g h
897 change zcUniversalDifferential C (φ.toMonoidHom.comp ψ) (g * h) =
898 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
899 zcCompletedGroupAlgebraScalar C ψ g •
900 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h
901 rw [ScalarCrossedHom.map_mul
902 (zcUniversalDifferential C (φ.toMonoidHom.comp ψ)) g h]
903 change zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
904 zcCompletedGroupAlgebraScalar C (φ.toMonoidHom.comp ψ) g •
905 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h =
906 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g +
907 zcCompletedGroupAlgebraMap C hC φ
908 (zcCompletedGroupAlgebraScalar C ψ g) •
909 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) h
910 rw [zcCompletedGroupAlgebraMap_scalar] }
912/--
913Target functoriality for the completed universal differential module. The codomain is regarded
914as a \(\mathbb{Z}_C\llbracket H\rrbracket\)-module by restriction of scalars along the completed
915group-algebra map induced by \(\varphi : H \to K\), and the universal differential
916\(d_{\psi}(g)\) is sent to \(d_{\varphi\circ\psi}(g)\).
917-/
918def zcCompletedDifferentialModuleTargetMap
919 (ψ : G →* H) (φ : H →ₜ* K) :
920 letI : Module (ZCCompletedGroupAlgebra C H)
921 (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
922 Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
923 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
924 ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ) := by
925 letI : Module (ZCCompletedGroupAlgebra C H)
926 (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
927 Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
928 exact
929 crossedHomModuleLift
930 (A := ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ))
931 (zcCompletedGroupAlgebraScalar C ψ)
932 (zcUniversalDifferentialTargetCrossedHom C hC ψ φ)
934/--
935The universal target map on the completed differential module is determined by the target
936homomorphism at finite stages.
937-/
938@[simp 900]
939theorem zcCompletedDifferentialModuleTargetMap_universal
940 (ψ : G →* H) (φ : H →ₜ* K) (g : G) :
941 letI : Module (ZCCompletedGroupAlgebra C H)
942 (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
943 Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
944 zcCompletedDifferentialModuleTargetMap C hC ψ φ
945 (zcUniversalDifferential C ψ g) =
946 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g := by
947 letI : Module (ZCCompletedGroupAlgebra C H)
948 (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
949 Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
950 exact
951 crossedHomModuleLift_universal
952 (A := ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ))
953 (zcCompletedGroupAlgebraScalar C ψ)
954 (zcUniversalDifferentialTargetCrossedHom C hC ψ φ) g
956include hC
958/-- Completed universal zero descends along a target homomorphism. -/
959theorem zcUniversalDifferential_eq_zero_of_target
960 (ψ : G →* H) (φ : H →ₜ* K) {g : G}
961 (hg : zcUniversalDifferential C ψ g = 0) :
962 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g = 0 := by
963 letI : Module (ZCCompletedGroupAlgebra C H)
964 (ZCCompletedDifferentialModule C (φ.toMonoidHom.comp ψ)) :=
965 Module.compHom _ (zcCompletedGroupAlgebraMap C hC φ)
966 rw [← zcCompletedDifferentialModuleTargetMap_universal C hC ψ φ g, hg, map_zero]
968variable {G' : Type u} [Group G']
970/--
971Vanishing of the completed universal differential descends along a commuting source-target
972square: the relation \(\psi'\circ f = \varphi\circ\psi\) carries \(d_{\psi}(g)=0\) to
973\(d_{\psi'}(f(g))=0\).
974-/
975theorem zcUniversalDifferential_eq_zero_of_source_target
976 (ψ : G →* H) (ψ' : G' →* K) (f : G →* G') (φ : H →ₜ* K)
977 (hcomm : ψ'.comp f = φ.toMonoidHom.comp ψ) {g : G}
978 (hg : zcUniversalDifferential C ψ g = 0) :
979 zcUniversalDifferential C ψ' (f g) = 0 := by
980 have ht :
981 zcUniversalDifferential C (φ.toMonoidHom.comp ψ) g = 0 :=
982 zcUniversalDifferential_eq_zero_of_target C hC ψ φ hg
983 have hs :
984 zcUniversalDifferential C (ψ'.comp f) g = 0 := by
985 rw [hcomm]
986 exact ht
987 exact zcUniversalDifferential_eq_zero_of_source C ψ' f hs
989end UniversalTarget
991section FreeGroup
993variable (C : ProCGroups.FiniteGroupClass.{v})
995variable {X : Type u} [DecidableEq X]
996variable {H K : Type v}
997variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
998variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
1000/-- A continuous homomorphism of target groups pushes completed Fox-coordinate vectors forward. -/
1001def zcFreeFoxCoordinatesMap (φ : H →ₜ* K) :
1002 ZCFreeFoxCoordinates C (X := X) (H := H) →
1003 ZCFreeFoxCoordinates C (X := X) (H := K) :=
1004 fun a x => zcCompletedGroupAlgebraMap C hC φ (a x)
1006omit [DecidableEq X] in
1007/--
1008The target push-forward map on completed free Fox-coordinate vectors is computed coordinatewise
1009by the completed group-algebra map.
1011@[simp]
1012theorem zcFreeFoxCoordinatesMap_apply
1013 (φ : H →ₜ* K) (a : ZCFreeFoxCoordinates C (X := X) (H := H)) (x : X) :
1014 zcFreeFoxCoordinatesMap (X := X) C hC φ a x =
1015 zcCompletedGroupAlgebraMap C hC φ (a x) :=
1016 rfl
1018omit [DecidableEq X] in
1019/-- The coordinatewise target map induced by the identity homomorphism is the identity map. -/
1020@[simp]
1021theorem zcFreeFoxCoordinatesMap_id
1022 (a : ZCFreeFoxCoordinates C (X := X) (H := H)) :
1023 zcFreeFoxCoordinatesMap (X := X) C hC (ContinuousMonoidHom.id H) a = a := by
1024 funext x
1025 simp only [zcFreeFoxCoordinatesMap, zcCompletedGroupAlgebraMap_id, RingHom.id_apply]
1027omit [DecidableEq X] in
1028/-- Coordinatewise target maps on completed Fox-coordinate vectors compose functorially. -/
1029@[simp]
1030theorem zcFreeFoxCoordinatesMap_comp
1031 {L : Type v} [Group L] [TopologicalSpace L] [IsTopologicalGroup L]
1032 (φ : H →ₜ* K) (ψ : K →ₜ* L)
1033 (a : ZCFreeFoxCoordinates C (X := X) (H := H)) :
1034 zcFreeFoxCoordinatesMap (X := X) C hC (ψ.comp φ) a =
1035 zcFreeFoxCoordinatesMap (X := X) C hC ψ
1036 (zcFreeFoxCoordinatesMap (X := X) C hC φ a) := by
1037 funext x
1038 simp only [zcFreeFoxCoordinatesMap, zcCompletedGroupAlgebraMap_comp, RingHom.coe_comp,
1039 Function.comp_apply]
1041/-- Completed free-group Fox derivatives are natural under target pushforward. -/
1042theorem zcFreeGroupFoxDerivativeVector_mapTarget
1043 (ψ : FreeGroup X →* H) (φ : H →ₜ* K) (w : FreeGroup X) :
1044 zcFreeGroupFoxDerivativeVector C (φ.toMonoidHom.comp ψ) w =
1045 zcFreeFoxCoordinatesMap (X := X) C hC φ (zcFreeGroupFoxDerivativeVector C ψ w) := by
1046 let delta : ScalarCrossedHom
1047 (zcCompletedGroupAlgebraScalar C (φ.toMonoidHom.comp ψ))
1048 (ZCFreeFoxCoordinates C (X := X) (H := K)) :=
1049 { toFun := fun w =>
1050 zcFreeFoxCoordinatesMap (X := X) C hC φ
1051 (zcFreeGroupFoxDerivativeVector C ψ w)
1052 map_mul' := by
1053 intro u v
1054 funext x
1055 simp only [scalarCrossedAction_apply, zcFreeFoxCoordinatesMap_apply,
1056 ScalarCrossedHom.map_mul,
1057 zcCompletedGroupAlgebraScalar_apply, Pi.add_apply, Pi.smul_apply,
1058 smul_eq_mul, map_add, map_mul, zcCompletedGroupAlgebraMap_groupLike,
1059 ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.coe_comp,
1060 MonoidHom.coe_coe, Function.comp_apply] }
1061 have hbasis :
1062 ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : ZCCompletedGroupAlgebra C K) := by
1063 intro x
1064 change zcFreeFoxCoordinatesMap (X := X) C hC φ
1065 (zcFreeGroupFoxDerivativeVector C ψ (FreeGroup.of x)) =
1066 Pi.single x (1 : ZCCompletedGroupAlgebra C K)
1067 funext y
1068 by_cases hxy : x = y
1069 · subst y
1070 simp only [zcFreeFoxCoordinatesMap_apply, zcFreeGroupFoxDerivativeVector_of,
1071 Pi.single_eq_same, map_one,
1073 · simp only [zcFreeFoxCoordinatesMap_apply, zcFreeGroupFoxDerivativeVector_of, ne_eq, hxy,
1074 not_false_eq_true,
1075 Pi.single_eq_of_ne', map_zero]
1076 have hdelta_eq :
1077 delta = zcFreeGroupFoxDerivativeVector C (φ.toMonoidHom.comp ψ) :=
1078 zcFreeGroupFoxDerivativeVector_unique C (φ.toMonoidHom.comp ψ) delta hbasis
1079 exact congrArg
1080 (fun d : ScalarCrossedHom
1081 (zcCompletedGroupAlgebraScalar C (φ.toMonoidHom.comp ψ))
1082 (ZCFreeFoxCoordinates C (X := X) (H := K)) => d w)
1083 hdelta_eq.symm
1085/--
1086Changing the target group maps each completed Fox derivative through the completed group-algebra
1087map.
1089theorem zcFreeGroupFoxDerivative_mapTarget
1090 (ψ : FreeGroup X →* H) (φ : H →ₜ* K) (w : FreeGroup X) (x : X) :
1091 zcFreeGroupFoxDerivative C (φ.toMonoidHom.comp ψ) x w =
1092 zcCompletedGroupAlgebraMap C hC φ (zcFreeGroupFoxDerivative C ψ x w) := by
1093 have h := congrFun (zcFreeGroupFoxDerivativeVector_mapTarget C hC ψ φ w) x
1094 change
1095 zcFreeGroupFoxDerivativeVector C (φ.toMonoidHom.comp ψ) w x =
1096 zcCompletedGroupAlgebraMap C hC φ
1097 (zcFreeGroupFoxDerivativeVector C ψ w x)
1098 exact h
1100section FiniteBasis
1102variable [Fintype X]
1104omit [DecidableEq X] in
1105/-- The completed Fox boundary is natural under target maps. -/
1106theorem zcFreeGroupFoxBoundary_mapTarget
1107 (ψ : FreeGroup X →* H) (φ : H →ₜ* K)
1108 (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
1109 zcCompletedGroupAlgebraMap C hC φ (zcFreeGroupFoxBoundary C ψ v) =
1110 zcFreeGroupFoxBoundary C (φ.toMonoidHom.comp ψ)
1111 (zcFreeFoxCoordinatesMap (X := X) C hC φ v) := by
1112 simp only [zcFreeGroupFoxBoundary_apply, map_sum, map_mul, map_sub,
1113 zcCompletedGroupAlgebraMap_groupLike,
1114 map_one, ContinuousMonoidHom.coe_toMonoidHom, zcFreeFoxCoordinatesMap, MonoidHom.coe_comp,
1115 MonoidHom.coe_coe,
1116 Function.comp_apply]
1118/--
1119Target naturality carries the boundary of the completed Fox derivative vector to the boundary of
1120the mapped derivative vector.
1122theorem zcFreeGroupFoxBoundary_derivativeVector_mapTarget
1123 (ψ : FreeGroup X →* H) (φ : H →ₜ* K) (w : FreeGroup X) :
1124 zcCompletedGroupAlgebraMap C hC φ
1125 (zcFreeGroupFoxBoundary C ψ (zcFreeGroupFoxDerivativeVector C ψ w)) =
1126 zcFreeGroupFoxBoundary C (φ.toMonoidHom.comp ψ)
1127 (zcFreeGroupFoxDerivativeVector C (φ.toMonoidHom.comp ψ) w) := by
1128 rw [zcFreeGroupFoxBoundary_mapTarget, ← zcFreeGroupFoxDerivativeVector_mapTarget]
1130/--
1131The target-mapped completed Euler formula expresses the mapped boundary as the sum of mapped Fox
1132derivatives times generator boundaries.
1134theorem zcFreeGroupFoxDerivative_euler_formula_mapTarget
1135 (ψ : FreeGroup X →* H) (φ : H →ₜ* K) (w : FreeGroup X) :
1136 zcCompletedGroupAlgebraMap C hC φ (zcGroupLike C H (ψ w) - 1) =
1137 ∑ i : X,
1138 zcFreeGroupFoxDerivative C (φ.toMonoidHom.comp ψ) i w *
1139 (zcGroupLike C K ((φ.toMonoidHom.comp ψ) (FreeGroup.of i)) - 1) := by
1140 change
1141 zcCompletedGroupAlgebraMap C hC φ
1142 (zcCompletedGroupAlgebraBoundary C ψ w) = _
1143 rw [zcCompletedGroupAlgebraMap_boundary]
1144 exact zcFreeGroupFoxDerivative_fundamental_formula C (φ.toMonoidHom.comp ψ) w
1146end FiniteBasis
1148end FreeGroup
1150end
1152end FoxDifferential