Yamaguchi Lean 4 Library
Source: ProCGroups.CrowellExactSequence.Profinite.FreeExactness
ProCGroups/CrowellExactSequence/Profinite/FreeExactness/Source

Source: ProCGroups.CrowellExactSequence.Profinite.FreeExactness

1import ProCGroups.CrowellExactSequence.Profinite.ContinuousMagnus.Injectivity
2import ProCGroups.CrowellExactSequence.Profinite.Exactness
3import ProCGroups.FoxDifferential.Completed.FreeProC.FundamentalFormula
5/-!
6# Free pro-C Crowell exactness
8For a free pro-\(C\) source, this file combines continuous Magnus injectivity, the completed
9boundary calculation, and bifiltered finite-stage exactness. The resulting theorems assemble the
10presented and separated Crowell exact sequences under a surjective presentation map.
11-/
13namespace CrowellExactSequence
15noncomputable section
17open FoxDifferential
18open ProCGroups.ProC
20universe u
22variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
23variable {C : ProCGroups.FiniteGroupClass.{u}}
27/--
28For surjective \(\psi\), the presented Crowell group-algebra sequence over the pro-\(C\)
29integers is exact.
30-/
31theorem freeProC_presentedCrowellGroupAlgebraExactProCInteger_of_psi_surjective
33 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
34 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
35 (psi : ContinuousMonoidHom sourceData.carrier H)
36 (hpsi : Function.Surjective psi) :
37 Function.Exact
38 (presentedCompletedDifferentialToCompletedGroupAlgebraProCInteger
39 (G := sourceData.carrier) (H := H) C psi)
40 (zcCompletedGroupAlgebraAugmentation C H) := by
41 let family : ULift.{u} (Fin r) → sourceData.carrier :=
42 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
43 have htargetGen :
45 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
46 simpa [family] using
47 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
48 (C := C) sourceData hbasis psi hpsi
49 exact
50 exact_presentedCompletedToZC_of_boundary_family_topologicallyGenerates
51 (G := sourceData.carrier) (H := H) C
52 hForm psi family htargetGen
54/--
55For surjective \(\psi\), the separated presented Crowell group-algebra sequence over the
56pro-\(C\) integers is exact.
57-/
58theorem freeProC_presentedSeparatedCrowellGroupAlgebraExactProCInteger_of_psi_surjective
60 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
61 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
62 (psi : ContinuousMonoidHom sourceData.carrier H)
63 (hpsi : Function.Surjective psi) :
64 Function.Exact
65 (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
66 (G := sourceData.carrier) (H := H) C
67 hC.hereditary psi)
68 (zcCompletedGroupAlgebraAugmentation C H) := by
69 let family : ULift.{u} (Fin r) → sourceData.carrier :=
70 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
71 have htargetGen :
73 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
74 simpa [family] using
75 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
76 (C := C) sourceData hbasis psi hpsi
77 exact
78 exact_presentedSepToZC_of_boundary_family_topologicallyGenerates
79 (G := sourceData.carrier) (H := H) C
80 hC.hereditary
81 (hC.melnikovFormation.formation) psi family htargetGen
83/--
84The continuous Magnus hypothesis makes the separated pro-\(C\) kernel-abelianization boundary
85injective.
86-/
87theorem freeProC_profKerAbBoundaryAddZCSep_inj_of_continuousMagnus
88 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
90 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
91 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
92 (psi : ContinuousMonoidHom sourceData.carrier H)
93 (hpsi : Function.Surjective psi)
94 [T1Space
95 (ZCFreeFoxCoordinates C
96 (X := ULift.{u} (Fin r)) (H := H))] :
97 Function.Injective
98 (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
99 (G := sourceData.carrier) (H := H) C psi) := by
100 apply
101 profKerAbBoundaryAddZCSep_inj_of_kernel_le_closedCommutator
102 (G := sourceData.carrier) (H := H) C psi
103 intro n hnsep
104 let htarget :=
105 freeProCClosedGeneratedTarget_proC_of_surjective
106 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
107 apply
108 freeProC_closedGeneratedFoxVector_kernel_le_closedCommutator
109 (H := H) (C := C) hC sourceData hbasis psi hpsi htarget n
110 have hcoord_zero :
111 freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
112 (H := H) (C := C) sourceData hbasis psi htarget n.1 = 0 := by
113 have happly :=
114 congrArg
115 (freeProCChosenULift_sepCoordinateMap
116 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi) hnsep
117 rw [freeProCChosenULift_sepCoordinateMap_universal] at happly
118 calc
119 freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
120 (H := H) (C := C) sourceData hbasis psi htarget n.1 =
121 freeProCChosenULift_sepCoordinateMap
122 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi 0 := by
123 simpa [freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger,
124 htarget] using happly
125 _ = 0 :=
126 (freeProCChosenULift_sepCoordinateMap
127 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi).map_zero
128 exact hcoord_zero
130omit [C.ContainsTrivialQuotients] in
131/--
132Under closed generation and surjectivity of \(\psi\), the completed boundary kills the
133topological commutator subgroup.
134-/
135theorem freeProC_completedBoundaryKillsTopCommZC_of_closedGen_and_psi_surj
136 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
138 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
139 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
140 (psi : ContinuousMonoidHom sourceData.carrier H)
141 (hpsi : Function.Surjective psi)
142 (htarget :
143 HasOpenNormalBasisInClass C
144 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
145 (C := C)
146 (fun i : ULift.{u} (Fin r) =>
147 psi (freeProCChosenULiftFamilyOfBasisCard
148 (C := C) sourceData hbasis i)) : Subgroup
149 (ZCCompletedFoxSemidirect
150 C (ULift.{u} (Fin r)) H)))
151 (hbasis_A :
152 IsPresentedCompletedDifferentialFamilyBasisProCInteger
153 (G := sourceData.carrier) (H := H) C psi
154 (freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis)) :
155 CompletedBoundaryKillsTopologicalCommutatorProCInteger
156 (G := sourceData.carrier) (H := H) C psi := by
157 let family : ULift.{u} (Fin r) → sourceData.carrier :=
158 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
159 let hfree :=
160 freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
161 let hφconv :=
162 freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
163 (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
164 have hH : HasOpenNormalBasisInClass C H :=
165 HasOpenNormalBasisInClass.of_surjective
166 hForm
167 sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
168 have hφHconv :
170 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
171 simpa [family] using
172 freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
173 (C := C) sourceData hbasis psi.toMonoidHom
174 have hφHgen :
176 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
177 simpa [family] using
178 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
179 (C := C) sourceData hbasis psi hpsi
180 have hleft_graph_eq :
181 ∀ g : sourceData.carrier,
182 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
183 (C := C) hfree (fun i : ULift.{u} (Fin r) => psi (family i))
184 htarget hφconv g =
185 presentedCompletedDifferentialFamilyCoordinatesProCInteger
186 (G := sourceData.carrier) (H := H) C psi family hbasis_A
187 (zcUniversalDifferential C psi.toMonoidHom g) := by
188 exact
189 freeProCZCCompletedFoxDerivativeVectorViaClosedGen_eq_presentedCoordinates_zcUnivDiff
190 (G := sourceData.carrier) (H := H) C psi family hbasis_A hfree hH htarget hφconv
191 hφHconv hφHgen
192 exact
193 completedBoundaryKillsTopCommZC_of_closedGen_leftGraph
194 (G := sourceData.carrier) (H := H) C psi family hbasis_A hfree htarget hφconv
195 hleft_graph_eq
197/--
198Continuous Magnus injectivity together with the bifiltered finite-quotient calculations gives
199exactness at the separated middle term for a finite-rank free pro-\(C\) presentation.
200-/
201theorem freeProC_exactAtSepA_of_continuousMagnus_zcBifilteredAllFiniteQuotientStages
202 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
204 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
205 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
206 (psi : ContinuousMonoidHom sourceData.carrier H)
207 (hpsi : Function.Surjective psi)
208 [T1Space
209 (ZCFreeFoxCoordinates C
210 (X := ULift.{u} (Fin r)) (H := H))] :
211 Function.Exact
212 (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
213 (G := sourceData.carrier) (H := H) C psi)
214 (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
215 (G := sourceData.carrier) (H := H) C
216 hC.hereditary psi) := by
217 let family : ULift.{u} (Fin r) → sourceData.carrier :=
218 freeProCChosenULiftFamilyOfBasisCard (C := C) sourceData hbasis
219 let hfree :=
220 freeProCChosenULiftFamilyOfBasisCard_isEpimorphicallyFree (C := C) sourceData hbasis
221 let htarget :=
222 freeProCClosedGeneratedTarget_proC_of_surjective
223 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
224 let hφconv :=
225 freeProCZCFoxSemiClosedGenGenerator_convergesToOneAlongOpenSubgroups_of_finite
226 (C := C) (fun i : ULift.{u} (Fin r) => psi (family i))
227 have hH : HasOpenNormalBasisInClass C H :=
228 HasOpenNormalBasisInClass.of_surjective
229 hC.melnikovFormation.formation
230 sourceData.isEpimorphicallyFree.hasOpenNormalBasisInClass psi hpsi
231 have hφHconv :
233 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
234 simpa [family] using
235 freeProCChosenULiftFamilyOfBasisCard_image_convergesToOneAlongOpenSubgroups
236 (C := C) sourceData hbasis psi.toMonoidHom
237 have hφHgen :
239 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
240 simpa [family] using
241 freeProCChosenULiftFamilyOfBasisCard_image_generates_of_surjective
242 (C := C) sourceData hbasis psi hpsi
243 let φ : ULift.{u} (Fin r) → H := fun i => psi (family i)
244 let coords :=
245 freeProCChosenULift_sepCoordinateEquiv
246 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
247 let Dcoords : sourceData.carrier →
248 ZCFreeFoxCoordinates C
249 (X := ULift.{u} (Fin r)) (H := H) :=
250 fun g =>
251 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
252 (C := C) hfree φ htarget hφconv g
253 have hright_graph_eq :
254 freeProCZCCompletedFoxRightHomViaClosedGenerated
255 (C := C) hfree φ htarget hφconv =
256 psi.toMonoidHom := by
257 exact
258 freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom
259 (C := C) (ULift.{u} (Fin r)) H hfree hH φ htarget hφconv
260 hφHconv hφHgen psi (by intro i; rfl)
261 have hcycle_closed :
262 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ ⊆
263 ((freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
264 (C := C) φ : Subgroup
265 (ZCCompletedFoxSemidirect C
266 (ULift.{u} (Fin r)) H)) : Set
267 (ZCCompletedFoxSemidirect C
268 (ULift.{u} (Fin r)) H)) := by
269 exact
270 freeProCZCFoxBoundaryCycles_subset_closedGenTarget_of_zcBiAllStages_coeffGraphRelDeriv
271 (C := C) hC.melnikovFormation.formation
272 (X := ULift.{u} (Fin r)) (H := H) φ hH hφHgen
273 refine
274 exact_boundaryAddZC_sep_of_coord_cycle_lift
275 (G := sourceData.carrier) (H := H) C
276 hC.hereditary psi family coords ?_ Dcoords ?_ ?_
277 · rfl
278 · intro n
279 have hcoords :
280 coords.toLinearMap =
281 freeProCChosenULift_sepCoordinateMap
282 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi := by
283 rfl
284 calc
285 Dcoords n =
286 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
287 (C := C) hfree φ htarget hφconv n := rfl
288 _ =
289 freeProCChosenULift_sepCoordinateMap
290 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi
291 (zcSeparatedUniversalDifferential C psi.toMonoidHom n) := by
292 simpa [family, hfree, htarget, hφconv, φ] using
293 (freeProCChosenULift_sepCoordinateMap_universal
294 (H := H) (C := C) hC sourceData hbasis psi hpsi n).symm
295 _ = coords (zcSeparatedUniversalDifferential C psi.toMonoidHom n) := by
296 exact congrArg
297 (fun L : ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom →ₗ[
298 ZCCompletedGroupAlgebra C H]
299 ZCFreeFoxCoordinates C (X := ULift.{u} (Fin r)) (H := H) =>
300 L (zcSeparatedUniversalDifferential C psi.toMonoidHom n))
301 hcoords.symm
302 · intro v hv
303 have hboundaryMap :
304 blanchfieldLyndonFiniteFamilyMap
305 (R := ZCCompletedGroupAlgebra C H)
306 (fun i : ULift.{u} (Fin r) =>
307 presentedCompletedDifferentialBoundaryProCInteger
308 (G := sourceData.carrier) (H := H) C psi (family i)) =
309 zcFreeGroupFoxBoundary
310 C
311 (FreeGroup.lift φ) :=
312 finiteBLMap_boundaryZC_eq_zcFreeGroupFoxBoundary
313 (G := sourceData.carrier) (H := H) C psi family
314 have hvBoundary :
315 zcFreeGroupFoxBoundary C (FreeGroup.lift φ) v = 0 := by
316 simpa [hboundaryMap, φ] using hv
317 have hy :
318 ({ left := v, right := (1 : H) } :
319 ZCCompletedFoxSemidirect C
320 (ULift.{u} (Fin r)) H) ∈
321 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (C := C) φ := by
322 constructor
323 · rfl
324 · exact hvBoundary
325 have hyTarget := hcycle_closed hy
326 rcases
327 freeProCZCFoxSemiLiftViaClosedGen_exists_preimage_of_mem_closedGenTarget
328 (C := C) hfree φ htarget hφconv hyTarget with
329 ⟨g, hg⟩
330 have hleft : Dcoords g = v := by
331 have h := congrArg
332 (fun z : ZCCompletedFoxSemidirect C
333 (ULift.{u} (Fin r)) H => z.left) hg
334 change
335 (freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
336 (C := C) hfree φ htarget hφconv g).left = v
337 exact h
338 have hrightLift :
339 freeProCZCCompletedFoxRightHomViaClosedGenerated
340 (C := C) hfree φ htarget hφconv g = 1 := by
341 have h := congrArg
342 (fun z : ZCCompletedFoxSemidirect C
343 (ULift.{u} (Fin r)) H => z.right) hg
344 simpa [freeProCZCCompletedFoxRightHomViaClosedGenerated] using h
345 have hright : psi g = 1 := by
346 simpa [hright_graph_eq] using hrightLift
347 exact ⟨⟨g, hright⟩, hleft⟩
349/--
350The all-stage continuous Magnus hypothesis and surjectivity of \(\psi\) give the separated
351Crowell exact sequence over \(\mathbb{Z}_C\).
352-/
353theorem freeProC_presentedSepCrowellZC_of_continuousMagnus_zcBiAllStages_of_psi_surj
354 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
356 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
357 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
358 (psi : ContinuousMonoidHom sourceData.carrier H)
359 (hpsi : Function.Surjective psi) :
360 Function.Injective
361 (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
362 (G := sourceData.carrier) (H := H) C psi) ∧
363 Function.Exact
364 (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
365 (G := sourceData.carrier) (H := H) C psi)
366 (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
367 (G := sourceData.carrier) (H := H) C
368 hC.hereditary psi) ∧
369 Function.Exact
370 (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
371 (G := sourceData.carrier) (H := H) C
372 hC.hereditary psi)
373 (zcCompletedGroupAlgebraAugmentation C H) ∧
374 Function.Surjective
375 (zcCompletedGroupAlgebraAugmentation C H) :=
376by
377 exact
378 ⟨freeProC_profKerAbBoundaryAddZCSep_inj_of_continuousMagnus
379 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi,
380 freeProC_exactAtSepA_of_continuousMagnus_zcBifilteredAllFiniteQuotientStages
381 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi,
382 freeProC_presentedSeparatedCrowellGroupAlgebraExactProCInteger_of_psi_surjective
383 (H := H) (C := C) (hC := hC) sourceData hbasis psi hpsi,
384 zcCompletedGroupAlgebraAugmentation_surjective
385 (C := C) (H := H)⟩
387end
389end CrowellExactSequence