Source: ProCGroups.CrowellExactSequence.Profinite.BlanchfieldLyndon
1import ProCGroups.CrowellExactSequence.Profinite.FreeExactness
2import ProCGroups.FreeProC.FiniteBasis
4/-!
5# Crowell Exact Sequence / Profinite / Blanchfield Lyndon
7This module gives the completed Blanchfield--Lyndon boundary maps and exact
8sequences in canonical lifted coordinates. Concrete `Fin n` formulations are
9obtained by reindexing only at their public presentation boundary.
10-/
12namespace CrowellExactSequence
14noncomputable section
16open FoxDifferential
17open ProCGroups.ProC
19universe u
21variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
22variable {C : ProCGroups.FiniteGroupClass.{u}}
24/--
25The first pro-\(C\) Blanchfield--Lyndon boundary map reads the kernel-abelianization boundary
26in the chosen \(A_{\psi}(C)\) coordinates.
27-/
28def freeProCBlanchfieldLyndonBoundaryProCInteger
29 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
30 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
31 (psi : ContinuousMonoidHom sourceData.carrier H)
32 (hbasis_A :
33 IsPresentedCompletedDifferentialFamilyBasisProCInteger
34 (G := sourceData.carrier) (H := H) C psi
35 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis))
36 (hwell_dN :
37 CompletedBoundaryKillsTopologicalCommutatorProCInteger
38 (G := sourceData.carrier) (H := H) C psi) :
39 ProfiniteKernelAbelianizationAdd psi →
40 ULift.{u} (Fin r) → ZCCompletedGroupAlgebra C H :=
41 fun x =>
42 presentedCompletedDifferentialFamilyCoordinatesProCInteger
43 (G := sourceData.carrier) (H := H) C psi
44 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) hbasis_A
45 (profiniteKernelAbelianizationBoundaryAddProCInteger
46 (G := sourceData.carrier) (H := H) C psi hwell_dN x)
48/--
49Exactness at the \(A\)-term is equivalent to the coordinatewise Blanchfield--Lyndon exactness
50condition.
51-/
52theorem freeProC_exactAtA_iff_blanchfieldLyndonExactAtCoordinatesProCInteger
53 {sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C}
54 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
55 {psi : ContinuousMonoidHom sourceData.carrier H}
56 (hbasis_A :
57 IsPresentedCompletedDifferentialFamilyBasisProCInteger
58 (G := sourceData.carrier) (H := H) C psi
59 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis))
60 {hwell_dN :
61 CompletedBoundaryKillsTopologicalCommutatorProCInteger
62 (G := sourceData.carrier) (H := H) C psi} :
63 Function.Exact
64 (profiniteKernelAbelianizationBoundaryAddProCInteger
65 (G := sourceData.carrier) (H := H) C psi hwell_dN)
66 (presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
67 (G := sourceData.carrier) (H := H) C psi) ↔
68 Function.Exact
69 (freeProCBlanchfieldLyndonBoundaryProCInteger
70 (H := H) (C := C) sourceData hbasis psi hbasis_A hwell_dN)
71 (blanchfieldLyndonFiniteFamilyMap
72 (R := ZCCompletedGroupAlgebra C H)
73 (fun i : ULift.{u} (Fin r) =>
74 presentedCompletedDifferentialBoundaryProCInteger
75 (G := sourceData.carrier) (H := H) C psi
76 ((freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) i))) := by
77 let family : ULift.{u} (Fin r) → sourceData.carrier :=
78 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
79 let dN :=
80 profiniteKernelAbelianizationBoundaryAddProCInteger
81 (G := sourceData.carrier) (H := H) C psi hwell_dN
82 let coords :=
83 presentedCompletedDifferentialFamilyCoordinatesProCInteger
84 (G := sourceData.carrier) (H := H) C psi family hbasis_A
85 let delta :=
86 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
87 (G := sourceData.carrier) (H := H) C psi
88 let blDelta :=
89 blanchfieldLyndonFiniteFamilyMap
90 (R := ZCCompletedGroupAlgebra C H)
91 (fun i : ULift.{u} (Fin r) =>
92 presentedCompletedDifferentialBoundaryProCInteger
93 (G := sourceData.carrier) (H := H) C psi (family i))
94 have hblDelta_comp : delta.comp coords.symm.toLinearMap = blDelta := by
95 rw [presentedCompletedDifferentialFamilyCoordinatesProCInteger_symm_toLinearMap]
96 exact
97 presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger_comp_familyMap
98 (G := sourceData.carrier) (H := H) C psi family
99 have hblDelta_apply (y) : blDelta y = delta (coords.symm y) := by
100 have h := congrArg (fun f => f y) hblDelta_comp
101 change delta (coords.symm y) = blDelta y at h
102 exact h.symm
103 change
104 Function.Exact dN delta ↔
105 Function.Exact (fun x => coords (dN x)) blDelta
106 constructor
107 · intro hexact_A y
108 constructor
109 · intro hy
110 have hy_delta : delta (coords.symm y) = 0 := by
111 simpa [hblDelta_apply y] using hy
112 rcases (hexact_A (coords.symm y)).1 hy_delta with ⟨x, hx⟩
113 refine ⟨x, ?_⟩
114 calc
115 coords (dN x) = coords (coords.symm y) := congrArg coords hx
116 _ = y := coords.apply_symm_apply y
117 · rintro ⟨x, rfl⟩
118 have hker : delta (dN x) = 0 :=
119 (hexact_A (dN x)).2 ⟨x, rfl⟩
120 calc
121 blDelta (coords (dN x)) = delta (coords.symm (coords (dN x))) :=
122 hblDelta_apply (coords (dN x))
123 _ = delta (dN x) := by rw [coords.symm_apply_apply]
124 _ = 0 := hker
125 · intro hexact_BL y
126 constructor
127 · intro hy
128 have hy_bl : blDelta (coords y) = 0 := by
129 calc
130 blDelta (coords y) = delta (coords.symm (coords y)) :=
131 hblDelta_apply (coords y)
132 _ = delta y := by rw [coords.symm_apply_apply]
133 _ = 0 := hy
134 rcases (hexact_BL (coords y)).1 hy_bl with ⟨x, hx⟩
135 refine ⟨x, ?_⟩
136 apply coords.injective
137 simpa using hx
138 · rintro ⟨x, rfl⟩
139 have hbl : blDelta (coords (dN x)) = 0 :=
140 (hexact_BL (coords (dN x))).2 ⟨x, rfl⟩
141 calc
142 delta (dN x) = delta (coords.symm (coords (dN x))) := by
143 rw [coords.symm_apply_apply]
144 _ = blDelta (coords (dN x)) := by
145 rw [hblDelta_apply]
146 _ = 0 := hbl
148/--
149The separated pro-\(C\) Blanchfield--Lyndon boundary map reads the separated
150kernel-abelianization boundary in the chosen coordinates.
151-/
152def freeProCSeparatedBlanchfieldLyndonBoundaryProCInteger
153 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
156 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
157 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
158 (psi : ContinuousMonoidHom sourceData.carrier H)
159 (hpsi : Function.Surjective psi) :
160 ProfiniteKernelAbelianizationAdd psi →
161 ZCFreeFoxCoordinates C
162 (X := ULift.{u} (Fin r)) (H := H) :=
163 fun x =>
164 freeProCChosenULift_sepCoordinateEquiv
165 (H := H) (C := C) hC sourceData hbasis psi hpsi
166 (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
167 (G := sourceData.carrier) (H := H) C psi x)
169/--
170Exactness at the separated Crowell module is equivalent to Blanchfield--Lyndon exactness in
171pro-\(C\)-integer coordinates.
172-/
173theorem freeProC_exactAtSepA_iff_blanchfieldLyndonExactAtCoordinatesProCInteger
174 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
177 {sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C}
178 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
179 {psi : ContinuousMonoidHom sourceData.carrier H}
180 (hpsi : Function.Surjective psi) :
181 Function.Exact
182 (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
183 (G := sourceData.carrier) (H := H) C psi)
184 (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
185 (G := sourceData.carrier) (H := H) C
186 hC.hereditary psi) ↔
187 Function.Exact
188 (freeProCSeparatedBlanchfieldLyndonBoundaryProCInteger
189 (H := H) (C := C) hC sourceData hbasis psi hpsi)
190 (blanchfieldLyndonFiniteFamilyMap
191 (R := ZCCompletedGroupAlgebra C H)
192 (fun i : ULift.{u} (Fin r) =>
193 presentedCompletedDifferentialBoundaryProCInteger
194 (G := sourceData.carrier) (H := H) C psi
195 ((freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) i))) := by
196 let family : ULift.{u} (Fin r) → sourceData.carrier :=
197 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
198 let dN :=
199 profiniteKernelAbelianizationBoundaryAddProCIntegerSep
200 (G := sourceData.carrier) (H := H) C psi
201 let coords :=
202 freeProCChosenULift_sepCoordinateEquiv
203 (H := H) (C := C) hC sourceData hbasis psi hpsi
204 let delta :=
205 presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
206 (G := sourceData.carrier) (H := H) C
207 hC.hereditary psi
208 let blDelta :=
209 blanchfieldLyndonFiniteFamilyMap
210 (R := ZCCompletedGroupAlgebra C H)
211 (fun i : ULift.{u} (Fin r) =>
212 presentedCompletedDifferentialBoundaryProCInteger
213 (G := sourceData.carrier) (H := H) C psi (family i))
214 have hcoords_symm :
215 coords.symm.toLinearMap =
216 freeProCChosenULift_sepFamilyMap
217 (H := H) (C := C) sourceData hbasis psi := by
218 rfl
219 have hblDelta_comp : delta.comp coords.symm.toLinearMap = blDelta := by
220 rw [hcoords_symm]
221 exact
222 presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger_comp_familyMap
223 (G := sourceData.carrier) (H := H) C
224 hC.hereditary psi family
225 have hblDelta_apply (y) : blDelta y = delta (coords.symm y) := by
226 have h := congrArg (fun f => f y) hblDelta_comp
227 change delta (coords.symm y) = blDelta y at h
228 exact h.symm
229 change
230 Function.Exact dN delta ↔
231 Function.Exact (fun x => coords (dN x)) blDelta
232 constructor
233 · intro hexact_A y
234 constructor
235 · intro hy
236 have hy_delta : delta (coords.symm y) = 0 := by
237 simpa [hblDelta_apply y] using hy
238 rcases (hexact_A (coords.symm y)).1 hy_delta with ⟨x, hx⟩
239 refine ⟨x, ?_⟩
240 calc
241 coords (dN x) = coords (coords.symm y) := congrArg coords hx
242 _ = y := coords.apply_symm_apply y
243 · rintro ⟨x, rfl⟩
244 have hker : delta (dN x) = 0 :=
245 (hexact_A (dN x)).2 ⟨x, rfl⟩
246 calc
247 blDelta (coords (dN x)) = delta (coords.symm (coords (dN x))) :=
248 hblDelta_apply (coords (dN x))
249 _ = delta (dN x) := by rw [coords.symm_apply_apply]
250 _ = 0 := hker
251 · intro hexact_BL y
252 constructor
253 · intro hy
254 have hy_bl : blDelta (coords y) = 0 := by
255 calc
256 blDelta (coords y) = delta (coords.symm (coords y)) :=
257 hblDelta_apply (coords y)
258 _ = delta y := by rw [coords.symm_apply_apply]
259 _ = 0 := hy
260 rcases (hexact_BL (coords y)).1 hy_bl with ⟨x, hx⟩
261 refine ⟨x, ?_⟩
262 apply coords.injective
263 simpa using hx
264 · rintro ⟨x, rfl⟩
265 have hbl : blDelta (coords (dN x)) = 0 :=
266 (hexact_BL (coords (dN x))).2 ⟨x, rfl⟩
267 calc
268 delta (dN x) = delta (coords.symm (coords (dN x))) := by
269 rw [coords.symm_apply_apply]
270 _ = blDelta (coords (dN x)) := (hblDelta_apply (coords (dN x))).symm
271 _ = 0 := hbl
275/--
276For a surjective \(\psi\), the presented Blanchfield--Lyndon group-algebra sequence over
277\(\mathbb{Z}_C\) is exact.
278-/
279theorem freeProC_presentedBlanchfieldLyndonGAExactZC_of_psi_surj
280 (hForm : ProCGroups.FiniteGroupClass.Formation C)
281 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
282 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
283 (psi : ContinuousMonoidHom sourceData.carrier H)
284 (hpsi : Function.Surjective psi) :
285 Function.Exact
286 (blanchfieldLyndonFiniteFamilyMap
287 (R := ZCCompletedGroupAlgebra C H)
288 (fun i : Fin r =>
289 presentedCompletedDifferentialBoundaryProCInteger
290 (G := sourceData.carrier) (H := H) C psi
291 (freeProCChosenULiftFamilyOfBasisCard
292 (C := C) sourceData hbasis (ULift.up i))))
293 (zcCompletedGroupAlgebraAugmentation C H) := by
294 let family : Fin r → sourceData.carrier :=
295 fun i =>
296 freeProCChosenULiftFamilyOfBasisCard
297 (C := C) sourceData hbasis (ULift.up i)
298 have htargetGen :
300 (G := H) (Set.range (fun i : Fin r => psi (family i))) := by
301 have hgen :=
302 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
303 (C := C) sourceData hbasis psi hpsi
304 have hrange :
305 Set.range (fun i : Fin r => psi (family i)) =
306 Set.range (fun i : ULift.{u} (Fin r) =>
307 psi (freeProCChosenULiftFamilyOfBasisCard
308 (C := C) sourceData hbasis i)) := by
309 ext h
310 constructor
311 · rintro ⟨i, rfl⟩
312 exact ⟨ULift.up i, rfl⟩
313 · rintro ⟨i, rfl⟩
314 exact ⟨i.down, by cases i; rfl⟩
315 rw [hrange]
316 exact hgen
317 simpa [family] using
318 exact_blanchfieldLyndonFiniteFamilyMap_boundary_family_of_topologicallyGenerates
319 (G := sourceData.carrier) (H := H) C
320 hForm psi family htargetGen
322/--
323For a surjective \(\psi\), the separated presented Blanchfield--Lyndon group-algebra sequence
324over \(\mathbb{Z}_C\) is exact.
325-/
326theorem freeProC_presentedSepBlanchfieldLyndonGAExactZC_of_psi_surj
327 (hForm : ProCGroups.FiniteGroupClass.Formation C)
328 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
329 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
330 (psi : ContinuousMonoidHom sourceData.carrier H)
331 (hpsi : Function.Surjective psi) :
332 Function.Exact
333 (blanchfieldLyndonFiniteFamilyMap
334 (R := ZCCompletedGroupAlgebra C H)
335 (fun i : ULift.{u} (Fin r) =>
336 presentedCompletedDifferentialBoundaryProCInteger
337 (G := sourceData.carrier) (H := H) C psi
338 ((freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) i)))
339 (zcCompletedGroupAlgebraAugmentation C H) := by
340 let family : ULift.{u} (Fin r) → sourceData.carrier :=
341 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
342 have htargetGen :
344 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
345 simpa [family] using
346 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
347 (C := C) sourceData hbasis psi hpsi
348 simpa [family] using
349 exact_blanchfieldLyndonFiniteFamilyMap_boundary_family_of_topologicallyGenerates
350 (G := sourceData.carrier) (H := H) C
351 hForm psi family htargetGen
353/--
354The all-stage continuous Magnus hypothesis and surjectivity of \(\psi\) give the separated
355Blanchfield--Lyndon exact sequence over \(\mathbb{Z}_C\).
356-/
357theorem freeProC_presentedSepBLZC_of_continuousMagnus_zcBiAllStages_of_psi_surj
358 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
360 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
361 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
362 (psi : ContinuousMonoidHom sourceData.carrier H)
363 (hpsi : Function.Surjective psi) :
364 Function.Injective
365 (freeProCSeparatedBlanchfieldLyndonBoundaryProCInteger
366 (H := H) (C := C) hC sourceData hbasis psi hpsi) ∧
367 Function.Exact
368 (freeProCSeparatedBlanchfieldLyndonBoundaryProCInteger
369 (H := H) (C := C) hC sourceData hbasis psi hpsi)
370 (blanchfieldLyndonFiniteFamilyMap
371 (R := ZCCompletedGroupAlgebra C H)
372 (fun i : ULift.{u} (Fin r) =>
373 presentedCompletedDifferentialBoundaryProCInteger
374 (G := sourceData.carrier) (H := H) C psi
375 ((freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) i))) ∧
376 Function.Exact
377 (blanchfieldLyndonFiniteFamilyMap
378 (R := ZCCompletedGroupAlgebra C H)
379 (fun i : ULift.{u} (Fin r) =>
380 presentedCompletedDifferentialBoundaryProCInteger
381 (G := sourceData.carrier) (H := H) C psi
382 ((freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) i)))
383 (zcCompletedGroupAlgebraAugmentation C H) ∧
384 Function.Surjective
385 (zcCompletedGroupAlgebraAugmentation C H) :=
386by
387 let dN :=
388 profiniteKernelAbelianizationBoundaryAddProCIntegerSep
389 (G := sourceData.carrier) (H := H) C psi
390 let coords :=
391 freeProCChosenULift_sepCoordinateEquiv
392 (H := H) (C := C) hC sourceData hbasis psi hpsi
393 let blDelta :=
394 blanchfieldLyndonFiniteFamilyMap
395 (R := ZCCompletedGroupAlgebra C H)
396 (fun i : ULift.{u} (Fin r) =>
397 presentedCompletedDifferentialBoundaryProCInteger
398 (G := sourceData.carrier) (H := H) C psi
399 ((freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) i))
400 have hinj_dN :
401 Function.Injective dN :=
402 freeProC_profKerAbBoundaryAddZCSep_inj_of_continuousMagnus
403 (H := H) (C := C) hC sourceData hbasis psi hpsi
404 have hexact_A :
405 Function.Exact dN
406 (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
407 (G := sourceData.carrier) (H := H) C
408 hC.hereditary psi) :=
409 freeProC_exactAtSepA_of_continuousMagnus_zcBifilteredAllFiniteQuotientStages
410 (H := H) (C := C) hC sourceData hbasis psi hpsi
411 have hexact_BL_A :
412 Function.Exact
413 (fun x : ProfiniteKernelAbelianizationAdd psi => coords (dN x))
414 blDelta :=
415 (freeProC_exactAtSepA_iff_blanchfieldLyndonExactAtCoordinatesProCInteger
416 (H := H) (C := C) hC (sourceData := sourceData) hbasis
417 (psi := psi) hpsi).1 hexact_A
418 change
419 Function.Injective
420 (fun x : ProfiniteKernelAbelianizationAdd psi => coords (dN x)) ∧
421 Function.Exact
422 (fun x : ProfiniteKernelAbelianizationAdd psi => coords (dN x)) blDelta ∧
423 Function.Exact blDelta
424 (zcCompletedGroupAlgebraAugmentation C H) ∧
425 Function.Surjective
426 (zcCompletedGroupAlgebraAugmentation C H)
427 refine ⟨?_, hexact_BL_A, ?_, ?_⟩
428 · intro x y hxy
429 exact hinj_dN (coords.injective hxy)
430 · exact
431 freeProC_presentedSepBlanchfieldLyndonGAExactZC_of_psi_surj
432 (H := H) (C := C) hC.melnikovFormation.formation
433 sourceData hbasis psi hpsi
434 · exact
435 zcCompletedGroupAlgebraAugmentation_surjective
436 (C := C) (H := H)
438/--
439The finite-index display reindexes the separated Blanchfield--Lyndon boundary map from
440\(\mathrm{ULift}(\mathrm{Fin}\, r)\) to \(\mathrm{Fin}\, r\).
441-/
442def freeProCSeparatedBlanchfieldLyndonBoundaryFinProCInteger
443 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
445 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
446 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
447 (psi : ContinuousMonoidHom sourceData.carrier H)
448 (hpsi : Function.Surjective psi) :
449 ProfiniteKernelAbelianizationAdd psi →
450 Fin r → ZCCompletedGroupAlgebra C H :=
451 let e : Fin r ≃ ULift.{u} (Fin r) := finULiftEquiv r
452 fun x =>
453 (piReindexLinearEquiv
454 (R := ZCCompletedGroupAlgebra C H) e).symm
455 (freeProCSeparatedBlanchfieldLyndonBoundaryProCInteger
456 (H := H) (C := C) hC sourceData hbasis psi hpsi x)
458/--
459Exactness at the separated Crowell module is equivalent to finite-coordinate
460Blanchfield--Lyndon exactness over the pro-\(C\) integers.
461-/
462theorem freeProC_exactAtSepA_iff_blanchfieldLyndonExactAtFinCoordinatesProCInteger
463 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
465 {sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C}
466 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
467 {psi : ContinuousMonoidHom sourceData.carrier H}
468 (hpsi : Function.Surjective psi) :
469 Function.Exact
470 (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
471 (G := sourceData.carrier) (H := H) C psi)
472 (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
473 (G := sourceData.carrier) (H := H) C
474 hC.hereditary psi) ↔
475 Function.Exact
476 (freeProCSeparatedBlanchfieldLyndonBoundaryFinProCInteger
477 (H := H) (C := C) hC sourceData hbasis psi hpsi)
478 (blanchfieldLyndonFiniteFamilyMap
479 (R := ZCCompletedGroupAlgebra C H)
480 (fun i : Fin r =>
481 presentedCompletedDifferentialBoundaryProCInteger
482 (G := sourceData.carrier) (H := H) C psi
483 (freeProCChosenULiftFamilyOfBasisCard
484 (C := C) sourceData hbasis (ULift.up i)))) := by
485 let e : Fin r ≃ ULift.{u} (Fin r) := finULiftEquiv r
486 let L :
487 (Fin r → ZCCompletedGroupAlgebra C H) ≃ₗ[
488 ZCCompletedGroupAlgebra C H]
489 (ULift.{u} (Fin r) →
490 ZCCompletedGroupAlgebra C H) :=
491 piReindexLinearEquiv
492 (R := ZCCompletedGroupAlgebra C H) e
493 let blULift :=
494 blanchfieldLyndonFiniteFamilyMap
495 (R := ZCCompletedGroupAlgebra C H)
496 (fun i : ULift.{u} (Fin r) =>
497 presentedCompletedDifferentialBoundaryProCInteger
498 (G := sourceData.carrier) (H := H) C psi
499 ((freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) i))
500 let blFin :=
501 blanchfieldLyndonFiniteFamilyMap
502 (R := ZCCompletedGroupAlgebra C H)
503 (fun i : Fin r =>
504 presentedCompletedDifferentialBoundaryProCInteger
505 (G := sourceData.carrier) (H := H) C psi
506 (freeProCChosenULiftFamilyOfBasisCard
507 (C := C) sourceData hbasis (ULift.up i)))
508 have hblFin :
509 blFin = blULift.comp L.toLinearMap := by
510 simpa [blFin, blULift, L, e, finULiftEquiv, freeProCChosenULiftFamilyOfBasisCard] using
511 (finiteFamilyLinearMap_reindex
512 (R := ZCCompletedGroupAlgebra C H)
513 e
514 (fun i : ULift.{u} (Fin r) =>
515 presentedCompletedDifferentialBoundaryProCInteger
516 (G := sourceData.carrier) (H := H) C psi
517 ((freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis) i)))
518 have hULiftIff :=
519 freeProC_exactAtSepA_iff_blanchfieldLyndonExactAtCoordinatesProCInteger
520 (H := H) (C := C) hC (sourceData := sourceData) hbasis
521 (psi := psi) hpsi
522 have htransport :
523 Function.Exact
524 (fun x : ProfiniteKernelAbelianizationAdd psi =>
525 L.symm
526 (freeProCSeparatedBlanchfieldLyndonBoundaryProCInteger
527 (H := H) (C := C) hC sourceData hbasis psi hpsi x))
528 (fun y : Fin r → ZCCompletedGroupAlgebra C H =>
529 blULift (L y)) ↔
530 Function.Exact
531 (freeProCSeparatedBlanchfieldLyndonBoundaryProCInteger
532 (H := H) (C := C) hC sourceData hbasis psi hpsi)
533 blULift :=
534 Function.Exact.linearEquiv_symm_comp_comp_iff
535 (R := ZCCompletedGroupAlgebra C H) L
536 change
537 Function.Exact
538 (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
539 (G := sourceData.carrier) (H := H) C psi)
540 (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
541 (G := sourceData.carrier) (H := H) C
542 hC.hereditary psi) ↔
543 Function.Exact
544 (fun x : ProfiniteKernelAbelianizationAdd psi =>
545 L.symm
546 (freeProCSeparatedBlanchfieldLyndonBoundaryProCInteger
547 (H := H) (C := C) hC sourceData hbasis psi hpsi x))
548 blFin
549 rw [hblFin]
550 exact hULiftIff.trans htransport.symm
552/--
553The all-stage continuous Magnus hypothesis and surjectivity of \(\psi\) give the
554finite-coordinate separated Blanchfield--Lyndon exact sequence over \(\mathbb{Z}_C\).
555-/
556theorem freeProC_presentedSepBLFinZC_of_continuousMagnus_zcBiAllStages_of_psi_surj
557 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
559 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
560 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
561 (psi : ContinuousMonoidHom sourceData.carrier H)
562 (hpsi : Function.Surjective psi) :
563 Function.Injective
564 (freeProCSeparatedBlanchfieldLyndonBoundaryFinProCInteger
565 (H := H) (C := C) hC sourceData hbasis psi hpsi) ∧
566 Function.Exact
567 (freeProCSeparatedBlanchfieldLyndonBoundaryFinProCInteger
568 (H := H) (C := C) hC sourceData hbasis psi hpsi)
569 (blanchfieldLyndonFiniteFamilyMap
570 (R := ZCCompletedGroupAlgebra C H)
571 (fun i : Fin r =>
572 presentedCompletedDifferentialBoundaryProCInteger
573 (G := sourceData.carrier) (H := H) C psi
574 (freeProCChosenULiftFamilyOfBasisCard
575 (C := C) sourceData hbasis (ULift.up i)))) ∧
576 Function.Exact
577 (blanchfieldLyndonFiniteFamilyMap
578 (R := ZCCompletedGroupAlgebra C H)
579 (fun i : Fin r =>
580 presentedCompletedDifferentialBoundaryProCInteger
581 (G := sourceData.carrier) (H := H) C psi
582 (freeProCChosenULiftFamilyOfBasisCard
583 (C := C) sourceData hbasis (ULift.up i))))
584 (zcCompletedGroupAlgebraAugmentation C H) ∧
585 Function.Surjective
586 (zcCompletedGroupAlgebraAugmentation C H) :=
587by
588 let e : Fin r ≃ ULift.{u} (Fin r) := finULiftEquiv r
589 let L :
590 (Fin r → ZCCompletedGroupAlgebra C H) ≃ₗ[
591 ZCCompletedGroupAlgebra C H]
592 (ULift.{u} (Fin r) →
593 ZCCompletedGroupAlgebra C H) :=
594 piReindexLinearEquiv
595 (R := ZCCompletedGroupAlgebra C H) e
596 let dN :=
597 profiniteKernelAbelianizationBoundaryAddProCIntegerSep
598 (G := sourceData.carrier) (H := H) C psi
599 let coords :=
600 freeProCChosenULift_sepCoordinateEquiv
601 (H := H) (C := C) hC sourceData hbasis psi hpsi
602 have hinj_dN :
603 Function.Injective dN :=
604 freeProC_profKerAbBoundaryAddZCSep_inj_of_continuousMagnus
605 (H := H) (C := C) hC sourceData hbasis psi hpsi
606 have hexact_A :
607 Function.Exact dN
608 (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
609 (G := sourceData.carrier) (H := H) C
610 hC.hereditary psi) :=
611 freeProC_exactAtSepA_of_continuousMagnus_zcBifilteredAllFiniteQuotientStages
612 (H := H) (C := C) hC sourceData hbasis psi hpsi
613 refine ⟨?_, ?_, ?_, ?_⟩
614 · intro x y hxy
615 change L.symm (coords (dN x)) = L.symm (coords (dN y)) at hxy
616 exact hinj_dN (coords.injective (L.symm.injective hxy))
617 · exact
618 (freeProC_exactAtSepA_iff_blanchfieldLyndonExactAtFinCoordinatesProCInteger
619 (H := H) (C := C) hC (sourceData := sourceData) hbasis
620 (psi := psi) hpsi).1 hexact_A
621 · exact
622 freeProC_presentedBlanchfieldLyndonGAExactZC_of_psi_surj
623 (H := H) (C := C) hC.melnikovFormation.formation
624 sourceData hbasis psi hpsi
625 · exact
626 zcCompletedGroupAlgebraAugmentation_surjective
627 (C := C) (H := H)
629end
631end CrowellExactSequence