Yamaguchi Lean 4 Library
Source: ProCGroups.CrowellExactSequence.Profinite.SequenceMaps.Exactness
ProCGroups/CrowellExactSequence/Profinite/SequenceMaps/Exactness/Source

Source: ProCGroups.CrowellExactSequence.Profinite.SequenceMaps.Exactness

1import ProCGroups.CrowellExactSequence.Basic
2import ProCGroups.CrowellExactSequence.Profinite.SequenceMaps.Basic
3import ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Topology
4import ProCGroups.FoxDifferential.Completed.Continuous.TailExactness
6/-!
7# Exactness criteria for profinite Crowell sequence maps
9This file identifies the completed map with the boundary expressed in closed-generator
10coordinates and transfers exactness between finite-family, completed, and separated sequences.
11It gives topological-generation and basis criteria and computes the maps on kernel elements.
12-/
14namespace CrowellExactSequence
16noncomputable section
18open scoped BigOperators
19open FoxDifferential
21universe u v w
23variable {G H : Type u}
24variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
25variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
27section ClosedGeneratedCoordinates
29variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
30variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
31variable (C : ProCGroups.FiniteGroupClass.{u})
32variable (psi : ContinuousMonoidHom G H)
33variable {X : Type u} [Fintype X] [DecidableEq X]
34variable (family : X → G)
35variable
36 (hfree :
38 (C := C) X G family)
39variable
40 (htarget :
42 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
43 (C := C) (fun i : X => psi (family i)) : Subgroup
44 (ZCCompletedFoxSemidirect C X H)))
45variable
46 (hφconv :
48 (G :=
49 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
50 (C := C) (fun i : X => psi (family i)) : Subgroup
51 (ZCCompletedFoxSemidirect C X H)))
52 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
53 (C := C) (fun i : X => psi (family i))))
56/--
57On the genuine \(A_{\psi}(C)\), the Crowell boundary is obtained by first reading the
58closed-generated Fox coordinates and then applying the completed Fox boundary.
59-/
60theorem presentedCompletedToZC_eq_boundary_comp_closedGenCoords
62 (hφHconv :
64 (G := H) (fun i : X => psi (family i)))
65 (hφHgen :
67 (G := H) (Set.range (fun i : X => psi (family i)))) :
68 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
69 (G := G) (H := H) C psi =
70 (freeProCZCCompletedFoxBoundary C
71 (fun i : X => psi (family i))).comp
72 (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
73 (G := G) (H := H) C psi family hfree htarget hφconv
74 hH hφHconv hφHgen) := by
75 apply
76 crossedDifferentialModuleHom_ext
77 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
78 intro g
79 change
80 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
81 (G := G) (H := H) C psi
82 (zcUniversalDifferential C psi.toMonoidHom g) =
83 ((freeProCZCCompletedFoxBoundary C
84 (fun i : X => psi (family i))).comp
85 (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
86 (G := G) (H := H) C psi family hfree htarget hφconv
87 hH hφHconv hφHgen))
88 (zcUniversalDifferential C psi.toMonoidHom g)
89 rw [presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger_d,
90 LinearMap.comp_apply,
91 closedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal]
92 have hright :
93 freeProCZCCompletedFoxRightHomViaClosedGenerated
94 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv =
95 psi.toMonoidHom :=
96 freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom
97 (C := C) X H hfree hH (fun i : X => psi (family i)) htarget hφconv
98 hφHconv hφHgen psi (by intro i; rfl)
99 let delta : ScalarCrossedHom
100 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
101 (ZCFreeFoxCoordinates C (X := X) (H := H)) :=
102 { toFun := fun g =>
103 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
104 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g
105 map_mul' := by
106 intro a b
107 rw [← hright]
108 exact
109 ScalarCrossedHom.map_mul
110 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
111 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv)
112 a b }
113 exact
114 (freeProCZCBoundary_of_topologicalGeneration
115 C hfree.generates_range psi.toMonoidHom
116 delta
117 (by
118 change Continuous
119 (fun g : G =>
120 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
121 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g)
122 exact
123 continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
124 (C := C) X H hfree (fun i : X => psi (family i)) htarget hφconv)
125 psi.continuous_toFun
126 (by
127 intro i
128 change
129 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
130 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv
131 (family i) =
132 Pi.single i (1 : ZCCompletedGroupAlgebra C H)
133 exact
134 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_generator
135 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv i)
136 g).symm
138end ClosedGeneratedCoordinates
140variable (C : ProCGroups.FiniteGroupClass.{u})
142omit [IsTopologicalGroup G] in
143/--
144The displayed Crowell map after the family map is the finite Blanchfield--Lyndon map with
145boundary generators \(\psi(\mathrm{family}\ i)-1\).
146-/
147theorem presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger_comp_familyMap
148 (psi : ContinuousMonoidHom G H)
149 {X : Type v} [Fintype X] (family : X -> G) :
150 (presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
151 (G := G) (H := H) C psi).comp
152 (presentedCompletedDifferentialFamilyMapProCInteger
153 (G := G) (H := H) C psi family) =
154 blanchfieldLyndonFiniteFamilyMap
155 (R := ZCCompletedGroupAlgebra C H)
156 (fun i : X =>
157 presentedCompletedDifferentialBoundaryProCInteger
158 (G := G) (H := H) C psi (family i)) := by
159 classical
160 apply LinearMap.ext
161 intro x
162 rw [LinearMap.comp_apply, presentedCompletedDifferentialFamilyMapProCInteger,
163 blanchfieldLyndonFiniteFamilyMap_apply, blanchfieldLyndonFiniteFamilyMap_apply, map_sum]
164 apply Finset.sum_congr rfl
165 intro i _hi
166 rw [map_smul, presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger_d]
168omit [IsTopologicalGroup G] in
169/--
170The separated displayed Crowell map after the separated family map is the finite
171Blanchfield--Lyndon map with boundary generators \(\psi(\mathrm{family}\ i)-1\).
172-/
173theorem presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger_comp_familyMap
175 (psi : ContinuousMonoidHom G H)
176 {X : Type v} [Fintype X] (family : X -> G) :
177 (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
178 (G := G) (H := H) C hC psi).comp
179 (presentedSeparatedDifferentialFamilyMapProCInteger
180 (G := G) (H := H) C psi family) =
181 blanchfieldLyndonFiniteFamilyMap
182 (R := ZCCompletedGroupAlgebra C H)
183 (fun i : X =>
184 presentedCompletedDifferentialBoundaryProCInteger
185 (G := G) (H := H) C psi (family i)) := by
186 classical
187 apply LinearMap.ext
188 intro x
189 rw [LinearMap.comp_apply, presentedSeparatedDifferentialFamilyMapProCInteger,
190 blanchfieldLyndonFiniteFamilyMap_apply, blanchfieldLyndonFiniteFamilyMap_apply, map_sum]
191 apply Finset.sum_congr rfl
192 intro i _hi
193 rw [map_smul, presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger_d]
196omit [IsTopologicalGroup G] in
197/--
198The finite Blanchfield--Lyndon boundary attached to the displayed family is exactly the
199source-shaped completed Fox boundary for the abstract free group on that family. This removes
200one layer from the remaining density statement: a BL-coordinate cycle is the same as a vector
201killed by the completed Fox boundary \(zcFreeGroupFoxBoundary C (FreeGroup.lift (fun i \mapsto
202psi (family i)))\).
203-/
204theorem finiteBLMap_boundaryZC_eq_zcFreeGroupFoxBoundary
205 (psi : ContinuousMonoidHom G H)
206 {X : Type v} [Fintype X] (family : X -> G) :
207 blanchfieldLyndonFiniteFamilyMap
208 (R := ZCCompletedGroupAlgebra C H)
209 (fun i : X =>
210 presentedCompletedDifferentialBoundaryProCInteger
211 (G := G) (H := H) C psi (family i)) =
213 C (FreeGroup.lift (fun i : X => psi (family i))) := by
214 classical
215 apply LinearMap.ext
216 intro v
217 change
218 (∑ x : X, v x *
219 (zcGroupLike C H (psi (family x)) - 1)) =
220 ∑ x : X, v x *
221 (zcGroupLike C H
222 (FreeGroup.lift (fun i : X => psi (family i)) (FreeGroup.of x)) - 1)
223 simp only [FreeGroup.lift_apply_of]
225omit [IsTopologicalGroup G] in
226/--
227If the pushed-forward finite family topologically generates \(H\), the finite
228Blanchfield--Lyndon map is used at the completed group algebra.
229-/
230theorem exact_blanchfieldLyndonFiniteFamilyMap_boundary_family_of_topologicallyGenerates
233 (psi : ContinuousMonoidHom G H)
234 {X : Type v} [Fintype X] (family : X -> G)
235 (hgen :
237 (G := H) (Set.range (fun i : X => psi (family i)))) :
238 Function.Exact
239 (blanchfieldLyndonFiniteFamilyMap
240 (R := ZCCompletedGroupAlgebra C H)
241 (fun i : X =>
242 presentedCompletedDifferentialBoundaryProCInteger
243 (G := G) (H := H) C psi (family i)))
244 (zcCompletedGroupAlgebraAugmentation C H :
245 ZCCompletedGroupAlgebra C H -> ZCCoeff C) := by
246 classical
247 have hfoxExact :
248 Function.Exact
250 (fun i : X => zcGroupLike C H (psi (family i)) - 1) :
251 (X → ZCCompletedGroupAlgebra C H) →
252 ZCCompletedGroupAlgebra C H)
253 (zcCompletedGroupAlgebraAugmentation C H :
254 ZCCompletedGroupAlgebra C H → ZCCoeff C) :=
256 (C := C) (hForm := hForm)
257 (φ := fun i : X => psi (family i)) hgen
258 have hmap :
259 blanchfieldLyndonFiniteFamilyMap
260 (R := ZCCompletedGroupAlgebra C H)
261 (fun i : X =>
262 presentedCompletedDifferentialBoundaryProCInteger
263 (G := G) (H := H) C psi (family i)) =
265 (fun i : X => zcGroupLike C H (psi (family i)) - 1) := by
266 rw [finiteBLMap_boundaryZC_eq_zcFreeGroupFoxBoundary
267 (G := G) (H := H) C psi family]
268 apply LinearMap.ext
269 intro v
270 change
271 (∑ x : X, v x *
272 (zcGroupLike C H
273 (FreeGroup.lift (fun i : X => psi (family i)) (FreeGroup.of x)) - 1)) =
274 ∑ x : X, v x * (zcGroupLike C H (psi (family x)) - 1)
275 simp only [FreeGroup.lift_apply_of]
276 rw [hmap]
277 exact hfoxExact
279omit [IsTopologicalGroup G] in
280/--
281Exactness of the finite Blanchfield--Lyndon map implies exactness of the displayed Crowell map;
282no coordinate basis hypothesis is needed in this direction.
283-/
284theorem exact_presentedCompletedToZC_of_blanchfieldLyndonFiniteFamilyMap_boundary_family
286 (psi : ContinuousMonoidHom G H)
287 {X : Type v} [Fintype X] (family : X -> G)
288 (hbl :
289 Function.Exact
290 (blanchfieldLyndonFiniteFamilyMap
291 (R := ZCCompletedGroupAlgebra C H)
292 (fun i : X =>
293 presentedCompletedDifferentialBoundaryProCInteger
294 (G := G) (H := H) C psi (family i)))
295 (zcCompletedGroupAlgebraAugmentation C H :
296 ZCCompletedGroupAlgebra C H -> ZCCoeff C)) :
297 Function.Exact
298 (presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger (G := G) (H := H) C psi :
299 ZCCompletedDifferentialModule C psi.toMonoidHom -> ZCCompletedGroupAlgebra C H)
300 (zcCompletedGroupAlgebraAugmentation C H :
301 ZCCompletedGroupAlgebra C H -> ZCCoeff C) := by
302 classical
303 let familyMap :=
304 presentedCompletedDifferentialFamilyMapProCInteger
305 (G := G) (H := H) C psi family
306 let delta :=
307 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
308 (G := G) (H := H) C psi
309 let blDelta :=
310 blanchfieldLyndonFiniteFamilyMap
311 (R := ZCCompletedGroupAlgebra C H)
312 (fun i : X =>
313 presentedCompletedDifferentialBoundaryProCInteger
314 (G := G) (H := H) C psi (family i))
315 have hcomp : delta.comp familyMap = blDelta :=
316 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger_comp_familyMap
317 (G := G) (H := H) C psi family
318 have hdelta_family : ∀ x, delta (familyMap x) = blDelta x := by
319 intro x
320 have hx := congrArg (fun f => f x) hcomp
321 change delta (familyMap x) = blDelta x at hx
322 exact hx
323 intro z
324 constructor
325 · intro hz
326 rcases (hbl z).1 hz with ⟨x, hx⟩
327 exact ⟨familyMap x, (hdelta_family x).trans hx⟩
328 · rintro ⟨m, rfl⟩
329 have hmem :
330 delta m ∈ zcCompletedGroupAlgebraAugmentationIdeal C H := by
331 have hstd :
332 delta m ∈ zcCompletedGroupAlgebraStandardAugmentationIdeal C H := by
333 simpa [delta, presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger] using
334 zcToCompletedGroupAlgebra_mem_standardAugmentationIdeal
335 C H psi.toMonoidHom m
336 exact zcCompletedGroupAlgebraStandardAugmentationIdeal_le_augmentationIdeal C H hstd
337 exact (mem_zcCompletedGroupAlgebraAugmentationIdeal_iff
338 (C := C) (H := H) (x := delta m)).1 hmem
340omit [IsTopologicalGroup G] in
341/--
342If the pushed-forward finite family topologically generates \(H\), then the displayed Crowell
343map is used at the completed group algebra.
344-/
345theorem exact_presentedCompletedToZC_of_boundary_family_topologicallyGenerates
348 (psi : ContinuousMonoidHom G H)
349 {X : Type v} [Finite X] (family : X -> G)
350 (hgen :
352 (G := H) (Set.range (fun i : X => psi (family i)))) :
353 Function.Exact
354 (presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger (G := G) (H := H) C psi :
355 ZCCompletedDifferentialModule C psi.toMonoidHom -> ZCCompletedGroupAlgebra C H)
356 (zcCompletedGroupAlgebraAugmentation C H :
357 ZCCompletedGroupAlgebra C H -> ZCCoeff C) := by
358 classical
359 letI : Fintype X := Fintype.ofFinite X
360 exact
361 exact_presentedCompletedToZC_of_blanchfieldLyndonFiniteFamilyMap_boundary_family
362 (G := G) (H := H) C psi family
363 (exact_blanchfieldLyndonFiniteFamilyMap_boundary_family_of_topologicallyGenerates
364 (G := G) (H := H) C hForm psi family hgen)
366omit [IsTopologicalGroup G] in
367/--
368Exactness of the finite Blanchfield--Lyndon map implies exactness of the separated displayed
369Crowell map at \(\mathbb{Z}_C\llbracket H\rrbracket\).
370-/
371theorem exact_presentedSepToZC_of_blanchfieldLyndonFiniteFamilyMap_boundary_family
374 (psi : ContinuousMonoidHom G H)
375 {X : Type v} [Fintype X] (family : X -> G)
376 (hbl :
377 Function.Exact
378 (blanchfieldLyndonFiniteFamilyMap
379 (R := ZCCompletedGroupAlgebra C H)
380 (fun i : X =>
381 presentedCompletedDifferentialBoundaryProCInteger
382 (G := G) (H := H) C psi (family i)))
383 (zcCompletedGroupAlgebraAugmentation C H :
384 ZCCompletedGroupAlgebra C H -> ZCCoeff C)) :
385 Function.Exact
386 (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
387 (G := G) (H := H) C hC psi :
388 ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom ->
389 ZCCompletedGroupAlgebra C H)
390 (zcCompletedGroupAlgebraAugmentation C H :
391 ZCCompletedGroupAlgebra C H -> ZCCoeff C) := by
392 classical
393 let familyMap :=
394 presentedSeparatedDifferentialFamilyMapProCInteger
395 (G := G) (H := H) C psi family
396 let delta :=
397 presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
398 (G := G) (H := H) C hC psi
399 let blDelta :=
400 blanchfieldLyndonFiniteFamilyMap
401 (R := ZCCompletedGroupAlgebra C H)
402 (fun i : X =>
403 presentedCompletedDifferentialBoundaryProCInteger
404 (G := G) (H := H) C psi (family i))
405 have hcomp : delta.comp familyMap = blDelta :=
406 presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger_comp_familyMap
407 (G := G) (H := H) C hC psi family
408 have hdelta_family : ∀ x, delta (familyMap x) = blDelta x := by
409 intro x
410 have hx := congrArg (fun f => f x) hcomp
411 change delta (familyMap x) = blDelta x at hx
412 exact hx
413 have hcompleted :
414 Function.Exact
415 (presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
416 (G := G) (H := H) C psi :
417 ZCCompletedDifferentialModule C psi.toMonoidHom -> ZCCompletedGroupAlgebra C H)
418 (zcCompletedGroupAlgebraAugmentation C H :
419 ZCCompletedGroupAlgebra C H -> ZCCoeff C) :=
420 exact_presentedCompletedToZC_of_blanchfieldLyndonFiniteFamilyMap_boundary_family
421 (G := G) (H := H) C psi family hbl
422 have htoSep_surj :
423 Function.Surjective (zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom) := by
424 intro a
425 refine Submodule.Quotient.induction_on
426 (p := zcCompletedDifferentialRelationFiniteClosedSubmodule C psi.toMonoidHom)
427 (C := fun a =>
428 ∃ b : ZCCompletedDifferentialModule C psi.toMonoidHom,
429 zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom b = a)
430 a ?_
431 intro x
432 refine ⟨(crossedDifferentialRelationSubmodule
433 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)).mkQ x, ?_⟩
434 rfl
435 intro z
436 constructor
437 · intro hz
438 rcases (hbl z).1 hz with ⟨x, hx⟩
439 exact ⟨familyMap x, (hdelta_family x).trans hx⟩
440 · rintro ⟨m, rfl⟩
441 rcases htoSep_surj m with ⟨b, hb⟩
442 have hdelta_lift :
443 delta m =
444 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
445 (G := G) (H := H) C psi b := by
446 rw [← hb]
447 have hcomp_toSep :=
448 congrArg (fun f => f b)
449 (presentedSepToZC_comp_toSep
450 (G := G) (H := H) C hC psi)
451 change
452 delta (zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom b) =
453 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
454 (G := G) (H := H) C psi b at hcomp_toSep
455 exact hcomp_toSep
456 rw [hdelta_lift]
457 exact
458 (hcompleted
459 (presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
460 (G := G) (H := H) C psi b)).2 ⟨b, rfl⟩
462omit [IsTopologicalGroup G] in
463/--
464If the pushed-forward finite family topologically generates \(H\), then the separated displayed
465Crowell map is used at the completed group algebra.
466-/
467theorem exact_presentedSepToZC_of_boundary_family_topologicallyGenerates
471 (psi : ContinuousMonoidHom G H)
472 {X : Type v} [Finite X] (family : X -> G)
473 (hgen :
475 (G := H) (Set.range (fun i : X => psi (family i)))) :
476 Function.Exact
477 (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
478 (G := G) (H := H) C hC psi :
479 ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom ->
480 ZCCompletedGroupAlgebra C H)
481 (zcCompletedGroupAlgebraAugmentation C H :
482 ZCCompletedGroupAlgebra C H -> ZCCoeff C) := by
483 classical
484 letI : Fintype X := Fintype.ofFinite X
485 exact
486 exact_presentedSepToZC_of_blanchfieldLyndonFiniteFamilyMap_boundary_family
487 (G := G) (H := H) C hC psi family
488 (exact_blanchfieldLyndonFiniteFamilyMap_boundary_family_of_topologicallyGenerates
489 (G := G) (H := H) C hForm psi family hgen)
491omit [IsTopologicalGroup G] in
492/--
493Exactness of the displayed Crowell map implies exactness of the finite Blanchfield--Lyndon map
494as soon as the chosen family map is surjective. Full basis/injectivity is not needed for this
495implication.
496-/
497theorem exact_finiteBLMap_boundary_of_presentedToZC_of_familyMap_surj
499 (psi : ContinuousMonoidHom G H)
500 {X : Type v} [Fintype X] (family : X -> G)
501 (hbasis_A_surj :
502 Function.Surjective
503 (presentedCompletedDifferentialFamilyMapProCInteger
504 (G := G) (H := H) C psi family))
505 (hexact_CompletedGroupAlgebra :
506 Function.Exact
507 (presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger (G := G) (H := H) C psi :
508 ZCCompletedDifferentialModule C psi.toMonoidHom -> ZCCompletedGroupAlgebra C H)
509 (zcCompletedGroupAlgebraAugmentation C H :
510 ZCCompletedGroupAlgebra C H -> ZCCoeff C)) :
511 Function.Exact
512 (blanchfieldLyndonFiniteFamilyMap
513 (R := ZCCompletedGroupAlgebra C H)
514 (fun i : X =>
515 presentedCompletedDifferentialBoundaryProCInteger
516 (G := G) (H := H) C psi (family i)))
517 (zcCompletedGroupAlgebraAugmentation C H :
518 ZCCompletedGroupAlgebra C H -> ZCCoeff C) := by
519 classical
520 let familyMap :=
521 presentedCompletedDifferentialFamilyMapProCInteger
522 (G := G) (H := H) C psi family
523 let delta :=
524 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
525 (G := G) (H := H) C psi
526 let blDelta :=
527 blanchfieldLyndonFiniteFamilyMap
528 (R := ZCCompletedGroupAlgebra C H)
529 (fun i : X =>
530 presentedCompletedDifferentialBoundaryProCInteger
531 (G := G) (H := H) C psi (family i))
532 have hcomp : delta.comp familyMap = blDelta :=
533 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger_comp_familyMap
534 (G := G) (H := H) C psi family
535 have hdelta_family : ∀ x, delta (familyMap x) = blDelta x := by
536 intro x
537 have hx := congrArg (fun f => f x) hcomp
538 change delta (familyMap x) = blDelta x at hx
539 exact hx
540 intro z
541 constructor
542 · intro hz
543 rcases (hexact_CompletedGroupAlgebra z).1 hz with ⟨m, hm⟩
544 rcases hbasis_A_surj m with ⟨x, hx⟩
545 refine ⟨x, ?_⟩
546 calc
547 blDelta x = delta (familyMap x) := (hdelta_family x).symm
548 _ = delta m := by rw [hx]
549 _ = z := hm
550 · rintro ⟨x, rfl⟩
551 exact (hexact_CompletedGroupAlgebra (blDelta x)).2 ⟨familyMap x, hdelta_family x⟩
553omit [IsTopologicalGroup G] in
554/--
555A basis family identifies exactness of the displayed Crowell map with exactness of the finite
556Blanchfield--Lyndon map obtained by evaluating the displayed boundary on that family.
557-/
558theorem exact_finiteBLMap_boundary_iff_presentedToZC_of_family_basis
559 {C}
561 {psi : ContinuousMonoidHom G H}
562 {X : Type v} [Fintype X] (family : X -> G)
563 (hbasis_A :
564 IsPresentedCompletedDifferentialFamilyBasisProCInteger
565 (G := G) (H := H) C psi family) :
566 Function.Exact
567 (blanchfieldLyndonFiniteFamilyMap
568 (R := ZCCompletedGroupAlgebra C H)
569 (fun i : X =>
570 presentedCompletedDifferentialBoundaryProCInteger
571 (G := G) (H := H) C psi (family i)))
572 (zcCompletedGroupAlgebraAugmentation C H :
573 ZCCompletedGroupAlgebra C H -> ZCCoeff C) <->
574 Function.Exact
575 (presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger (G := G) (H := H) C psi :
576 ZCCompletedDifferentialModule C psi.toMonoidHom -> ZCCompletedGroupAlgebra C H)
577 (zcCompletedGroupAlgebraAugmentation C H :
578 ZCCompletedGroupAlgebra C H -> ZCCoeff C) := by
579 constructor
580 · exact
581 exact_presentedCompletedToZC_of_blanchfieldLyndonFiniteFamilyMap_boundary_family
582 (G := G) (H := H) C psi family
583 · exact
584 exact_finiteBLMap_boundary_of_presentedToZC_of_familyMap_surj
585 (G := G) (H := H) C psi family hbasis_A.2
587omit [IsTopologicalGroup G] in
588/-- If \(g \in \ker \psi\), the displayed Crowell map sends \(dg\) to zero. -/
589@[simp]
590theorem presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger_d_of_mem_ker
591 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
592 (n : psi.toMonoidHom.ker) :
593 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger (G := G) (H := H) C psi
594 (zcUniversalDifferential C psi.toMonoidHom n.1) =
595 0 := by
596 rw [presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger_d]
597 exact zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker
598 (C := C) (H := H) psi.toMonoidHom n.2
600omit [IsTopologicalGroup G] in
601/--
602If \(g \in \ker \psi\), the separated Crowell boundary sends the separated differential \(dg\)
603to zero.
604-/
605@[simp]
606theorem presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger_d_of_mem_ker
607 (C : ProCGroups.FiniteGroupClass.{u})
609 (psi : ContinuousMonoidHom G H) (n : psi.toMonoidHom.ker) :
610 presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
611 (G := G) (H := H) C hC psi
612 (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1) =
613 0 := by
614 rw [presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger_d]
615 exact zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker
616 (C := C) (H := H) psi.toMonoidHom n.2
618end
620end CrowellExactSequence