Yamaguchi Lean 4 Library
CrowellExactSequence/Profinite/BlanchfieldLyndon.lean
CrowellExactSequence/Profinite/BlanchfieldLyndon/Source

CrowellExactSequence/Profinite/BlanchfieldLyndon.lean

1import CrowellExactSequence.Profinite.FreeExactness
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CrowellExactSequence/Profinite/BlanchfieldLyndon.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Free pro-C Blanchfield--Lyndon over pro-C integer coefficients
14BL is only the finite-basis coordinate expression of the displayed Crowell sequence
16```text
17N^ab(C) -> A_psi(C) -> Z_C[[H]] -> Z_C.
18```
20This file transports exactness through the chosen finite basis of `A_psi(C)`.
21-/
23namespace CrowellExactSequence
25noncomputable section
27open FoxDifferential
28open ProCGroups.ProC
30universe u
32variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
33variable {ProC : ProCGroupPredicate.{u}}
35/-- The BL first map: take the genuine `d_N : N^ab(C) -> A_psi(C)` and read it in the chosen
36finite basis coordinates of `A_psi(C)`. -/
38 (sourceData : FreeProCSourceData ProC)
39 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
40 (psi : ContinuousMonoidHom sourceData.carrier H)
41 (hbasis_A :
43 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
44 (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis))
45 (hwell_dN :
47 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi) :
49 Fin r → ZCCompletedGroupAlgebra ProC.finiteQuotientClass H :=
50 fun x =>
52 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
53 (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis) hbasis_A
55 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi hwell_dN x)
57/-- Exactness at the Crowell middle term is equivalent to exactness at the finite
58Blanchfield--Lyndon coordinate middle term, once the chosen family is a basis of
59`A_psi(C)`.
61In paper language, this is only the change of coordinates
62`A_psi(C) ≃ Z_C[[H]]^r`; it does not change the kernel/image statement. -/
64 (sourceData : FreeProCSourceData ProC)
65 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
66 (psi : ContinuousMonoidHom sourceData.carrier H)
67 (hbasis_A :
69 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
70 (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis))
71 (hwell_dN :
73 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi) :
74 Function.Exact
76 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi hwell_dN)
78 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi) ↔
79 Function.Exact
81 (H := H) (ProC := ProC) sourceData hbasis psi hbasis_A hwell_dN)
83 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
84 (fun i : Fin r =>
86 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
87 ((freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis) i))) := by
88 let family : Fin r → sourceData.carrier :=
89 freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis
90 let dN :=
92 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi hwell_dN
93 let coords :=
95 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi family hbasis_A
96 let delta :=
98 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
99 let blDelta :=
101 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
102 (fun i : Fin r =>
104 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi (family i))
105 have hblDelta_comp : delta.comp coords.symm.toLinearMap = blDelta := by
107 exact
109 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi family
110 have hblDelta_apply (y) : blDelta y = delta (coords.symm y) := by
111 have h := congrArg (fun f => f y) hblDelta_comp
112 simpa [LinearMap.comp_apply] using h.symm
113 change
114 Function.Exact dN delta ↔
115 Function.Exact (fun x => coords (dN x)) blDelta
116 constructor
117 · intro hexact_A y
118 constructor
119 · intro hy
120 have hy_delta : delta (coords.symm y) = 0 := by
121 simpa [hblDelta_apply y] using hy
122 rcases (hexact_A (coords.symm y)).1 hy_delta with ⟨x, hx⟩
123 exact ⟨x, by simpa using congrArg coords hx⟩
124 · rintro ⟨x, rfl⟩
125 have hker : delta (dN x) = 0 :=
126 (hexact_A (dN x)).2 ⟨x, rfl⟩
127 calc
128 blDelta (coords (dN x)) = delta (coords.symm (coords (dN x))) :=
129 hblDelta_apply (coords (dN x))
130 _ = delta (dN x) := by rw [coords.symm_apply_apply]
131 _ = 0 := hker
132 · intro hexact_BL y
133 constructor
134 · intro hy
135 have hy_bl : blDelta (coords y) = 0 := by
136 calc
137 blDelta (coords y) = delta (coords.symm (coords y)) :=
138 hblDelta_apply (coords y)
139 _ = delta y := by rw [coords.symm_apply_apply]
140 _ = 0 := hy
141 rcases (hexact_BL (coords y)).1 hy_bl with ⟨x, hx⟩
142 refine ⟨x, ?_⟩
143 apply coords.injective
144 simpa using hx
145 · rintro ⟨x, rfl⟩
146 have hbl : blDelta (coords (dN x)) = 0 :=
147 (hexact_BL (coords (dN x))).2 ⟨x, rfl⟩
148 calc
149 delta (dN x) = delta (coords.symm (coords (dN x))) := by
150 rw [coords.symm_apply_apply]
151 _ = blDelta (coords (dN x)) := by
152 rw [hblDelta_apply]
153 _ = 0 := hbl
155/-- The separated BL first map: take `d_N^sep` and read it in the separated chosen coordinates. -/
157 [T2Space H]
158 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
159 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
160 [ProC.DeterminedByFiniteQuotients]
161 (sourceData : FreeProCSourceData ProC)
162 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
163 (psi : ContinuousMonoidHom sourceData.carrier H)
164 (hpsi : Function.Surjective psi) :
166 ZCFreeFoxCoordinates ProC.finiteQuotientClass
167 (X := ULift.{u} (Fin r)) (H := H) :=
168 fun x =>
170 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
172 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi x)
174/-- Exactness at the separated Crowell middle term is equivalent to exactness at the finite
175Blanchfield--Lyndon coordinate middle term for the separated coordinate equivalence. -/
177 [T2Space H]
178 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
179 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
180 [ProC.DeterminedByFiniteQuotients]
181 (sourceData : FreeProCSourceData ProC)
182 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
183 (psi : ContinuousMonoidHom sourceData.carrier H)
184 (hpsi : Function.Surjective psi) :
185 Function.Exact
187 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi)
189 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
190 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi) ↔
191 Function.Exact
193 (H := H) (ProC := ProC) sourceData hbasis psi hpsi)
195 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
196 (fun i : ULift.{u} (Fin r) =>
198 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
199 ((freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) i))) := by
200 let family : ULift.{u} (Fin r) → sourceData.carrier :=
201 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
202 let dN :=
204 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
205 let coords :=
207 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
208 let delta :=
210 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
211 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi
212 let blDelta :=
214 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
215 (fun i : ULift.{u} (Fin r) =>
217 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi (family i))
218 have hcoords_symm :
219 coords.symm.toLinearMap =
221 (H := H) (ProC := ProC) sourceData hbasis psi := by
222 rfl
223 have hblDelta_comp : delta.comp coords.symm.toLinearMap = blDelta := by
224 rw [hcoords_symm]
225 exact
227 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
228 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi family
229 have hblDelta_apply (y) : blDelta y = delta (coords.symm y) := by
230 have h := congrArg (fun f => f y) hblDelta_comp
231 simpa [LinearMap.comp_apply] using h.symm
232 change
233 Function.Exact dN delta ↔
234 Function.Exact (fun x => coords (dN x)) blDelta
235 constructor
236 · intro hexact_A y
237 constructor
238 · intro hy
239 have hy_delta : delta (coords.symm y) = 0 := by
240 simpa [hblDelta_apply y] using hy
241 rcases (hexact_A (coords.symm y)).1 hy_delta with ⟨x, hx⟩
242 exact ⟨x, by simpa using congrArg coords hx⟩
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/-- BL exactness at `Z_C[[H]]`, supplied by a finite free basis and surjectivity of `psi`. -/
277 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
278 (sourceData : FreeProCSourceData ProC)
279 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
280 (psi : ContinuousMonoidHom sourceData.carrier H)
281 (hpsi : Function.Surjective psi) :
282 Function.Exact
284 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
285 (fun i : Fin r =>
287 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
288 ((freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis) i)))
289 (zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H) := by
290 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
291 ⟨by
292 intro Q _ hQ
293 exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
294 let family : Fin r → sourceData.carrier :=
295 freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis
296 have htargetGen :
298 (G := H) (Set.range (fun i : Fin r => psi (family i))) := by
299 simpa [family] using
301 (ProC := ProC) sourceData hbasis psi hpsi
302 simpa [family] using
304 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
305 (ProCGroupPredicate.finiteQuotientFormation ProC) psi family htargetGen
307/-- Separated-coordinate BL exactness at `Z_C[[H]]`, supplied by a finite free basis and
308surjectivity of `psi`. -/
310 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
311 (sourceData : FreeProCSourceData ProC)
312 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
313 (psi : ContinuousMonoidHom sourceData.carrier H)
314 (hpsi : Function.Surjective psi) :
315 Function.Exact
317 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
318 (fun i : ULift.{u} (Fin r) =>
320 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
321 ((freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) i)))
322 (zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H) := by
323 letI : Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass) :=
324 ⟨by
325 intro Q _ hQ
326 exact ProCGroupPredicate.finiteQuotientFinite ProC hQ⟩
327 let family : ULift.{u} (Fin r) → sourceData.carrier :=
328 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis
329 have htargetGen :
331 (G := H) (Set.range (fun i : ULift.{u} (Fin r) => psi (family i))) := by
332 simpa [family] using
334 (ProC := ProC) sourceData hbasis psi hpsi
335 simpa [family] using
337 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
338 (ProCGroupPredicate.finiteQuotientFormation ProC) psi family htargetGen
340/-- Separated-coordinate BL exactness from the standard all-finite-quotient stage family and
341surjectivity of `psi`.
343This is the public separated Blanchfield-Lyndon assembly theorem. The separated Crowell
344middle-exactness input is proved internally from the all-finite stage family. -/
346 [T2Space H]
347 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
348 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
349 [ProC.DeterminedByFiniteQuotients]
350 (sourceData : FreeProCSourceData ProC)
351 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
352 (psi : ContinuousMonoidHom sourceData.carrier H)
353 (hpsi : Function.Surjective psi) :
356 (H := H) (ProC := ProC) sourceData hbasis psi hpsi)
358 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
359 (fun i : ULift.{u} (Fin r) =>
361 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
362 ((freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) i)))
363 (zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H) :=
364by
365 let dN :=
367 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
368 let coords :=
370 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
371 let blDelta :=
373 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
374 (fun i : ULift.{u} (Fin r) =>
376 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
377 ((freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) i))
378 have hinj_dN :
379 Function.Injective dN :=
381 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
382 have hexact_A :
383 Function.Exact dN
385 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
386 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi) :=
388 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
389 have hexact_BL_A :
390 Function.Exact
391 (fun x : ProCKernelAbelianizationAdd ProC psi => coords (dN x))
392 blDelta :=
394 (H := H) (ProC := ProC) sourceData hbasis psi hpsi).1 hexact_A
395 change
397 (fun x : ProCKernelAbelianizationAdd ProC psi => coords (dN x)) blDelta
398 (zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H)
399 refine ⟨?_, hexact_BL_A, ?_, ?_⟩
400 · intro x y hxy
401 exact hinj_dN (coords.injective hxy)
402 · exact
404 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
405 · exact
407 (C := ProC.finiteQuotientClass) (H := H)
409/-- The canonical equivalence from concrete finite coordinates to the universe-lifted copy used by
410the free pro-`C` universal property. -/
411def finULiftEquiv (r : Nat) : Fin r ≃ ULift.{u} (Fin r) where
412 toFun i := ULift.up i
413 invFun i := i.down
414 left_inv := by
415 intro i
416 rfl
417 right_inv := by
418 intro i
419 cases i
420 rfl
422/-- The separated BL first map in the concrete `Fin r` basis. It is the public separated
423coordinate map reindexed back from the universe-lifted finite basis. -/
425 [T2Space H]
426 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
427 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
428 [ProC.DeterminedByFiniteQuotients]
429 (sourceData : FreeProCSourceData ProC)
430 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
431 (psi : ContinuousMonoidHom sourceData.carrier H)
432 (hpsi : Function.Surjective psi) :
434 Fin r → ZCCompletedGroupAlgebra ProC.finiteQuotientClass H :=
435 let e : Fin r ≃ ULift.{u} (Fin r) := finULiftEquiv r
436 fun x =>
438 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) e).symm
440 (H := H) (ProC := ProC) sourceData hbasis psi hpsi x)
443/-- Exactness at the separated Crowell middle term is equivalent to exactness at the concrete
444`Fin r` Blanchfield--Lyndon coordinate middle term. -/
446 [T2Space H]
447 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
448 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
449 [ProC.DeterminedByFiniteQuotients]
450 (sourceData : FreeProCSourceData ProC)
451 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
452 (psi : ContinuousMonoidHom sourceData.carrier H)
453 (hpsi : Function.Surjective psi) :
454 Function.Exact
456 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi)
458 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
459 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi) ↔
460 Function.Exact
462 (H := H) (ProC := ProC) sourceData hbasis psi hpsi)
464 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
465 (fun i : Fin r =>
467 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
468 ((freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis) i))) := by
469 let e : Fin r ≃ ULift.{u} (Fin r) := finULiftEquiv r
470 let L :
471 (Fin r → ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) ≃ₗ[
472 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
473 (ULift.{u} (Fin r) →
474 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) :=
476 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) e
477 let blULift :=
479 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
480 (fun i : ULift.{u} (Fin r) =>
482 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
483 ((freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) i))
484 let blFin :=
486 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
487 (fun i : Fin r =>
489 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
490 ((freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis) i))
491 have hblFin :
492 blFin = blULift.comp L.toLinearMap := by
493 simpa [blFin, blULift, L, e, finULiftEquiv, freeProCChosenULiftFamilyOfBasisCard] using
495 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
496 e
497 (fun i : ULift.{u} (Fin r) =>
499 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
500 ((freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) i)))
501 have hULiftIff :=
503 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
504 have htransport :
505 Function.Exact
506 (fun x : ProCKernelAbelianizationAdd ProC psi =>
507 L.symm
509 (H := H) (ProC := ProC) sourceData hbasis psi hpsi x))
510 (fun y : Fin r → ZCCompletedGroupAlgebra ProC.finiteQuotientClass H =>
511 blULift (L y)) ↔
512 Function.Exact
514 (H := H) (ProC := ProC) sourceData hbasis psi hpsi)
515 blULift :=
517 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) L
518 change
519 Function.Exact
521 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi)
523 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
524 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi) ↔
525 Function.Exact
526 (fun x : ProCKernelAbelianizationAdd ProC psi =>
527 L.symm
529 (H := H) (ProC := ProC) sourceData hbasis psi hpsi x))
530 blFin
531 rw [hblFin]
532 exact hULiftIff.trans htransport.symm
534/-- Concrete `Fin r` separated-coordinate BL exactness from the standard all-finite-quotient stage
535family and surjectivity of `psi`.
537This is the same theorem as
539transported through the finite reindexing equivalence `Fin r ≃ ULift (Fin r)`. It leaves no
540closedness, coordinate-injectivity, algebraic-basis, `d_N` well-definedness, or middle-exactness
541inputs in the statement. -/
543 [T2Space H]
544 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
545 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
546 [ProC.DeterminedByFiniteQuotients]
547 (sourceData : FreeProCSourceData ProC)
548 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
549 (psi : ContinuousMonoidHom sourceData.carrier H)
550 (hpsi : Function.Surjective psi) :
553 (H := H) (ProC := ProC) sourceData hbasis psi hpsi)
555 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
556 (fun i : Fin r =>
558 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
559 ((freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis) i)))
560 (zcCompletedGroupAlgebraAugmentation ProC.finiteQuotientClass H) :=
561by
562 let e : Fin r ≃ ULift.{u} (Fin r) := finULiftEquiv r
563 let L :
564 (Fin r → ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) ≃ₗ[
565 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
566 (ULift.{u} (Fin r) →
567 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) :=
569 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) e
570 let dN :=
572 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
573 let coords :=
575 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
576 have hinj_dN :
577 Function.Injective dN :=
579 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
580 have hexact_A :
581 Function.Exact dN
583 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass
584 (ProCGroupPredicate.finiteQuotientHereditary ProC) psi) :=
586 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
587 refine ⟨?_, ?_, ?_, ?_⟩
588 · intro x y hxy
589 change L.symm (coords (dN x)) = L.symm (coords (dN y)) at hxy
590 exact hinj_dN (coords.injective (L.symm.injective hxy))
591 · exact
593 (H := H) (ProC := ProC) sourceData hbasis psi hpsi).1 hexact_A
594 · exact
596 (H := H) (ProC := ProC) sourceData hbasis psi hpsi
597 · exact
599 (C := ProC.finiteQuotientClass) (H := H)
602/-- The `ULift (Fin r)` display of the chosen free basis has the completed differential basis
603property whenever the concrete `Fin r` display does. -/
605 (sourceData : FreeProCSourceData ProC)
606 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
607 (psi : ContinuousMonoidHom sourceData.carrier H)
608 (hbasis_A :
610 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
611 (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis)) :
613 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
614 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis) := by
615 let e : ULift.{u} (Fin r) ≃ Fin r :=
616 { toFun := fun i => i.down
617 invFun := fun i => ULift.up i
618 left_inv := by
619 intro i
620 cases i
621 rfl
622 right_inv := by
623 intro i
624 rfl }
625 change
627 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
628 (fun i : ULift.{u} (Fin r) =>
629 freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis (e i))
630 exact
632 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi e
633 (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
634 hbasis_A
637/-- The finite `Fin r` display inherits the `A_psi(C)` basis from the universe-lifted chosen
638family. -/
640 (sourceData : FreeProCSourceData ProC)
641 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
642 (psi : ContinuousMonoidHom sourceData.carrier H)
643 (hbasis_A :
645 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
646 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)) :
648 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
649 (freeProCChosenFamilyOfBasisCard (ProC := ProC) sourceData hbasis) := by
650 let e : Fin r ≃ ULift.{u} (Fin r) :=
651 { toFun := fun i => ULift.up i
652 invFun := fun i => i.down
653 left_inv := by
654 intro i
655 rfl
656 right_inv := by
657 intro i
658 cases i
659 rfl }
660 change
662 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi
663 (fun i : Fin r =>
664 freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis (e i))
665 exact
667 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi e
668 (freeProCChosenULiftFamilyOfBasisCard (ProC := ProC) sourceData hbasis)
669 hbasis_A
671end
673end CrowellExactSequence