CrowellExactSequence/Profinite/FreeExactness.lean
1import CrowellExactSequence.Profinite.ContinuousMagnus.Injectivity
2import CrowellExactSequence.Profinite.SequenceMaps
3import CrowellExactSequence.Profinite.Exactness
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/CrowellExactSequence/Profinite/FreeExactness.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Free pro-C Crowell exactness over pro-C integer coefficients
16The public route is the paper sequence
18```text
19N^ab(C) -> A_psi(C) -> Z_C[[H]] -> Z_C.
20```
22This file only assembles the displayed maps. Injectivity of `d_N`, exactness at `A_psi(C)`, and
24`Z_C[[H]]` can be derived from surjectivity of `psi`.
25-/
27namespace CrowellExactSequence
29noncomputable section
31open FoxDifferential
32open ProCGroups.ProC
34universe u
36variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
37variable {ProC : ProCGroupPredicate.{u}}
39variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass]
41/-- Free pro-`C` exactness at `Z_C[[H]]`, supplied by a finite free basis and surjectivity of
42`psi`. -/
44 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
45 (sourceData : FreeProCSourceData ProC)
46 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
47 (psi : ContinuousMonoidHom sourceData.carrier H)
48 (hpsi : Function.Surjective psi) :
49 Function.Exact
51 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi)
52 (zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H) := by
53 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
54 ⟨by
55 intro Q _ hQ
56 exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
57 let family : Fin r → sourceData.carrier :=
58 freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis
59 have htargetGen :
61 (G := H) (Set.range (fun i : Fin r => psi (family i))) := by
62 simpa [family] using
64 (ProC := ProC) sourceData hbasis psi hpsi
65 exact
67 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
68 (ProCGroupPredicate.finiteQuotientFormation ProC) psi family htargetGen
70/-- Free pro-`C` exactness at `Z_C[[H]]` for the separated middle term, supplied by a finite
71free basis and surjectivity of `psi`. -/
73 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
74 [ProC.HasFiniteQuotientHereditary]
75 (sourceData : FreeProCSourceData ProC)
76 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
77 (psi : ContinuousMonoidHom sourceData.carrier H)
78 (hpsi : Function.Surjective psi) :
79 Function.Exact
81 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
82 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi)
83 (zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H) := by
84 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
85 ⟨by
86 intro Q _ hQ
87 exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
88 let family : Fin r → sourceData.carrier :=
89 freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis
90 have htargetGen :
92 (G := H) (Set.range (fun i : Fin r => psi (family i))) := by
93 simpa [family] using
95 (ProC := ProC) sourceData hbasis psi hpsi
96 exact
98 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
99 (ProCGroupPredicate.finiteQuotientHereditary ProC)
100 (ProCGroupPredicate.finiteQuotientFormation ProC) psi family htargetGen
102omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass] in
103/-- The closed subgroup generated by the completed Fox graph of a finite free pro-`C` basis is
104pro-`C`. The only target-side input is surjectivity of `psi`; it makes `H` a pro-`C` group, and
105the ambient semidirect product is then pro-`C` by the right-projection exact sequence. -/
107 [T2Space H]
108 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientMelnikovFormation]
109 [ProC.HasFiniteQuotientHereditary] [ProC.DeterminedByFiniteQuotients]
110 (sourceData : FreeProCSourceData ProC)
111 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
112 (psi : ContinuousMonoidHom sourceData.carrier H)
113 (hpsi : Function.Surjective psi) :
114 ProC
115 (G :=
117 (ProC := ProC)
118 (fun i : ULift.{u} (Fin r) =>
120 (ProC := ProC) sourceData hbasis i)) : Subgroup
122 ProC.finiteQuotientClass (ULift.{u} (Fin r)) H))) := by
123 let family : ULift.{u} (Fin r) → sourceData.carrier :=
124 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
126 ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi
128 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass (ULift.{u} (Fin r)) H) :=
129 FoxDifferential.proCGroup_zcCompletedFoxSemidirect
130 (X := ULift.{u} (Fin r)) (H := H) ProC
131 simpa [family] using
133 (ProC := ProC)
134 (fun i : ULift.{u} (Fin r) => psi (family i))
136omit [ProC.finiteQuotientClass.ContainsTrivialQuotients] in
137/-- Free pro-`C` finite-stage separation of `A_psi(C)` from the relation-reflection form of the
139reflection hypothesis. -/
141 (sourceData : FreeProCSourceData ProC)
142 (psi : ContinuousMonoidHom sourceData.carrier H)
143 (hreflect :
145 ProC.finiteQuotientClass psi.toMonoidHom) :
147 ProC.finiteQuotientClass psi.toMonoidHom :=
149 ProC.finiteQuotientClass psi.toMonoidHom
151 ProC.finiteQuotientClass psi.toMonoidHom).2 hreflect)
153omit [ProC.finiteQuotientClass.ContainsTrivialQuotients] in
154/-- Free pro-`C` Hausdorffness of the finite-stage completed topology on `A_psi(C)`, reduced to
157 (sourceData : FreeProCSourceData ProC)
158 (psi : ContinuousMonoidHom sourceData.carrier H)
159 (hreflect :
161 ProC.finiteQuotientClass psi.toMonoidHom) :
162 @T2Space
163 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
165 ProC.finiteQuotientClass psi.toMonoidHom) :=
167 ProC.finiteQuotientClass psi.toMonoidHom
169 (H := H) (ProC := ProC) sourceData psi hreflect)
171/-- Free pro-`C` finite-stage separation of `A_psi(C)`, reduced to closedness of the completed
174 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientHereditary]
175 (sourceData : FreeProCSourceData ProC)
176 (psi : ContinuousMonoidHom sourceData.carrier H)
177 (hclosed :
179 ProC.finiteQuotientClass psi.toMonoidHom) :
181 ProC.finiteQuotientClass psi.toMonoidHom := by
182 letI :
183 Nonempty
185 ProC.finiteQuotientClass psi.toMonoidHom) :=
187 (C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
188 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi
190 (C := ProC.finiteQuotientClass) inferInstance),
191 zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
192 have hdir :
193 Directed (· ≤ ·)
194 (id :
196 ProC.finiteQuotientClass psi.toMonoidHom →
198 ProC.finiteQuotientClass psi.toMonoidHom) :=
200 (C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
201 (ProCGroupPredicate.finiteQuotientFormation ProC)
202 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi
203 exact
205 (H := H) (ProC := ProC) sourceData psi
207 ProC.finiteQuotientClass psi.toMonoidHom hdir hclosed)
209/-- Free pro-`C` Hausdorffness of the finite-stage completed topology on `A_psi(C)`, reduced to
211pre-module topology. -/
213 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientHereditary]
214 (sourceData : FreeProCSourceData ProC)
215 (psi : ContinuousMonoidHom sourceData.carrier H)
216 (hclosed :
218 ProC.finiteQuotientClass psi.toMonoidHom) :
219 @T2Space
220 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
222 ProC.finiteQuotientClass psi.toMonoidHom) :=
224 ProC.finiteQuotientClass psi.toMonoidHom
226 (H := H) (ProC := ProC) sourceData psi hclosed)
228omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass] in
229/-- For a free pro-`C` source, the current finite-stage separation target is exactly the
231pre-module topology. -/
233 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientHereditary]
234 (sourceData : FreeProCSourceData ProC)
235 (psi : ContinuousMonoidHom sourceData.carrier H) :
237 ProC.finiteQuotientClass psi.toMonoidHom ↔
239 ProC.finiteQuotientClass psi.toMonoidHom := by
240 letI :
241 Nonempty
243 ProC.finiteQuotientClass psi.toMonoidHom) :=
245 (C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
246 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi
248 (C := ProC.finiteQuotientClass) inferInstance),
249 zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
250 have hdir :
251 Directed (· ≤ ·)
252 (id :
254 ProC.finiteQuotientClass psi.toMonoidHom →
256 ProC.finiteQuotientClass psi.toMonoidHom) :=
258 (C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
259 (ProCGroupPredicate.finiteQuotientFormation ProC)
260 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi
261 exact
263 ProC.finiteQuotientClass psi.toMonoidHom hdir
265omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass] in
266/-- For a free pro-`C` source, closedness of the completed crossed-differential relation
268module `A_psi(C)`.
270This is the free-source formulation of the separation frontier: proving `A_psi(C)` is separated
272submodule closedness. -/
274 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientHereditary]
275 (sourceData : FreeProCSourceData ProC)
276 (psi : ContinuousMonoidHom sourceData.carrier H) :
278 ProC.finiteQuotientClass psi.toMonoidHom ↔
279 @T2Space
280 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
282 ProC.finiteQuotientClass psi.toMonoidHom) := by
283 letI :
284 Nonempty
286 ProC.finiteQuotientClass psi.toMonoidHom) :=
288 (C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
289 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi
291 (C := ProC.finiteQuotientClass) inferInstance),
292 zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
293 have hdir :
294 Directed (· ≤ ·)
295 (id :
297 ProC.finiteQuotientClass psi.toMonoidHom →
299 ProC.finiteQuotientClass psi.toMonoidHom) :=
301 (C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
302 (ProCGroupPredicate.finiteQuotientFormation ProC)
303 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi
304 exact
306 ProC.finiteQuotientClass psi.toMonoidHom hdir
308omit [ProC.finiteQuotientClass.ContainsTrivialQuotients] in
309/-- The closed-generated module expansion used in the free finite-basis route is continuous for
312 [T2Space H]
313 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
314 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
315 [ProC.DeterminedByFiniteQuotients]
316 (sourceData : FreeProCSourceData ProC)
317 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
318 (psi : ContinuousMonoidHom sourceData.carrier H)
319 (hpsi : Function.Surjective psi) :
320 @Continuous sourceData.carrier
321 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
322 inferInstance
324 ProC.finiteQuotientClass psi.toMonoidHom)
325 (fun g : sourceData.carrier =>
327 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
328 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
330 (ProC := ProC)
331 (freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
332 (fun i : ULift.{u} (Fin r) =>
334 (ProC := ProC) sourceData hbasis i))
336 (H := H) (ProC := ProC) sourceData hbasis psi hpsi)
338 (ProC := ProC)
339 (fun i : ULift.{u} (Fin r) =>
341 (ProC := ProC) sourceData hbasis i)))
342 g)) := by
343 let family : ULift.{u} (Fin r) → sourceData.carrier :=
344 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
345 let hfree :=
346 freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
347 let htarget :=
349 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
350 let hφconv :=
352 (ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
353 simpa [family, hfree, htarget, hφconv] using
355 (G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconv
357/-- The closed-generated coordinate map for the chosen finite free pro-`C` basis. -/
359 [T2Space H]
360 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
361 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
362 [ProC.DeterminedByFiniteQuotients]
363 (sourceData : FreeProCSourceData ProC)
364 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
365 (psi : ContinuousMonoidHom sourceData.carrier H)
366 (hpsi : Function.Surjective psi) :
367 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom →ₗ[
368 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
369 ZCFreeFoxCoordinates ProC.finiteQuotientClass
370 (X := ULift.{u} (Fin r)) (H := H) := by
371 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
372 ⟨by
373 intro Q _ hQ
374 exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
375 let family : ULift.{u} (Fin r) → sourceData.carrier :=
376 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
377 let hfree :=
378 freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
379 let htarget :=
381 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
382 let hφconv :=
384 (ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
385 have hH : ProC (G := H) :=
387 have hφHconv :
388 ProCGroups.FreeProC.FamilyConvergesToOne
389 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
390 simpa [family] using
392 (ProC := ProC) sourceData hbasis psi.toMonoidHom
393 have hφHgen :
395 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
396 simpa [family] using
398 (ProC := ProC) sourceData hbasis psi hpsi
399 exact
401 (G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconv
402 hH hφHconv hφHgen
404/-- The separated finite-family map for the chosen finite free pro-`C` basis. -/
406 (sourceData : FreeProCSourceData ProC)
407 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
408 (psi : ContinuousMonoidHom sourceData.carrier H) :
409 ZCFreeFoxCoordinates ProC.finiteQuotientClass
410 (X := ULift.{u} (Fin r)) (H := H) →ₗ[
411 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
413 ProC.finiteQuotientClass psi.toMonoidHom :=
415 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
416 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
418omit [ProC.finiteQuotientClass.ContainsTrivialQuotients] in
419/-- On a basis vector, the separated finite-family map is the separated universal
420differential of the corresponding chosen free generator. -/
421@[simp 900]
423 (sourceData : FreeProCSourceData ProC)
424 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
425 (psi : ContinuousMonoidHom sourceData.carrier H)
426 (i : ULift.{u} (Fin r)) :
428 (H := H) (ProC := ProC) sourceData hbasis psi
429 (Pi.single i (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) =
431 ProC.finiteQuotientClass psi.toMonoidHom
432 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i) := by
433 exact
435 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
436 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) i
438/-- The separated closed-generated coordinate map for the chosen finite free pro-`C` basis. -/
440 [T2Space H]
441 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
442 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
443 [ProC.DeterminedByFiniteQuotients]
444 (sourceData : FreeProCSourceData ProC)
445 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
446 (psi : ContinuousMonoidHom sourceData.carrier H)
447 (hpsi : Function.Surjective psi)
448 [T1Space
449 (ZCFreeFoxCoordinates ProC.finiteQuotientClass
450 (X := ULift.{u} (Fin r)) (H := H))] :
452 ProC.finiteQuotientClass psi.toMonoidHom →ₗ[
453 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
454 ZCFreeFoxCoordinates ProC.finiteQuotientClass
455 (X := ULift.{u} (Fin r)) (H := H) := by
456 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
457 ⟨by
458 intro Q _ hQ
459 exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
460 letI :
461 Nonempty
463 ProC.finiteQuotientClass psi.toMonoidHom) :=
465 (C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
466 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi
468 (C := ProC.finiteQuotientClass) inferInstance),
469 zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
470 have hdir :
471 Directed (· ≤ ·)
472 (id :
474 ProC.finiteQuotientClass psi.toMonoidHom →
476 ProC.finiteQuotientClass psi.toMonoidHom) :=
478 (C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
479 (ProCGroupPredicate.finiteQuotientFormation ProC)
480 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi
481 let family : ULift.{u} (Fin r) → sourceData.carrier :=
482 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
483 let hfree :=
484 freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
485 let htarget :=
487 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
488 let hφconv :=
490 (ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
491 have hH : ProC (G := H) :=
493 have hφHconv :
494 ProCGroups.FreeProC.FamilyConvergesToOne
495 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
496 simpa [family] using
498 (ProC := ProC) sourceData hbasis psi.toMonoidHom
499 have hφHgen :
501 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
502 simpa [family] using
504 (ProC := ProC) sourceData hbasis psi hpsi
505 exact
507 (G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconv
508 hdir sourceData.proCGroup.isProCGroup hH hφHconv hφHgen
510/-- The separated coordinate map sends the separated universal differential to
511the closed-generated Fox derivative vector. -/
512@[simp 900]
514 [T2Space H]
515 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
516 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
517 [ProC.DeterminedByFiniteQuotients]
518 (sourceData : FreeProCSourceData ProC)
519 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
520 (psi : ContinuousMonoidHom sourceData.carrier H)
521 (hpsi : Function.Surjective psi)
522 [T1Space
523 (ZCFreeFoxCoordinates ProC.finiteQuotientClass
524 (X := ULift.{u} (Fin r)) (H := H))]
525 (g : sourceData.carrier) :
527 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
529 ProC.finiteQuotientClass psi.toMonoidHom g) =
531 (ProC := ProC)
532 (freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
533 (fun i : ULift.{u} (Fin r) =>
534 psi (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i))
536 (H := H) (ProC := ProC) sourceData hbasis psi hpsi)
538 (ProC := ProC)
539 (fun i : ULift.{u} (Fin r) =>
540 psi (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis i)))
541 g := by
542 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
543 ⟨by
544 intro Q _ hQ
545 exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
546 letI :
547 Nonempty
549 ProC.finiteQuotientClass psi.toMonoidHom) :=
551 (C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
552 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi
554 (C := ProC.finiteQuotientClass) inferInstance),
555 zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
556 have hdir :
557 Directed (· ≤ ·)
558 (id :
560 ProC.finiteQuotientClass psi.toMonoidHom →
562 ProC.finiteQuotientClass psi.toMonoidHom) :=
564 (C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
565 (ProCGroupPredicate.finiteQuotientFormation ProC)
566 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi
567 let family : ULift.{u} (Fin r) → sourceData.carrier :=
568 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
569 let hfree :=
570 freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
571 let htarget :=
573 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
574 let hφconv :=
576 (ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
577 have hH : ProC (G := H) :=
579 have hφHconv :
580 ProCGroups.FreeProC.FamilyConvergesToOne
581 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
582 simpa [family] using
584 (ProC := ProC) sourceData hbasis psi.toMonoidHom
585 have hφHgen :
587 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
588 simpa [family] using
590 (ProC := ProC) sourceData hbasis psi hpsi
591 simpa [freeProCChosenULift_sepCoordinateMap, family, hfree, htarget, hφconv] using
593 (G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconv
594 hdir sourceData.proCGroup.isProCGroup hH hφHconv hφHgen g
596/-- The separated coordinate equivalence for the chosen finite free pro-`C` basis. -/
598 [T2Space H]
599 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
600 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
601 [ProC.DeterminedByFiniteQuotients]
602 (sourceData : FreeProCSourceData ProC)
603 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
604 (psi : ContinuousMonoidHom sourceData.carrier H)
605 (hpsi : Function.Surjective psi)
606 [T1Space
607 (ZCFreeFoxCoordinates ProC.finiteQuotientClass
608 (X := ULift.{u} (Fin r)) (H := H))] :
610 ProC.finiteQuotientClass psi.toMonoidHom ≃ₗ[
611 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
612 ZCFreeFoxCoordinates ProC.finiteQuotientClass
613 (X := ULift.{u} (Fin r)) (H := H) := by
614 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
615 ⟨by
616 intro Q _ hQ
617 exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
618 letI :
619 Nonempty
621 ProC.finiteQuotientClass psi.toMonoidHom) :=
623 (C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
624 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi
626 (C := ProC.finiteQuotientClass) inferInstance),
627 zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
628 have hdir :
629 Directed (· ≤ ·)
630 (id :
632 ProC.finiteQuotientClass psi.toMonoidHom →
634 ProC.finiteQuotientClass psi.toMonoidHom) :=
636 (C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
637 (ProCGroupPredicate.finiteQuotientFormation ProC)
638 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi
639 let family : ULift.{u} (Fin r) → sourceData.carrier :=
640 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
641 let hfree :=
642 freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
643 let htarget :=
645 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
646 let hφconv :=
648 (ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
649 have hH : ProC (G := H) :=
651 have hφHconv :
652 ProCGroups.FreeProC.FamilyConvergesToOne
653 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
654 simpa [family] using
656 (ProC := ProC) sourceData hbasis psi.toMonoidHom
657 have hφHgen :
659 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
660 simpa [family] using
662 (ProC := ProC) sourceData hbasis psi hpsi
663 exact
665 (G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconv
666 hdir sourceData.proCGroup.isProCGroup hH hφHconv hφHgen
668/-- Continuous Magnus injectivity for the separated boundary
669`d_N^sep : N^ab(C) -> A_psi(C)_sep`.
672or separate well-definedness hypothesis for `d_N` is needed. -/
674 [T2Space H]
675 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
676 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
677 [ProC.DeterminedByFiniteQuotients]
678 (sourceData : FreeProCSourceData ProC)
679 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
680 (psi : ContinuousMonoidHom sourceData.carrier H)
681 (hpsi : Function.Surjective psi)
682 [T1Space
683 (ZCFreeFoxCoordinates ProC.finiteQuotientClass
684 (X := ULift.{u} (Fin r)) (H := H))] :
685 Function.Injective
687 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi) := by
688 apply
690 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
691 intro n hnsep
692 let htarget :=
694 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
695 apply
697 (H := H) (ProC := ProC) sourceData hbasis psi hpsi htarget n
698 have hcoord_zero :
700 (H := H) (ProC := ProC) sourceData hbasis psi htarget n.1 = 0 := by
701 have happly :=
702 congrArg
704 (H := H) (ProC := ProC) sourceData hbasis psi hpsi) hnsep
705 rw [freeProCChosenULift_sepCoordinateMap_universal] at happly
706 simpa [freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger, htarget] using happly
707 exact hcoord_zero
709omit [ProC.finiteQuotientClass.ContainsTrivialQuotients] in
710/-- Closed-generated fundamental formula for the chosen finite free pro-`C` basis after applying
715algebraic module `A_psi(C)`. -/
717 [T2Space H]
718 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
719 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
720 [ProC.DeterminedByFiniteQuotients]
721 (sourceData : FreeProCSourceData ProC)
722 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
723 (psi : ContinuousMonoidHom sourceData.carrier H)
724 (hpsi : Function.Surjective psi)
726 ProC.finiteQuotientClass psi.toMonoidHom)
727 (g : sourceData.carrier) :
729 ProC.finiteQuotientClass psi.toMonoidHom i
731 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
732 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
734 (ProC := ProC)
735 (freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
736 (fun i : ULift.{u} (Fin r) =>
738 (ProC := ProC) sourceData hbasis i))
740 (H := H) (ProC := ProC) sourceData hbasis psi hpsi)
742 (ProC := ProC)
743 (fun i : ULift.{u} (Fin r) =>
745 (ProC := ProC) sourceData hbasis i)))
746 g)) =
748 ProC.finiteQuotientClass psi.toMonoidHom i
749 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) := by
750 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
751 ⟨by
752 intro Q _ hQ
753 exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
754 let family : ULift.{u} (Fin r) → sourceData.carrier :=
755 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
756 let hfree :=
757 freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
758 let htarget :=
760 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
761 let hφconv :=
763 (ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
764 have hH : ProC (G := H) :=
766 have hφHconv :
767 ProCGroups.FreeProC.FamilyConvergesToOne
768 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
769 simpa [family] using
771 (ProC := ProC) sourceData hbasis psi.toMonoidHom
772 have hφHgen :
774 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
775 simpa [family] using
777 (ProC := ProC) sourceData hbasis psi hpsi
778 simpa [family, hfree, htarget, hφconv] using
780 (G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconv
781 hH hφHconv hφHgen i g
783omit [ProC.finiteQuotientClass.ContainsTrivialQuotients] in
784/-- Closed-generated fundamental formula for the chosen finite free pro-`C` basis, with all
789 [T2Space H]
790 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
791 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
792 [ProC.DeterminedByFiniteQuotients]
793 (sourceData : FreeProCSourceData ProC)
794 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
795 (psi : ContinuousMonoidHom sourceData.carrier H)
796 (hpsi : Function.Surjective psi)
797 (hsep :
799 ProC.finiteQuotientClass psi.toMonoidHom) :
800 ∀ g : sourceData.carrier,
802 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
803 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
805 (ProC := ProC)
806 (freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
807 (fun i : ULift.{u} (Fin r) =>
809 (ProC := ProC) sourceData hbasis i))
811 (H := H) (ProC := ProC) sourceData hbasis psi hpsi)
813 (ProC := ProC)
814 (fun i : ULift.{u} (Fin r) =>
816 (ProC := ProC) sourceData hbasis i)))
817 g) =
818 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g := by
819 let family : ULift.{u} (Fin r) → sourceData.carrier :=
820 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
821 let hfree :=
822 freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
823 let htarget :=
825 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
826 let hφconv :=
828 (ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
829 have hH : ProC (G := H) :=
831 have hφHconv :
832 ProCGroups.FreeProC.FamilyConvergesToOne
833 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
834 simpa [family] using
836 (ProC := ProC) sourceData hbasis psi.toMonoidHom
837 have hφHgen :
839 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
840 simpa [family] using
842 (ProC := ProC) sourceData hbasis psi hpsi
843 simpa [family, hfree, htarget, hφconv] using
845 (G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconv
846 hsep hH hφHconv hφHgen
848/-- Closed-generated fundamental formula for the chosen finite free pro-`C` basis, reduced to
849closedness of the completed crossed-differential relation submodule.
851This is a conditional route theorem: the remaining mathematical content is the closedness
854 [T2Space H]
855 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
856 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
857 [ProC.DeterminedByFiniteQuotients]
858 (sourceData : FreeProCSourceData ProC)
859 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
860 (psi : ContinuousMonoidHom sourceData.carrier H)
861 (hpsi : Function.Surjective psi)
862 (hclosed :
864 ProC.finiteQuotientClass psi.toMonoidHom) :
865 ∀ g : sourceData.carrier,
867 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
868 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
870 (ProC := ProC)
871 (freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
872 (fun i : ULift.{u} (Fin r) =>
874 (ProC := ProC) sourceData hbasis i))
876 (H := H) (ProC := ProC) sourceData hbasis psi hpsi)
878 (ProC := ProC)
879 (fun i : ULift.{u} (Fin r) =>
881 (ProC := ProC) sourceData hbasis i)))
882 g) =
883 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g := by
884 exact
886 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
888 (H := H) (ProC := ProC) sourceData psi hclosed)
890omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass] in
891/-- Free pro-`C` closedness of the completed crossed-differential relation submodule from a
892non-circular closed-generated fundamental formula.
895pro-`C` source structure of `sourceData.carrier`; hence this theorem isolates the remaining paper
896input as exactly the module-valued fundamental formula in the algebraic `A_psi(C)`. -/
898 [T2Space H]
899 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
900 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
901 [ProC.DeterminedByFiniteQuotients]
902 (sourceData : FreeProCSourceData ProC)
903 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
904 (psi : ContinuousMonoidHom sourceData.carrier H)
905 (hpsi : Function.Surjective psi)
906 (hfundamental :
907 let htarget :=
909 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
910 ∀ g : sourceData.carrier,
912 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
913 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
915 (ProC := ProC)
916 (freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
917 (fun i : ULift.{u} (Fin r) =>
919 (ProC := ProC) sourceData hbasis i))
920 htarget
922 (ProC := ProC)
923 (fun i : ULift.{u} (Fin r) =>
925 (ProC := ProC) sourceData hbasis i)))
926 g) =
927 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
929 ProC.finiteQuotientClass psi.toMonoidHom := by
930 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
931 ⟨by
932 intro Q _ hQ
933 exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
934 let family : ULift.{u} (Fin r) → sourceData.carrier :=
935 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
936 let hfree :=
937 freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
938 let htarget :=
940 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
941 let hφconv :=
943 (ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
945 ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi
946 have hH : ProC (G := H) :=
947 hHProCGroup.isProC
948 have hφHconv :
949 ProCGroups.FreeProC.FamilyConvergesToOne
950 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
951 simpa [family] using
953 (ProC := ProC) sourceData hbasis psi.toMonoidHom
954 have hφHgen :
956 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
957 simpa [family] using
959 (ProC := ProC) sourceData hbasis psi hpsi
960 exact
962 (G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconv
963 sourceData.proCGroup.isProCGroup hH hφHconv hφHgen
964 (by simpa [family, hfree, htarget, hφconv] using hfundamental)
966/-- For the chosen finite free pro-`C` basis, relation-submodule closedness is exactly
967injectivity of the closed-generated coordinate map.
969This is the free-source form of Morishita's coordinate theorem before the final augmentation-ideal
970or relation-reflection argument: after this point the only missing theorem is the unconditional
971injectivity of this coordinate map. -/
972-- Do not derive coordinate injectivity from the fundamental formula; both are downstream of closedness.
974 [T2Space H]
975 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
976 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
977 [ProC.DeterminedByFiniteQuotients]
978 (sourceData : FreeProCSourceData ProC)
979 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
980 (psi : ContinuousMonoidHom sourceData.carrier H)
981 (hpsi : Function.Surjective psi) :
983 ProC.finiteQuotientClass psi.toMonoidHom ↔
984 Function.Injective
986 (H := H) (ProC := ProC) sourceData hbasis psi hpsi) := by
987 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
988 ⟨by
989 intro Q _ hQ
990 exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
991 letI :
992 Nonempty
994 ProC.finiteQuotientClass psi.toMonoidHom) :=
996 (C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
997 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi
999 (C := ProC.finiteQuotientClass) inferInstance),
1000 zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
1001 have hdir :
1002 Directed (· ≤ ·)
1003 (id :
1005 ProC.finiteQuotientClass psi.toMonoidHom →
1007 ProC.finiteQuotientClass psi.toMonoidHom) :=
1009 (C := ProC.finiteQuotientClass) (G := sourceData.carrier) (H := H)
1010 (ProCGroupPredicate.finiteQuotientFormation ProC)
1011 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi
1012 let family : ULift.{u} (Fin r) → sourceData.carrier :=
1013 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
1014 let hfree :=
1015 freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
1016 let htarget :=
1018 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
1019 let hφconv :=
1021 (ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
1022 have hH : ProC (G := H) :=
1024 have hφHconv :
1025 ProCGroups.FreeProC.FamilyConvergesToOne
1026 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
1027 simpa [family] using
1029 (ProC := ProC) sourceData hbasis psi.toMonoidHom
1030 have hφHgen :
1032 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
1033 simpa [family] using
1035 (ProC := ProC) sourceData hbasis psi hpsi
1036 have hiff :=
1038 (G := sourceData.carrier) (H := H) ProC psi family hfree htarget hφconv
1039 hdir sourceData.proCGroup.isProCGroup hH hφHconv hφHgen
1040 simpa [freeProCChosenULift_closedGeneratedCoordinateMap, family, hfree, htarget, hφconv,
1041 hH, hφHconv, hφHgen] using hiff
1043/-- The closed-generated coordinate-injectivity form of the remaining Morishita frontier.
1045Once the augmentation-ideal identification proves this injectivity, the finite-stage
1046relation-submodule closedness used by the Crowell and BL route theorems follows immediately. -/
1048 [T2Space H]
1049 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
1050 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
1051 [ProC.DeterminedByFiniteQuotients]
1052 (sourceData : FreeProCSourceData ProC)
1053 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
1054 (psi : ContinuousMonoidHom sourceData.carrier H)
1055 (hpsi : Function.Surjective psi)
1056 (hcoord_inj :
1057 Function.Injective
1059 (H := H) (ProC := ProC) sourceData hbasis psi hpsi)) :
1061 ProC.finiteQuotientClass psi.toMonoidHom :=
1063 (H := H) (ProC := ProC) sourceData hbasis psi hpsi).2 hcoord_inj
1065/-- Coordinate-injectivity form of the closed-generated fundamental formula. -/
1067 [T2Space H]
1068 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
1069 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
1070 [ProC.DeterminedByFiniteQuotients]
1071 (sourceData : FreeProCSourceData ProC)
1072 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
1073 (psi : ContinuousMonoidHom sourceData.carrier H)
1074 (hpsi : Function.Surjective psi)
1075 (hcoord_inj :
1076 Function.Injective
1078 (H := H) (ProC := ProC) sourceData hbasis psi hpsi)) :
1079 let htarget :=
1081 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
1082 ∀ g : sourceData.carrier,
1084 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
1085 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
1087 (ProC := ProC)
1088 (freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
1089 (fun i : ULift.{u} (Fin r) =>
1091 (ProC := ProC) sourceData hbasis i))
1092 htarget
1094 (ProC := ProC)
1095 (fun i : ULift.{u} (Fin r) =>
1097 (ProC := ProC) sourceData hbasis i)))
1098 g) =
1099 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g := by
1100 exact
1102 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
1104 (H := H) (ProC := ProC) sourceData hbasis psi hpsi hcoord_inj)
1106omit [ProC.finiteQuotientClass.ContainsTrivialQuotients] in
1107/-- For the chosen finite free pro-`C` basis, the closed-generated Fox graph internally supplies
1108the well-definedness of `d_N`. -/
1110 [T2Space H]
1111 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
1112 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
1113 [ProC.DeterminedByFiniteQuotients]
1114 (sourceData : FreeProCSourceData ProC)
1115 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
1116 (psi : ContinuousMonoidHom sourceData.carrier H)
1117 (hpsi : Function.Surjective psi)
1118 (htarget :
1119 ProC
1120 (G :=
1122 (ProC := ProC)
1123 (fun i : ULift.{u} (Fin r) =>
1125 (ProC := ProC) sourceData hbasis i)) : Subgroup
1127 ProC.finiteQuotientClass (ULift.{u} (Fin r)) H))))
1128 (hbasis_A :
1130 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
1131 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)) :
1133 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi := by
1134 let family : ULift.{u} (Fin r) → sourceData.carrier :=
1135 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
1136 let hfree :=
1137 freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
1138 let hφconv :=
1140 (ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
1142 ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi
1143 have hH : ProC (G := H) :=
1144 hHProCGroup.isProC
1145 have hφHconv :
1146 ProCGroups.FreeProC.FamilyConvergesToOne
1147 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
1148 simpa [family] using
1150 (ProC := ProC) sourceData hbasis psi.toMonoidHom
1151 have hφHgen :
1153 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
1154 simpa [family] using
1156 (ProC := ProC) sourceData hbasis psi hpsi
1157 have hleft_graph_eq :
1158 ∀ g : sourceData.carrier,
1160 (ProC := ProC) hfree (fun i : ULift.{u} (Fin r) => psi (family i))
1161 htarget hφconv g =
1163 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi family hbasis_A
1164 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) := by
1165 exact
1167 (G := sourceData.carrier) (H := H) ProC psi family hbasis_A hfree hH htarget hφconv
1168 hφHconv hφHgen
1169 exact
1171 (G := sourceData.carrier) (H := H) ProC psi family hbasis_A hfree htarget hφconv
1172 hleft_graph_eq
1174/-- Exactness at the separated Crowell middle term from the standard all-finite-quotient stage
1175family.
1178lies in the closed-generated Fox graph target, and the separated coordinate equivalence turns that
1180`A_psi(C)` basis or relation-submodule closedness hypothesis is used. -/
1182 [T2Space H]
1183 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
1184 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
1185 [ProC.DeterminedByFiniteQuotients]
1186 (sourceData : FreeProCSourceData ProC)
1187 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
1188 (psi : ContinuousMonoidHom sourceData.carrier H)
1189 (hpsi : Function.Surjective psi)
1190 [T1Space
1191 (ZCFreeFoxCoordinates ProC.finiteQuotientClass
1192 (X := ULift.{u} (Fin r)) (H := H))] :
1193 Function.Exact
1195 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi)
1197 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
1198 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi) := by
1199 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
1200 ⟨by
1201 intro Q _ hQ
1202 exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
1203 letI : CompactSpace sourceData.carrier :=
1204 ProCGroup.compactSpace ProC sourceData.carrier
1205 let family : ULift.{u} (Fin r) → sourceData.carrier :=
1206 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
1207 let hfree :=
1208 freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
1209 let htarget :=
1211 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
1212 let hφconv :=
1214 (ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
1216 ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi
1217 have hH : ProC (G := H) :=
1218 hHProCGroup.isProC
1219 have hH_isProC : IsProCGroup ProC.finiteQuotientClass H :=
1220 hHProCGroup.isProCGroup
1221 have hφHconv :
1222 ProCGroups.FreeProC.FamilyConvergesToOne
1223 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
1224 simpa [family] using
1226 (ProC := ProC) sourceData hbasis psi.toMonoidHom
1227 have hφHgen :
1229 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
1230 simpa [family] using
1232 (ProC := ProC) sourceData hbasis psi hpsi
1233 let φ : ULift.{u} (Fin r) → H := fun i => psi (family i)
1234 let coords :=
1236 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
1237 let Dcoords : sourceData.carrier →
1238 ZCFreeFoxCoordinates ProC.finiteQuotientClass
1239 (X := ULift.{u} (Fin r)) (H := H) :=
1240 fun g =>
1242 (ProC := ProC) hfree φ htarget hφconv g
1243 have hright_graph_eq :
1245 (ProC := ProC) hfree φ htarget hφconv =
1246 psi.toMonoidHom := by
1247 exact
1249 (ProC := ProC) (ULift.{u} (Fin r)) H hfree hH φ htarget hφconv
1250 hφHconv hφHgen psi (by intro i; rfl)
1251 have hcycle_closed :
1252 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ ⊆
1254 (ProC := ProC) φ : Subgroup
1255 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass
1256 (ULift.{u} (Fin r)) H)) : Set
1257 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass
1258 (ULift.{u} (Fin r)) H)) := by
1259 exact
1261 (ProC := ProC) (X := ULift.{u} (Fin r)) (H := H) φ hH_isProC hφHgen
1262 refine
1264 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
1265 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi family coords ?_ Dcoords ?_ ?_
1266 · rfl
1267 · intro n
1268 simpa [coords, Dcoords, family, hfree, htarget, hφconv, φ] using
1270 (H := H) (ProC := ProC) sourceData hbasis psi hpsi n.1).symm
1271 · intro v hv
1272 have hboundaryMap :
1274 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
1275 (fun i : ULift.{u} (Fin r) =>
1277 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi (family i)) =
1279 ProC.finiteQuotientClass
1280 (FreeGroup.lift φ) :=
1282 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi family
1283 have hvBoundary :
1284 zcFreeGroupFoxBoundary ProC.finiteQuotientClass (FreeGroup.lift φ) v = 0 := by
1285 simpa [hboundaryMap, φ] using hv
1286 have hy :
1287 ({ left := v, right := (1 : H) } :
1288 ZCCompletedFoxSemidirect ProC.finiteQuotientClass
1289 (ULift.{u} (Fin r)) H) ∈
1290 freeProCZCCompletedFoxSemidirectBoundaryCycleSet (ProC := ProC) φ := by
1291 constructor
1292 · rfl
1293 · exact hvBoundary
1294 have hyTarget := hcycle_closed hy
1295 rcases
1297 (ProC := ProC) hfree φ htarget hφconv hyTarget with
1298 ⟨g, hg⟩
1299 have hleft : Dcoords g = v := by
1300 have h := congrArg
1301 (fun z : ZCCompletedFoxSemidirect ProC.finiteQuotientClass
1302 (ULift.{u} (Fin r)) H => z.left) hg
1303 simpa [Dcoords, freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated] using h
1304 have hrightLift :
1306 (ProC := ProC) hfree φ htarget hφconv g = 1 := by
1307 have h := congrArg
1308 (fun z : ZCCompletedFoxSemidirect ProC.finiteQuotientClass
1309 (ULift.{u} (Fin r)) H => z.right) hg
1310 simpa [freeProCZCCompletedFoxRightHomViaClosedGenerated] using h
1311 have hright : psi g = 1 := by
1312 simpa [hright_graph_eq] using hrightLift
1313 exact ⟨⟨g, hright⟩, hleft⟩
1315omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass] in
1316/-- The universe-lifted chosen free basis is an `A_psi(C)` basis once the closed-generated
1317derivative vector satisfies the completed fundamental formula. -/
1319 [T2Space H]
1320 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
1321 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
1322 [ProC.DeterminedByFiniteQuotients]
1323 (sourceData : FreeProCSourceData ProC)
1324 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
1325 (psi : ContinuousMonoidHom sourceData.carrier H)
1326 (hpsi : Function.Surjective psi)
1327 (htarget :
1328 ProC
1329 (G :=
1331 (ProC := ProC)
1332 (fun i : ULift.{u} (Fin r) =>
1334 (ProC := ProC) sourceData hbasis i)) : Subgroup
1336 ProC.finiteQuotientClass (ULift.{u} (Fin r)) H))))
1337 (hfundamental :
1338 ∀ g : sourceData.carrier,
1340 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
1341 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
1343 (ProC := ProC)
1344 (freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
1345 (fun i : ULift.{u} (Fin r) =>
1347 (ProC := ProC) sourceData hbasis i))
1348 htarget
1350 (ProC := ProC)
1351 (fun i : ULift.{u} (Fin r) =>
1353 (ProC := ProC) sourceData hbasis i)))
1354 g) =
1355 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
1357 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
1358 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) := by
1359 let family : ULift.{u} (Fin r) → sourceData.carrier :=
1360 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
1361 let hfree :=
1362 freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
1363 let hφconv :=
1365 (ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
1367 ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi
1368 have hH : ProC (G := H) :=
1369 hHProCGroup.isProC
1370 have hφHconv :
1371 ProCGroups.FreeProC.FamilyConvergesToOne
1372 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
1373 simpa [family] using
1375 (ProC := ProC) sourceData hbasis psi.toMonoidHom
1376 have hφHgen :
1378 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
1379 simpa [family] using
1381 (ProC := ProC) sourceData hbasis psi hpsi
1382 exact
1384 (G := sourceData.carrier) (H := H) ProC psi family hfree
1385 (by simpa [family] using htarget) hφconv hH hφHconv hφHgen
1386 (by simpa [family, hfree, hφconv] using hfundamental)
1388omit [ProC.finiteQuotientClass.ContainsTrivialQuotients] in
1389/-- The universe-lifted chosen free basis is an `A_psi(C)` basis when the closed-generated
1390module-valued fundamental formula follows from continuity into a Hausdorff topology on
1391`A_psi(C)`.
1393This is the topological version of
1395derives the former `hfundamental` hypothesis from continuous-crossed-differential uniqueness. -/
1397 [T2Space H]
1398 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
1399 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
1400 [ProC.DeterminedByFiniteQuotients]
1401 (sourceData : FreeProCSourceData ProC)
1402 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
1403 (psi : ContinuousMonoidHom sourceData.carrier H)
1404 (hpsi : Function.Surjective psi)
1405 [TopologicalSpace (ZCCompletedDifferentialModule
1406 ProC.finiteQuotientClass psi.toMonoidHom)]
1407 [T2Space (ZCCompletedDifferentialModule
1408 ProC.finiteQuotientClass psi.toMonoidHom)]
1409 (htarget :
1410 ProC
1411 (G :=
1413 (ProC := ProC)
1414 (fun i : ULift.{u} (Fin r) =>
1416 (ProC := ProC) sourceData hbasis i)) : Subgroup
1418 ProC.finiteQuotientClass (ULift.{u} (Fin r)) H))))
1419 (hmodule_continuous :
1420 Continuous
1421 (fun g : sourceData.carrier =>
1423 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
1424 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
1426 (ProC := ProC)
1427 (freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
1428 (fun i : ULift.{u} (Fin r) =>
1430 (ProC := ProC) sourceData hbasis i))
1431 htarget
1433 (ProC := ProC)
1434 (fun i : ULift.{u} (Fin r) =>
1436 (ProC := ProC) sourceData hbasis i)))
1437 g)))
1438 (huniv_continuous :
1439 Continuous
1440 (fun g : sourceData.carrier =>
1441 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)) :
1443 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
1444 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) := by
1445 let family : ULift.{u} (Fin r) → sourceData.carrier :=
1446 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
1447 let hfree :=
1448 freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis
1449 let hφconv :=
1451 (ProC := ProC) (fun i : ULift.{u} (Fin r) => psi (family i))
1453 ProCGroup.of_surjective (G := sourceData.carrier) ProC psi hpsi
1454 have hH : ProC (G := H) :=
1455 hHProCGroup.isProC
1456 have hφHconv :
1457 ProCGroups.FreeProC.FamilyConvergesToOne
1458 (G := H) (fun i : ULift.{u} (Fin r) => psi (family i)) := by
1459 simpa [family] using
1461 (ProC := ProC) sourceData hbasis psi.toMonoidHom
1462 have hφHgen :
1464 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
1465 simpa [family] using
1467 (ProC := ProC) sourceData hbasis psi hpsi
1468 have hfundamental :
1469 ∀ g : sourceData.carrier,
1471 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi family
1473 (ProC := ProC) hfree (fun i : ULift.{u} (Fin r) => psi (family i))
1474 (by simpa [family] using htarget) hφconv g) =
1475 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g :=
1477 (G := sourceData.carrier) (H := H) ProC psi family hfree
1478 (by simpa [family] using htarget) hφconv hH hφHconv hφHgen
1479 (by simpa [family, hfree, hφconv] using hmodule_continuous)
1480 (by simpa using huniv_continuous)
1481 exact
1483 (H := H) (ProC := ProC) sourceData hbasis psi hpsi htarget
1484 (by simpa [family, hfree, hφconv] using hfundamental)
1486/-- The universe-lifted chosen free basis is an `A_psi(C)` basis, reduced to closedness of the
1487completed crossed-differential relation submodule.
1489This is a conditional route theorem: it removes the topology, Hausdorffness, continuity, and
1490fundamental-formula inputs, but still depends on the closedness statement that is the remaining
1493 [T2Space H]
1494 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
1495 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
1496 [ProC.DeterminedByFiniteQuotients]
1497 (sourceData : FreeProCSourceData ProC)
1498 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
1499 (psi : ContinuousMonoidHom sourceData.carrier H)
1500 (hpsi : Function.Surjective psi)
1501 (hclosed :
1503 ProC.finiteQuotientClass psi.toMonoidHom) :
1505 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
1506 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) := by
1507 let htarget :=
1509 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
1510 have hfundamental :
1511 ∀ g : sourceData.carrier,
1513 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
1514 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
1516 (ProC := ProC)
1517 (freeProCChosenULiftFamilyOfBasisCard_isFree (ProC := ProC) sourceData hbasis)
1518 (fun i : ULift.{u} (Fin r) =>
1520 (ProC := ProC) sourceData hbasis i))
1521 htarget
1523 (ProC := ProC)
1524 (fun i : ULift.{u} (Fin r) =>
1526 (ProC := ProC) sourceData hbasis i)))
1527 g) =
1528 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g := by
1529 simpa [htarget] using
1531 (H := H) (ProC := ProC) sourceData hbasis psi hpsi hclosed
1532 exact
1534 (H := H) (ProC := ProC) sourceData hbasis psi hpsi htarget hfundamental
1536/-- Coordinate-injectivity form of the finite `A_psi(C)` basis theorem. -/
1538 [T2Space H]
1539 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
1540 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
1541 [ProC.DeterminedByFiniteQuotients]
1542 (sourceData : FreeProCSourceData ProC)
1543 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
1544 (psi : ContinuousMonoidHom sourceData.carrier H)
1545 (hpsi : Function.Surjective psi)
1546 (hcoord_inj :
1547 Function.Injective
1549 (H := H) (ProC := ProC) sourceData hbasis psi hpsi)) :
1551 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
1552 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) :=
1554 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
1556 (H := H) (ProC := ProC) sourceData hbasis psi hpsi hcoord_inj)
1558/-- Free pro-`C` separated Crowell exactness from the standard all-finite-quotient stage
1559family and surjectivity of `psi`.
1561This is the public separated Crowell assembly theorem. The exactness at the separated middle
1563continuous Magnus. -/
1565 [T2Space H]
1566 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
1567 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
1568 [ProC.DeterminedByFiniteQuotients]
1569 (sourceData : FreeProCSourceData ProC)
1570 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
1571 (psi : ContinuousMonoidHom sourceData.carrier H)
1572 (hpsi : Function.Surjective psi) :
1573 Function.Injective
1575 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi) ∧
1576 Function.Exact
1578 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi)
1580 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
1581 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi) ∧
1582 Function.Exact
1584 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
1585 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi)
1586 (zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H) ∧
1587 Function.Surjective
1588 (zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H) :=
1589by
1590 exact
1592 (H := H) (ProC := ProC) sourceData hbasis psi hpsi,
1594 (H := H) (ProC := ProC) sourceData hbasis psi hpsi,
1596 (H := H) (ProC := ProC) sourceData hbasis psi hpsi,
1598 (C := ProC.finiteQuotientClass) (H := H)⟩
1600end
1602end CrowellExactSequence