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

CrowellExactSequence/Profinite/Exactness.lean

1import CrowellExactSequence.Profinite.KernelInjectivity
2import FoxDifferential.Completed.FreeProC.FiniteQuotientStages
3import FoxDifferential.Completed.Continuous.SemidirectKernelBasis
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/CrowellExactSequence/Profinite/Exactness.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Crowell exactness over pro-C integer coefficients
16This file contains only the displayed paper sequence
18```text
19N^ab(C) -> A_psi(C) -> Z_C[[H]] -> Z_C.
20```
22The theorem below is stated in the paper's four maps, without route-level packages.
23-/
25namespace CrowellExactSequence
27noncomputable section
29open FoxDifferential
30open ProCGroups.ProC
31open ProCGroups.Completion
32open ProCGroups.InverseSystems
34universe u v
36variable {G H : Type u}
37variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
38variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
40/-- The separated displayed boundary kills the separated kernel boundary. -/
42 (C : ProCGroups.FiniteGroupClass.{u})
44 (psi : ContinuousMonoidHom G H)
47 (G := G) (H := H) C hC psi
49 (G := G) (H := H) C psi x) =
50 0 := by
51 change
54 (G := G) (H := H) C hC psi
56 (G := G) (H := H) C psi (Additive.ofMul y)) =
57 0) (Additive.toMul x)
58 refine QuotientGroup.induction_on (Additive.toMul x) ?_
59 intro n
60 change
62 (G := G) (H := H) C hC psi
64 (G := G) (H := H) C psi
65 (Additive.ofMul
66 (QuotientGroup.mk'
67 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n))) =
68 0
72 (C := C) (H := H) psi.toMonoidHom n.2
74/-- Separated middle exactness is equivalent to integrating every separated `delta`-cycle by a
75kernel element. -/
77 (C : ProCGroups.FiniteGroupClass.{u})
79 (psi : ContinuousMonoidHom G H) :
80 Function.Exact
82 (G := G) (H := H) C psi)
84 (G := G) (H := H) C hC psi) ↔
85 ∀ a : ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom,
87 (G := G) (H := H) C hC psi a = 0 →
89 zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 = a := by
90 let dN :=
92 (G := G) (H := H) C psi
93 let delta :=
95 (G := G) (H := H) C hC psi
96 constructor
97 · intro hexact a ha
98 rcases (hexact a).1 ha with ⟨x, hx⟩
99 revert hx
100 change
102 dN (Additive.ofMul q) = a →
104 zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 = a) (Additive.toMul x)
105 refine QuotientGroup.induction_on (Additive.toMul x) ?_
106 intro n hn
107 refine ⟨n, ?_⟩
108 simpa [dN] using hn
109 · intro hintegrates a
110 constructor
111 · intro ha
112 rcases hintegrates a ha with ⟨n, hn⟩
113 refine ⟨Additive.ofMul
114 (QuotientGroup.mk'
115 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n), ?_⟩
116 simpa [dN] using hn
117 · rintro ⟨x, hx⟩
118 rw [← hx]
119 exact
121 (G := G) (H := H) C hC psi x
123/-- Separated middle exactness from a direct coordinate-lifting criterion for finite Fox cycles.
125The coordinate system is supplied explicitly as an equivalence from the separated completed
126module to finite Fox coordinates. This is the separated replacement for the algebraic finite
127basis route: no closedness or algebraic coordinate-basis hypothesis is used. -/
129 (C : ProCGroups.FiniteGroupClass.{u})
131 (psi : ContinuousMonoidHom G H)
132 {X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
133 (coords :
136 ZCFreeFoxCoordinates C (X := X) (H := H))
137 (hcoords_symm :
138 coords.symm.toLinearMap =
140 (G := G) (H := H) C psi family)
141 (Dcoords : G → ZCFreeFoxCoordinates C (X := X) (H := H))
142 (hDcoords_kernel :
144 Dcoords n.1 =
145 coords (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1))
146 (hcycle_lift :
147 ∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
150 (fun i : X =>
152 (G := G) (H := H) C psi (family i)) v = 0 →
153 ∃ n : ProfiniteKernelSubgroup psi, Dcoords n.1 = v) :
154 Function.Exact
156 (G := G) (H := H) C psi)
158 (G := G) (H := H) C hC psi) := by
159 let dN :=
161 (G := G) (H := H) C psi
162 let delta :=
164 (G := G) (H := H) C hC psi
165 let blDelta :=
168 (fun i : X =>
170 (G := G) (H := H) C psi (family i))
171 have hblDelta_comp : delta.comp coords.symm.toLinearMap = blDelta := by
172 rw [hcoords_symm]
173 exact
175 (G := G) (H := H) C hC psi family
176 have hblDelta_apply (y) : blDelta y = delta (coords.symm y) := by
177 have h := congrArg (fun f => f y) hblDelta_comp
178 simpa [LinearMap.comp_apply, delta, blDelta] using h.symm
179 change Function.Exact dN delta
180 intro a
181 constructor
182 · intro ha
183 have hcoord_cycle : blDelta (coords a) = 0 := by
184 calc
185 blDelta (coords a) = delta (coords.symm (coords a)) := hblDelta_apply (coords a)
186 _ = delta a := by rw [coords.symm_apply_apply]
187 _ = 0 := ha
188 rcases hcycle_lift (coords a) hcoord_cycle with ⟨n, hncoords⟩
189 refine ⟨Additive.ofMul
190 (QuotientGroup.mk'
191 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n), ?_⟩
192 apply coords.injective
193 calc
194 coords
195 (dN (Additive.ofMul
196 (QuotientGroup.mk'
197 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n))) =
198 coords (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1) := by
200 _ = Dcoords n.1 := (hDcoords_kernel n).symm
201 _ = coords a := hncoords
202 · rintro ⟨x, hx⟩
203 rw [← hx]
204 exact
206 (G := G) (H := H) C hC psi x
208/-- Continuity of the paper coordinate universal differential follows once its coordinates are
209identified with the closed-generated completed Fox derivative vector. -/
211 (ProC : ProCGroupPredicate.{u}) (psi : ContinuousMonoidHom G H)
212 {X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
213 (hbasis_A :
215 (G := G) (H := H) ProC.finiteQuotientClass psi family)
216 (hfree :
217 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
218 (ProC := ProC) X G family)
219 (htarget :
220 ProC
221 (G :=
223 (ProC := ProC) (fun i : X => psi (family i)) : Subgroup
224 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
225 (hφconv :
226 ProCGroups.FreeProC.FamilyConvergesToOne
227 (G :=
229 (ProC := ProC) (fun i : X => psi (family i)) : Subgroup
230 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
232 (ProC := ProC) (fun i : X => psi (family i))))
233 (hleft_graph_eq :
234 ∀ g : G,
236 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g =
238 (G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A
239 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)) :
240 Continuous
241 (fun g : G =>
243 (G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A
244 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)) := by
245 let Dclosed : G → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
246 fun g =>
248 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g
249 have hclosed_continuous : Continuous Dclosed := by
250 simpa [Dclosed] using
252 (ProC := ProC) X H hfree (fun i : X => psi (family i)) htarget hφconv
253 have hcoords_eq :
254 (fun g : G =>
256 (G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A
257 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)) = Dclosed := by
258 funext g
259 exact (hleft_graph_eq g).symm
260 rw [hcoords_eq]
261 exact hclosed_continuous
263/-- The left coordinate of the closed-generated completed Fox graph is the paper coordinate
264universal differential, once the chosen completed differentials form the finite coordinate basis.
266The proof avoids a separate continuity assumption for the paper coordinate map. The
267closed-generated Fox vector is a crossed differential, hence it is represented by a linear map out
268of the universal completed differential module. This linear map sends each basis differential
269`d(family i)` to the standard coordinate vector, so the finite-basis hypothesis identifies it with
270the inverse coordinate map. -/
272 (ProC : ProCGroupPredicate.{u}) (psi : ContinuousMonoidHom G H)
273 {X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
274 (hbasis_A :
276 (G := G) (H := H) ProC.finiteQuotientClass psi family)
277 (hfree :
278 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
279 (ProC := ProC) X G family)
280 (hH : ProC (G := H))
281 (htarget :
282 ProC
283 (G :=
285 (ProC := ProC) (fun i : X => psi (family i)) : Subgroup
286 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
287 (hφconv :
288 ProCGroups.FreeProC.FamilyConvergesToOne
289 (G :=
291 (ProC := ProC) (fun i : X => psi (family i)) : Subgroup
292 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
294 (ProC := ProC) (fun i : X => psi (family i))))
295 (hφHconv :
296 ProCGroups.FreeProC.FamilyConvergesToOne
297 (G := H) (fun i : X => psi (family i)))
298 (hφHgen :
300 (G := H) (Set.range (fun i : X => psi (family i)))) :
301 ∀ g : G,
303 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g =
305 (G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A
306 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) := by
307 let coords :=
309 (G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A
310 let f :
311 (X → ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) →ₗ[
312 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
313 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom :=
315 (G := G) (H := H) ProC.finiteQuotientClass psi family
316 let L :
317 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom →ₗ[
318 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
319 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
321 (G := G) (H := H) ProC psi family hfree htarget hφconv hH hφHconv hφHgen
322 have hL_comp : L.comp f = LinearMap.id := by
323 exact
325 (G := G) (H := H) ProC psi family hfree htarget hφconv hH hφHconv hφHgen
326 have hL_eq_coords : L = coords.toLinearMap := by
327 exact
329 (G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A L hL_comp
330 intro g
331 calc
333 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g =
334 L (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) := by
336 (G := G) (H := H) ProC psi family hfree htarget hφconv hH hφHconv hφHgen g]
337 _ = coords
338 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) := by
339 rw [hL_eq_coords]
340 rfl
342/-- The closed-generated coordinate identity makes the displayed boundary map on `N` factor through
343the topological abelianization. -/
345 (ProC : ProCGroupPredicate.{u}) (psi : ContinuousMonoidHom G H)
346 {X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
347 [T1Space (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))]
348 (hbasis_A :
350 (G := G) (H := H) ProC.finiteQuotientClass psi family)
351 (hfree :
352 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
353 (ProC := ProC) X G family)
354 (htarget :
355 ProC
356 (G :=
358 (ProC := ProC) (fun i : X => psi (family i)) : Subgroup
359 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
360 (hφconv :
361 ProCGroups.FreeProC.FamilyConvergesToOne
362 (G :=
364 (ProC := ProC) (fun i : X => psi (family i)) : Subgroup
365 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
367 (ProC := ProC) (fun i : X => psi (family i))))
368 (hleft_graph_eq :
369 ∀ g : G,
371 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g =
373 (G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A
374 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)) :
376 (G := G) (H := H) ProC.finiteQuotientClass psi := by
377 let Dclosed : G → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
378 fun g =>
380 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g
381 refine
383 (G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A Dclosed ?_ ?_
384 · simpa [Dclosed] using
386 (ProC := ProC) X H hfree (fun i : X => psi (family i)) htarget hφconv
387 · intro n
388 exact hleft_graph_eq n.1
390/-- The full standard finite quotient coefficient maps have zero-neighbourhood kernels.
392For an open zero-neighbourhood in `Z_C[[H]]`, the inverse-limit topology gives a completed
393group-algebra stage projection whose kernel lies inside the neighbourhood. At the same index,
394the finite Fox target is canonically identified with that `H/U` stage, so vanishing after the
395finite Fox coefficient map forces vanishing of the original completed-stage projection. -/
397 {ProC : ProCGroupPredicate.{u}} [ProC.HasFiniteQuotientFormation]
398 {X H : Type u} [DecidableEq X]
399 [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
400 [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
401 (φ : X → H)
402 (hφgen :
405 (A := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
406 (fun j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H =>
408 (ProC := ProC) (X := X) (H := H) φ hφgen j).toAddMonoidHom) := by
410 ProC.finiteQuotientContainsTrivialQuotients
411 letI : Nonempty (ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) :=
412 ⟨(ProCIntegerIndex.terminal (C := ProC.finiteQuotientClass) inferInstance,
413 zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
414 let S := zcCompletedGroupAlgebraSystem ProC.finiteQuotientClass H
415 have hdir :
416 Directed (· ≤ ·) (id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →
417 ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) :=
419 (C := ProC.finiteQuotientClass) (H := H) ProC.finiteQuotientFormation
420 intro U hU hUzero
421 rcases S.exists_projection_preimage_subset hdir hU hUzero with
422 ⟨j, V, _hVopen, hzeroV, hpre⟩
423 refine ⟨j, ?_⟩
424 intro z hz
425 apply hpre
426 change zcCompletedGroupAlgebraProjection ProC.finiteQuotientClass H j z ∈ V
427 letI :
428 ∀ j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H,
429 DiscreteTopology
430 (CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2) :=
431 fun j =>
432 QuotientGroup.discreteTopology
434 ((OrderDual.ofDual j.2).1 : OpenNormalSubgroup H))
435 have hqmap_inj :
436 Function.Injective
438 (C := ProC.finiteQuotientClass) φ
439 (id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →
440 ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) hφgen j) := by
441 exact
443 (C := ProC.finiteQuotientClass) φ
444 (id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →
445 ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) hφgen j
446 have hstage_inj :
447 Function.Injective
449 (ProC := ProC) (X := X) (H := H)
451 (C := ProC.finiteQuotientClass) φ
452 (id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →
453 ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) j)
454 j.1.modulus j dvd_rfl
456 (C := ProC.finiteQuotientClass) φ
457 (id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →
458 ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) hφgen j)) := by
459 exact
461 (ProC := ProC) (X := X) (H := H)
463 (C := ProC.finiteQuotientClass) φ
464 (id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →
465 ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) j)
466 j
468 (C := ProC.finiteQuotientClass) φ
469 (id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →
470 ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) hφgen j)
471 hqmap_inj
472 have hzstage :
473 zcCompletedGroupAlgebraProjection ProC.finiteQuotientClass H j z = 0 := by
474 apply hstage_inj
479 simpa [hzstage] using hzeroV
481/-- Closed-generated target membership for all completed Fox boundary cycles from the standard
482all-finite quotient stage family of `Z_C[[H]]`.
484This is the finite-stage input needed by the separated route. It is deliberately stated before
485any Crowell middle term appears, so it does not mention the algebraic completed differential
486module or its finite coordinate basis. -/
488 {ProC : ProCGroupPredicate.{u}} [ProC.HasFiniteQuotientFormation]
489 {X H : Type u} [Fintype X] [DecidableEq X]
490 [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
491 [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
492 (φ : X → H)
493 (hH_isProC : IsProCGroup ProC.finiteQuotientClass H)
494 (hφgen :
498 (ProC := ProC) φ : Subgroup
499 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) : Set
500 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)) := by
502 ProC.finiteQuotientContainsTrivialQuotients
503 letI : Nonempty (ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) :=
504 ⟨(ProCIntegerIndex.terminal (C := ProC.finiteQuotientClass) inferInstance,
505 zcCompletedGroupAlgebraTopIndex ProC.finiteQuotientClass H)⟩
506 letI :
507 ∀ j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H,
508 Fact (0 < j.1.modulus) :=
509 fun j => ProCIntegerIndex.positiveFact j.1
510 letI :
511 ∀ j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H,
512 DiscreteTopology
513 (CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2) :=
514 fun j =>
515 QuotientGroup.discreteTopology
517 ((OrderDual.ofDual j.2).1 : OpenNormalSubgroup H))
518 let J := ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H
519 let Nstage : J → Subgroup (FreeGroup X) :=
521 (C := ProC.finiteQuotientClass) φ
522 (id : J → J)
523 let nstage : J → ℕ := fun j => j.1.modulus
524 let zcIndex : J → ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H := id
525 let qmap : ∀ j : J,
526 CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2 →*
527 finiteFoxStageTargetQuotient (X := X) (Nstage j) :=
529 (C := ProC.finiteQuotientClass) φ
530 (id : J → J) hφgen
531 have hdir : Directed (· ≤ ·) (id : J → J) :=
533 (C := ProC.finiteQuotientClass) (H := H) ProC.finiteQuotientFormation
534 have hN :
535 ∀ {i j : J}, i ≤ j → Nstage j ≤ Nstage i :=
537 (C := ProC.finiteQuotientClass) φ
538 (id : J → J) (fun hij => hij)
539 have hcoeff_mod :
540 ∀ {i j : J} (hij : i ≤ j),
541 ∀ a : ModNCompletedCoeff (zcIndex j).1.modulus,
543 (n := nstage i) (m := (zcIndex i).1.modulus) (dvd_rfl)
545 (n := (zcIndex i).1.modulus) (m := (zcIndex j).1.modulus)
546 (hij.1) a) =
547 modNCompletedCoeffMap (n := nstage i) (m := nstage j) (hij.1)
549 (n := nstage j) (m := (zcIndex j).1.modulus) (dvd_rfl) a) := by
550 intro i j hij a
551 simp only [id_eq, modNCompletedCoeffMap_rfl, RingHomCompTriple.comp_apply, RingHom.id_apply, nstage, zcIndex]
552 have hqmap_transition :
553 ∀ {i j : J} (hij : i ≤ j),
554 ∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2,
555 qmap i
556 ((OpenNormalSubgroupInClass.map
557 (C := ProC.finiteQuotientClass) (G := H)
558 (U := OrderDual.ofDual (zcIndex i).2)
559 (V := OrderDual.ofDual (zcIndex j).2)
560 (hij.2) q)) =
561 finiteFoxStageTargetQuotientMap (X := X) (hN hij) (qmap j q) := by
562 intro i j hij q
563 exact
565 (C := ProC.finiteQuotientClass) φ zcIndex (fun hij => hij) hφgen hij q
566 have hgenerators :
567 ∀ j : J, ∀ x : X,
568 qmap j (QuotientGroup.mk (φ x)) =
569 QuotientGroup.mk' (Nstage j) (FreeGroup.of x) := by
570 simpa [J, Nstage, zcIndex, qmap] using
572 (C := ProC.finiteQuotientClass) φ
573 (id : J → J) hφgen
574 have hcoeff_basis :
576 (A := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
577 (fun j : J =>
579 (ProC := ProC) (X := X) (H := H) Nstage nstage zcIndex
580 (fun _ => dvd_rfl) qmap j).toAddMonoidHom) := by
581 simpa [J, nstage, zcIndex, qmap, freeProCZCBifilteredFiniteQuotientStageCoeffMap] using
583 (ProC := ProC) (X := X) (H := H) φ hφgen
584 exact
586 (ProC := ProC) (X := X) (H := H)
587 (J := J) (Nstage := Nstage) (nstage := nstage)
588 (hN := hN) (hn := fun hij => hij.1)
589 (zcIndex := zcIndex) (hzcIndex := fun hij => hij)
590 (hmod := fun _ => dvd_rfl) (qmap := qmap)
591 φ hcoeff_mod hqmap_transition hgenerators
593 (ProC := ProC) (X := X) (H := H)
594 (Nstage := Nstage) (nstage := nstage) (hN := hN) (hn := fun hij => hij.1)
595 (zcIndex := zcIndex) (hzcIndex := fun hij => hij)
596 (hmod := fun _ => dvd_rfl) (qmap := qmap)
597 hdir hcoeff_mod hqmap_transition
599 (ProC := ProC) (X := X) (H := H)
600 (Nstage := Nstage) (nstage := nstage) (hN := hN) (hn := fun hij => hij.1)
601 (zcIndex := zcIndex) (hzcIndex := fun hij => hij)
602 (hmod := fun _ => dvd_rfl) (qmap := qmap)
603 hdir hcoeff_mod hqmap_transition hcoeff_basis)
605 (ProC := ProC) (X := X) (H := H)
606 (Nstage := Nstage) (zcIndex := zcIndex) (qmap := qmap)
607 (by
608 simpa [J, zcIndex] using
610 (C := ProC.finiteQuotientClass) (H := H) hH_isProC)
611 (by
612 intro j
613 simpa [J, Nstage, zcIndex, qmap] using
615 (C := ProC.finiteQuotientClass) φ
616 (id : J → J) hφgen j)))
618end
620end CrowellExactSequence