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

CrowellExactSequence/Profinite/SequenceMaps.lean

1import CrowellExactSequence.FiniteFamilyExactness
2import FoxDifferential.Completed.Continuous.TopologicalGeneration
3import FoxDifferential.Completed.Continuous.TailExactness
4import FoxDifferential.Completed.Continuous.Universal.NaturalTopology
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/CrowellExactSequence/Profinite/SequenceMaps.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Crowell maps over pro-C integer coefficients
17This file names the maps in the paper sequence
18`A_psi(C) -> Z_C[[H]] -> Z_C` and the finite-family BL coordinate map.
19-/
21namespace CrowellExactSequence
23noncomputable section
25open scoped BigOperators
26open FoxDifferential
28universe u v w
30variable {G H : Type u}
31variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
32variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
34/-- The value of `A_psi(C) -> Z_C[[H]]` on a displayed generator, `dg |-> psi(g)-1`. -/
36 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) (g : G) :
40/-- The displayed Crowell map `A_psi(C) -> Z_C[[H]]`. -/
42 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) :
45 zcToCompletedGroupAlgebra C psi.toMonoidHom
47/-- The displayed Crowell boundary from the separated completed middle term
48`A_psi(C)_sep -> Z_C[[H]]`. -/
50 (C : ProCGroups.FiniteGroupClass.{u})
52 (psi : ContinuousMonoidHom G H) :
57omit [IsTopologicalGroup G] in
58@[simp]
60 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) (g : G) :
62 (zcUniversalDifferential C psi.toMonoidHom g) =
64 exact zcToCompletedGroupAlgebra_universal C psi.toMonoidHom g
66omit [IsTopologicalGroup G] in
67@[simp]
69 (C : ProCGroups.FiniteGroupClass.{u})
71 (psi : ContinuousMonoidHom G H) (g : G) :
73 (G := G) (H := H) C hC psi
74 (zcSeparatedUniversalDifferential C psi.toMonoidHom g) =
77 (G := G) (H := H) C hC psi g
79omit [IsTopologicalGroup G] in
81 (C : ProCGroups.FiniteGroupClass.{u})
83 (psi : ContinuousMonoidHom G H) :
85 (G := G) (H := H) C hC psi).comp
88 (G := G) (H := H) C psi := by
90 (G := G) (H := H) C hC psi
92variable (C : ProCGroups.FiniteGroupClass.{u})
94/-- The `Z_C[[H]]`-linear family map sending the standard coordinate vector `e_i` to
95`d(family i)`. -/
97 (psi : ContinuousMonoidHom G H)
98 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G) :
100 ZCCompletedDifferentialModule C psi.toMonoidHom :=
103 (fun i : X => zcUniversalDifferential C psi.toMonoidHom (family i))
105omit [IsTopologicalGroup G] in
106@[simp]
108 (psi : ContinuousMonoidHom G H)
109 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G) (i : X) :
111 (G := G) (H := H) C psi family (Pi.single i 1) =
112 zcUniversalDifferential C psi.toMonoidHom (family i) := by
113 exact
116 (fun i : X => zcUniversalDifferential C psi.toMonoidHom (family i)) i
118/-- The finite-family map into the separated completed differential module. -/
120 (psi : ContinuousMonoidHom G H)
121 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G) :
122 ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
126 (fun i : X => zcSeparatedUniversalDifferential C psi.toMonoidHom (family i))
128omit [IsTopologicalGroup G] in
129@[simp]
131 (psi : ContinuousMonoidHom G H)
132 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G) (i : X) :
134 (G := G) (H := H) C psi family (Pi.single i 1) =
135 zcSeparatedUniversalDifferential C psi.toMonoidHom (family i) := by
136 exact
139 (fun i : X => zcSeparatedUniversalDifferential C psi.toMonoidHom (family i)) i
141omit [IsTopologicalGroup G] in
142/-- Projecting the separated finite-family map to a finite stage agrees with projecting the
143algebraic finite-family map to the same finite stage. -/
145 (psi : ContinuousMonoidHom G H)
146 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G)
147 (i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom) :
150 (G := G) (H := H) C psi family) =
153 (G := G) (H := H) C psi family) := by
155 intro x
156 rw [LinearMap.comp_apply, LinearMap.comp_apply,
162omit [IsTopologicalGroup G] in
163/-- The finite-family map into `A_psi(C)` is continuous for the finite-stage completed topology on
164`A_psi(C)`. -/
166 (psi : ContinuousMonoidHom G H)
167 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G) :
168 @Continuous
169 (ZCFreeFoxCoordinates C (X := X) (H := H))
171 inferInstance
174 (G := G) (H := H) C psi family) := by
175 rw [continuous_induced_rng]
176 change Continuous
177 (fun x : ZCFreeFoxCoordinates C (X := X) (H := H) =>
178 fun i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom =>
181 (G := G) (H := H) C psi family x))
182 refine continuous_pi fun i => ?_
183 letI : TopologicalSpace (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom i) :=
184 inferInstance
185 letI : DiscreteTopology (zcCompletedDifferentialModuleStageRing C psi.toMonoidHom i) :=
186 inferInstance
187 have hstageAction :
188 Continuous (fun p : zcCompletedDifferentialModuleStageRing C psi.toMonoidHom i ×
189 ZCCompletedDifferentialModuleStage C psi.toMonoidHom i => p.1 • p.2) :=
190 continuous_of_discreteTopology
191 have hsum :
192 Continuous
193 (fun x : ZCFreeFoxCoordinates C (X := X) (H := H) =>
194 ∑ k, x k •
195 zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i (family k)) := by
196 refine continuous_finset_sum _ fun k _ => ?_
197 have hcoeff :
198 Continuous (fun x : ZCFreeFoxCoordinates C (X := X) (H := H) =>
201 (continuous_apply k)
202 have hconst :
203 Continuous (fun _ : ZCFreeFoxCoordinates C (X := X) (H := H) =>
204 zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i (family k)) :=
205 continuous_const
206 have hterm := hstageAction.comp (hcoeff.prodMk hconst)
210 using hsum
212/-- The basis property for a finite family in the Fox completed differential module. -/
214 (psi : ContinuousMonoidHom G H)
215 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G) : Prop :=
216 Function.Bijective
218 (G := G) (H := H) C psi family)
220omit [IsTopologicalGroup G] in
221/-- The completed differential basis property is invariant under reindexing a finite family. -/
223 (psi : ContinuousMonoidHom G H)
224 {X : Type v} [Fintype X] [DecidableEq X]
225 {Y : Type w} [Fintype Y] [DecidableEq Y]
226 (e : X ≃ Y) (family : Y -> G)
227 (hbasis_A :
229 (G := G) (H := H) C psi family) :
231 (G := G) (H := H) C psi (fun x : X => family (e x)) := by
233 have hmap :
235 (G := G) (H := H) C psi (fun x : X => family (e x)) =
237 (G := G) (H := H) C psi family).comp
239 (R := ZCCompletedGroupAlgebra C H) e).toLinearMap := by
244 (M := ZCCompletedDifferentialModule C psi.toMonoidHom)
245 e (fun y : Y => zcUniversalDifferential C psi.toMonoidHom (family y)))
246 rw [hmap]
247 exact hbasis_A.comp
249 (R := ZCCompletedGroupAlgebra C H) e).bijective
251/-- Coordinates associated to a basis family in `A_psi(C)`. -/
253 (psi : ContinuousMonoidHom G H)
254 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G)
255 (hbasis_A :
257 (G := G) (H := H) C psi family) :
260 (LinearEquiv.ofBijective
262 (G := G) (H := H) C psi family)
263 hbasis_A).symm
265omit [IsTopologicalGroup G] in
267 (psi : ContinuousMonoidHom G H)
268 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G)
269 (hbasis_A :
271 (G := G) (H := H) C psi family) :
273 (G := G) (H := H) C psi family hbasis_A).symm.toLinearMap =
275 (G := G) (H := H) C psi family :=
276 rfl
278omit [IsTopologicalGroup G] in
279@[simp 900]
281 (psi : ContinuousMonoidHom G H)
282 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G)
283 (hbasis_A :
285 (G := G) (H := H) C psi family) (i : X) :
287 (G := G) (H := H) C psi family hbasis_A
288 (zcUniversalDifferential C psi.toMonoidHom (family i)) =
289 Pi.single i (1 : ZCCompletedGroupAlgebra C H) := by
290 let coords :=
292 (G := G) (H := H) C psi family hbasis_A
293 have hsingle :
294 coords.symm (Pi.single i (1 : ZCCompletedGroupAlgebra C H)) =
295 zcUniversalDifferential C psi.toMonoidHom (family i) := by
296 change
298 (G := G) (H := H) C psi family (Pi.single i 1) =
299 zcUniversalDifferential C psi.toMonoidHom (family i)
301 (G := G) (H := H) C psi family i
302 calc
303 coords (zcUniversalDifferential C psi.toMonoidHom (family i)) =
304 coords (coords.symm (Pi.single i (1 : ZCCompletedGroupAlgebra C H))) := by
305 rw [hsingle]
306 _ = Pi.single i (1 : ZCCompletedGroupAlgebra C H) := by
307 exact coords.apply_symm_apply (Pi.single i (1 : ZCCompletedGroupAlgebra C H))
309section ClosedGeneratedCoordinates
311variable (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
312variable (psi : ContinuousMonoidHom G H)
313variable {X : Type u} [Fintype X] [DecidableEq X]
314variable (family : X → G)
315variable
316 (hfree :
317 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
318 (ProC := ProC) X G family)
319variable
320 (htarget :
321 ProC
322 (G :=
324 (ProC := ProC) (fun i : X => psi (family i)) : Subgroup
325 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
326variable
327 (hφconv :
328 ProCGroups.FreeProC.FamilyConvergesToOne
329 (G :=
331 (ProC := ProC) (fun i : X => psi (family i)) : Subgroup
332 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
334 (ProC := ProC) (fun i : X => psi (family i))))
336/-- The closed-generated expansion into `A_psi(C)` is continuous for the finite-stage completed
337topology on `A_psi(C)`. -/
339 @Continuous G
340 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
341 inferInstance
343 ProC.finiteQuotientClass psi.toMonoidHom)
344 (fun g : G =>
346 (G := G) (H := H) ProC.finiteQuotientClass psi family
348 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g)) := by
349 letI : TopologicalSpace
350 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom) :=
351 zcCompletedDifferentialModuleNaturalTopology ProC.finiteQuotientClass psi.toMonoidHom
352 change Continuous
353 (fun g : G =>
355 (G := G) (H := H) ProC.finiteQuotientClass psi family
357 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g))
358 exact
360 (G := G) (H := H) ProC.finiteQuotientClass psi family).comp
362 (ProC := ProC) X H hfree (fun i : X => psi (family i)) htarget hφconv)
364/-- The closed-generated Fox vector, read as a crossed differential with the intended scalar
365`psi`, gives a linear map from `A_psi(C)` to finite completed Fox coordinates. -/
367 (hright :
369 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv =
370 psi.toMonoidHom) :
371 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom →ₗ[
372 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
373 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
374 let Dclosed : G → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
375 fun g =>
377 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g
378 have hclosed_cross :
380 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass psi.toMonoidHom)
381 Dclosed := by
382 have hraw :=
384 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv
385 simpa [Dclosed, hright] using hraw
387 (A := ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
388 ProC.finiteQuotientClass psi.toMonoidHom Dclosed hclosed_cross
390omit [Fintype X] in
391/-- Evaluation of the closed-generated coordinate lift on universal differentials. -/
392@[simp]
394 (hright :
396 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv =
397 psi.toMonoidHom)
398 (g : G) :
400 (G := G) (H := H) ProC psi family hfree htarget hφconv hright
401 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) =
403 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g := by
404 exact
406 (A := ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
407 ProC.finiteQuotientClass psi.toMonoidHom
408 (fun g : G =>
410 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g)
411 (by
412 have hraw :=
414 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv
415 simpa [hright] using hraw)
416 g
417/-- The closed-generated coordinate lift is a left inverse to the family map. -/
419 (hright :
421 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv =
422 psi.toMonoidHom) :
424 (G := G) (H := H) ProC psi family hfree htarget hφconv hright).comp
426 (G := G) (H := H) ProC.finiteQuotientClass psi family) =
427 LinearMap.id := by
428 let L :=
430 (G := G) (H := H) ProC psi family hfree htarget hφconv hright
431 have hL_family :
432 ∀ i : X,
433 L (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom (family i)) =
434 Pi.single i (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
435 intro i
436 calc
437 L (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom (family i)) =
439 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv
440 (family i) := by
441 simpa [L] using
443 (G := G) (H := H) ProC psi family hfree htarget hφconv hright
444 (family i)
445 _ = Pi.single i (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
450 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
451 (generators := fun i : X =>
452 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom (family i))
453 L hL_family)
455/-- Closed-generated coordinates with the right component identified by the free pro-`C`
456universal property. -/
458 (hH : ProC (G := H))
459 (hφHconv :
460 ProCGroups.FreeProC.FamilyConvergesToOne
461 (G := H) (fun i : X => psi (family i)))
462 (hφHgen :
464 (G := H) (Set.range (fun i : X => psi (family i)))) :
465 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom →ₗ[
466 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
467 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
469 (G := G) (H := H) ProC psi family hfree htarget hφconv
471 (ProC := ProC) X H hfree hH (fun i : X => psi (family i)) htarget hφconv
472 hφHconv hφHgen psi (by intro i; rfl))
474omit [Fintype X] in
475/-- Evaluation formula for `closedGeneratedDerivativeCoordinatesLinearMapProCInteger`. -/
476@[simp]
478 (hH : ProC (G := H))
479 (hφHconv :
480 ProCGroups.FreeProC.FamilyConvergesToOne
481 (G := H) (fun i : X => psi (family i)))
482 (hφHgen :
484 (G := H) (Set.range (fun i : X => psi (family i))))
485 (g : G) :
487 (G := G) (H := H) ProC psi family hfree htarget hφconv
488 hH hφHconv hφHgen
489 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) =
491 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g := by
493 exact
495 (G := G) (H := H) ProC psi family hfree htarget hφconv
497 (ProC := ProC) X H hfree hH (fun i : X => psi (family i)) htarget hφconv
498 hφHconv hφHgen psi (by intro i; rfl))
499 g
500omit [Fintype X] in
501/-- A finite-stage factorization criterion for continuity of the closed-generated coordinate
502lift.
504To prove the coordinate map `A_psi(C) -> Z_C[[H]]^X` is continuous for the natural finite-stage
505topology, it is enough to show that every finite coefficient coordinate of the map factors
506through some finite source/target/coefficient stage of `A_psi(C)`. This is the formal
507finite-stage compatibility statement left by the paper definition of `A_psi(C)`. -/
509 (hH : ProC (G := H))
510 (hφHconv :
511 ProCGroups.FreeProC.FamilyConvergesToOne
512 (G := H) (fun i : X => psi (family i)))
513 (hφHgen :
515 (G := H) (Set.range (fun i : X => psi (family i))))
516 (hfactor :
517 ∀ (x : X) (j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H),
519 ProC.finiteQuotientClass psi.toMonoidHom,
520 ∃ stageCoord :
522 ProC.finiteQuotientClass psi.toMonoidHom i →
523 ZCCompletedGroupAlgebraStage ProC.finiteQuotientClass H j,
524 ∀ a :
525 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom,
526 zcCompletedGroupAlgebraProjection ProC.finiteQuotientClass H j
528 (G := G) (H := H) ProC psi family hfree htarget hφconv
529 hH hφHconv hφHgen a x) =
530 stageCoord
532 ProC.finiteQuotientClass psi.toMonoidHom i a)) :
533 @Continuous
534 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
535 (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
537 ProC.finiteQuotientClass psi.toMonoidHom)
538 inferInstance
540 (G := G) (H := H) ProC psi family hfree htarget hφconv
541 hH hφHconv hφHgen) := by
542 letI : TopologicalSpace
543 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom) :=
545 ProC.finiteQuotientClass psi.toMonoidHom
546 let L :=
548 (G := G) (H := H) ProC psi family hfree htarget hφconv
549 hH hφHconv hφHgen
550 change @Continuous
551 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
552 (X → ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
554 ProC.finiteQuotientClass psi.toMonoidHom)
555 inferInstance L
556 refine continuous_pi fun x => ?_
557 refine Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible
558 ProC.finiteQuotientClass H) ?_ (fun a => (L a x).property)
559 refine continuous_pi fun j => ?_
560 rcases hfactor x j with ⟨i, stageCoord, hstageCoord⟩
561 letI : TopologicalSpace
563 ProC.finiteQuotientClass psi.toMonoidHom i) := inferInstance
564 letI : DiscreteTopology
566 ProC.finiteQuotientClass psi.toMonoidHom i) := inferInstance
567 have hstage : Continuous stageCoord := continuous_of_discreteTopology
568 have hproj :
569 @Continuous
570 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
572 ProC.finiteQuotientClass psi.toMonoidHom i)
574 ProC.finiteQuotientClass psi.toMonoidHom)
575 inferInstance
577 ProC.finiteQuotientClass psi.toMonoidHom i) :=
579 ProC.finiteQuotientClass psi.toMonoidHom i
580 have hcomp : Continuous
581 (fun a :
582 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom =>
583 stageCoord
585 ProC.finiteQuotientClass psi.toMonoidHom i a)) :=
586 hstage.comp hproj
587 have hfun :
588 (fun a :
589 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom =>
590 zcCompletedGroupAlgebraProjection ProC.finiteQuotientClass H j (L a x)) =
591 (fun a :
592 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom =>
593 stageCoord
595 ProC.finiteQuotientClass psi.toMonoidHom i a)) := by
596 funext a
597 simpa [L] using hstageCoord a
598 change Continuous
599 (fun a :
600 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom =>
601 zcCompletedGroupAlgebraProjection ProC.finiteQuotientClass H j (L a x))
602 rw [hfun]
603 exact hcomp
605omit [Fintype X] in
606/-- Concrete finite-stage factorization of each closed-generated coordinate.
608For a fixed coordinate `x` and finite coefficient/target stage `j`, the scalar-valued
609closed-generated Fox derivative is locally unchanged at `1` after intersecting with the target
610kernel. The pro-`C` open-normal basis supplies a source quotient in the same finite quotient
611class, and the crossed-differential rule descends the coordinate to that quotient. -/
613 (hGproC : ProCGroups.ProC.IsProCGroup ProC.finiteQuotientClass G)
614 (hH : ProC (G := H))
615 (hφHconv :
616 ProCGroups.FreeProC.FamilyConvergesToOne
617 (G := H) (fun i : X => psi (family i)))
618 (hφHgen :
620 (G := H) (Set.range (fun i : X => psi (family i))))
621 (x : X) (j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) :
623 ProC.finiteQuotientClass psi.toMonoidHom,
624 ∃ stageCoord :
626 ProC.finiteQuotientClass psi.toMonoidHom i →
627 ZCCompletedGroupAlgebraStage ProC.finiteQuotientClass H j,
628 ∀ a :
629 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom,
630 zcCompletedGroupAlgebraProjection ProC.finiteQuotientClass H j
632 (G := G) (H := H) ProC psi family hfree htarget hφconv
633 hH hφHconv hφHgen a x) =
634 stageCoord
636 ProC.finiteQuotientClass psi.toMonoidHom i a) := by
637 let C := ProC.finiteQuotientClass
638 let φ : X → H := fun i => psi (family i)
639 let L :=
641 (G := G) (H := H) ProC psi family hfree htarget hφconv
642 hH hφHconv hφHgen
643 let coordStage :
644 ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
646 {
647 toFun v := zcCompletedGroupAlgebraProjection C H j (v x)
648 map_add' v w := by
649 simp only [Pi.add_apply, zcCompletedGroupAlgebraProjection_add]
650 map_smul' r v := by
651 change zcCompletedGroupAlgebraProjection C H j (r * v x) =
655 }
656 let Dclosed : G → ZCFreeFoxCoordinates C (X := X) (H := H) :=
657 fun g =>
659 (ProC := ProC) hfree φ htarget hφconv g
660 let D : G → ZCCompletedGroupAlgebraStage C H j := fun g => coordStage (Dclosed g)
661 have hright :
663 (ProC := ProC) hfree φ htarget hφconv =
664 psi.toMonoidHom := by
665 exact
667 (ProC := ProC) X H hfree hH φ htarget hφconv hφHconv hφHgen psi
668 (by intro i; rfl)
669 have hclosed_cross :
672 Dclosed := by
673 have hraw :=
675 (ProC := ProC) hfree φ htarget hφconv
676 simpa [C, Dclosed, φ, hright] using hraw
677 have hDcross :
680 D := by
681 exact IsCrossedDifferential.map_linear hclosed_cross coordStage
682 have hDcont : Continuous D := by
683 have hvec :
684 Continuous Dclosed := by
685 simpa [C, Dclosed, φ] using
687 (ProC := ProC) X H hfree φ htarget hφconv)
688 have hcoord : Continuous (fun g : G => Dclosed g x) :=
689 (continuous_apply x).comp hvec
690 have hproj :
691 Continuous (fun a : ZCCompletedGroupAlgebra C H =>
694 simpa [D, coordStage] using hproj.comp hcoord
695 let Utarget : OpenNormalSubgroup H := (OrderDual.ofDual j.2).1
696 let W : Set G :=
697 {g : G | D g = 0 ∧ psi.toMonoidHom g ∈ (Utarget : Subgroup H)}
698 have hDzero_open : IsOpen {g : G | D g = 0} := by
699 change IsOpen (D ⁻¹' ({0} : Set (ZCCompletedGroupAlgebraStage C H j)))
700 exact (isOpen_discrete _).preimage hDcont
701 have htarget_open :
702 IsOpen {g : G | psi.toMonoidHom g ∈ (Utarget : Subgroup H)} := by
703 change IsOpen (psi ⁻¹' (((Utarget : Subgroup H) : Set H)))
704 exact (ProCGroups.openNormalSubgroup_isOpen (G := H) Utarget).preimage
705 psi.continuous_toFun
706 have hWopen : IsOpen W := hDzero_open.inter htarget_open
707 have h1W : (1 : G) ∈ W := by
708 constructor
709 · simpa [D] using IsCrossedDifferential.one hDcross
710 · simp only [ContinuousMonoidHom.coe_toMonoidHom, map_one, one_mem, Utarget]
711 rcases hGproC.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hWopen h1W with
712 ⟨V, hVW⟩
713 let i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom :=
714 { source := V
715 target := j
717 intro g hg
718 exact (hVW hg).2 }
719 have hD_eq_of_mem :
720 ∀ a b : G, a⁻¹ * b ∈ (V.1 : Subgroup G) → D a = D b := by
721 intro a b hab
722 have hzero : D (a⁻¹ * b) = 0 := (hVW hab).1
723 have hmul := hDcross a (a⁻¹ * b)
724 have habmul : a * (a⁻¹ * b) = b := by simp only [mul_inv_cancel_left]
725 symm
726 calc
727 D b = D (a * (a⁻¹ * b)) := by rw [habmul]
728 _ = D a + zcCompletedGroupAlgebraScalar C psi.toMonoidHom a •
729 D (a⁻¹ * b) := hmul
730 _ = D a := by rw [hzero, smul_zero, add_zero]
731 let Dstage : zcCompletedDifferentialModuleStageSource C psi.toMonoidHom i →
733 fun q => Quotient.liftOn' q D (by
734 intro a b hab
735 have habi : a⁻¹ * b ∈ (i.source.1 : Subgroup G) := by
736 have hq : (a : G ⧸ (i.source.1 : Subgroup G)) = b := Quotient.sound' hab
737 exact QuotientGroup.eq.1 hq
738 exact hD_eq_of_mem a b (by simpa [i] using habi))
739 have hDstage_cross :
742 Dstage := by
743 intro q r
744 refine QuotientGroup.induction_on q ?_
745 intro a
746 refine QuotientGroup.induction_on r ?_
747 intro b
748 change D (a * b) =
750 (QuotientGroup.mk' (i.source.1 : Subgroup G) a) • D b
751 have hscalar :
753 (QuotientGroup.mk' (i.source.1 : Subgroup G) a) =
755 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom a) := by
757 rfl
758 have h := hDcross a b
759 change D (a * b) =
761 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom a) • D b at h
762 rw [hscalar]
763 exact h
764 let stageCoordFinite :
765 ZCCompletedDifferentialModuleStage C psi.toMonoidHom i →ₗ[
771 Dstage hDstage_cross
772 letI : Module (ZCCompletedGroupAlgebra C H)
773 (ZCCompletedDifferentialModuleStage C psi.toMonoidHom i) :=
774 Module.compHom _ (zcCompletedGroupAlgebraProjectionRingHom C H i.target)
775 let stageCoordLinear :
776 ZCCompletedDifferentialModuleStage C psi.toMonoidHom i →ₗ[
779 {
780 toFun := stageCoordFinite
781 map_add' m n := by
782 exact map_add stageCoordFinite m n
783 map_smul' r m := by
784 change stageCoordFinite
786 (zcCompletedGroupAlgebraProjectionRingHom C H i.target r) • stageCoordFinite m
787 exact map_smul stageCoordFinite
789 }
790 have hcomp :
791 stageCoordLinear.comp
793 coordStage.comp L := by
795 intro g
796 change stageCoordLinear
798 (zcUniversalDifferential C psi.toMonoidHom g)) =
799 coordStage (L (zcUniversalDifferential C psi.toMonoidHom g))
800 calc
801 stageCoordLinear
803 (zcUniversalDifferential C psi.toMonoidHom g)) =
804 stageCoordFinite
807 rfl
808 _ = Dstage (zcCompletedDifferentialModuleStageSourceProj C psi.toMonoidHom i g) := by
809 simp only [ContinuousMonoidHom.coe_toMonoidHom, zcCompletedDifferentialModuleStageDifferential,
812 _ = D g := by
813 rfl
814 _ = coordStage (Dclosed g) := rfl
815 _ = coordStage (L (zcUniversalDifferential C psi.toMonoidHom g)) := by
817 (G := G) (H := H) ProC psi family hfree htarget hφconv
818 hH hφHconv hφHgen g]
819 refine ⟨i, fun m => stageCoordLinear m, ?_⟩
820 intro a
821 have h := congrArg (fun f => f a) hcomp
822 simpa [LinearMap.comp_apply, coordStage, L] using h.symm
824omit [Fintype X] in
825/-- The closed-generated coordinate lift is continuous for the natural finite-stage topology once
826the source is a concrete pro-`C` group. -/
828 (hGproC : ProCGroups.ProC.IsProCGroup ProC.finiteQuotientClass G)
829 (hH : ProC (G := H))
830 (hφHconv :
831 ProCGroups.FreeProC.FamilyConvergesToOne
832 (G := H) (fun i : X => psi (family i)))
833 (hφHgen :
835 (G := H) (Set.range (fun i : X => psi (family i)))) :
836 @Continuous
837 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
838 (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
840 ProC.finiteQuotientClass psi.toMonoidHom)
841 inferInstance
843 (G := G) (H := H) ProC psi family hfree htarget hφconv
844 hH hφHconv hφHgen) :=
846 (G := G) (H := H) ProC psi family hfree htarget hφconv hH hφHconv hφHgen
847 (fun x j =>
849 (G := G) (H := H) ProC psi family hfree htarget hφconv hGproC
850 hH hφHconv hφHgen x j)
852omit [Fintype X] in
853/-- The pre-quotient closed-generated coordinate lift is continuous for the finite-stage
854pre-module topology once the source is a concrete pro-`C` group. -/
856 (hGproC : ProCGroups.ProC.IsProCGroup ProC.finiteQuotientClass G)
857 (hH : ProC (G := H))
858 (hφHconv :
859 ProCGroups.FreeProC.FamilyConvergesToOne
860 (G := H) (fun i : X => psi (family i)))
861 (hφHgen :
863 (G := H) (Set.range (fun i : X => psi (family i)))) :
864 @Continuous
866 (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) G)
867 (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
869 ProC.finiteQuotientClass psi.toMonoidHom)
870 inferInstance
872 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
873 (fun g : G =>
875 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g)) := by
876 let C := ProC.finiteQuotientClass
877 letI : TopologicalSpace
880 letI : TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
882 let Dclosed : G → ZCFreeFoxCoordinates C (X := X) (H := H) :=
883 fun g =>
885 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g
886 let L :=
888 (G := G) (H := H) ProC psi family hfree htarget hφconv hH hφHconv hφHgen
889 let q :
892 ZCFreeFoxCoordinates C (X := X) (H := H) :=
893 L.comp
895 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)).mkQ
896 have hqcont :
897 @Continuous
899 (ZCFreeFoxCoordinates C (X := X) (H := H))
901 inferInstance q := by
902 have hLcont :=
904 (G := G) (H := H) ProC psi family hfree htarget hφconv
905 hGproC hH hφHconv hφHgen
906 have hmk :=
908 C psi.toMonoidHom
909 exact hLcont.comp hmk
910 have hq :
911 q =
913 (R := ZCCompletedGroupAlgebra C H) Dclosed := by
914 apply Finsupp.lhom_ext
915 intro g r
916 have hsingle :
918 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)).mkQ
919 (Finsupp.single g r) :
920 ZCCompletedDifferentialModule C psi.toMonoidHom) =
921 r • zcUniversalDifferential C psi.toMonoidHom g := by
922 rw [← Finsupp.smul_single_one]
923 rfl
924 calc
925 q (Finsupp.single g r) =
927 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)).mkQ
928 (Finsupp.single g r)) := rfl
929 _ = L (r • zcUniversalDifferential C psi.toMonoidHom g) := by
930 rw [hsingle]
931 _ = r • L (zcUniversalDifferential C psi.toMonoidHom g) := by
933 _ = r • Dclosed g := by
935 _ =
937 (R := ZCCompletedGroupAlgebra C H) Dclosed (Finsupp.single g r) := by
939 rw [hq] at hqcont
940 simpa [C, Dclosed] using hqcont
942omit [Fintype X] in
943/-- Closed-generated coordinates as a map out of the separated completed differential module. -/
945 [T1Space (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))]
946 [Nonempty
947 (ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom)]
948 (hdir : Directed (· ≤ ·)
949 (id : ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom →
950 ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom))
951 (hGproC : ProCGroups.ProC.IsProCGroup ProC.finiteQuotientClass G)
952 (hH : ProC (G := H))
953 (hφHconv :
954 ProCGroups.FreeProC.FamilyConvergesToOne
955 (G := H) (fun i : X => psi (family i)))
956 (hφHgen :
958 (G := H) (Set.range (fun i : X => psi (family i)))) :
959 ZCSeparatedCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom →ₗ[
960 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
961 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) := by
962 let C := ProC.finiteQuotientClass
963 let Dclosed : G → ZCFreeFoxCoordinates C (X := X) (H := H) :=
964 fun g =>
966 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g
967 have hright :
969 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv =
970 psi.toMonoidHom :=
972 (ProC := ProC) X H hfree hH (fun i : X => psi (family i)) htarget hφconv
973 hφHconv hφHgen psi (by intro i; rfl)
974 have hclosed_cross :
976 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom) Dclosed := by
977 have hraw :=
979 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv
980 simpa [C, Dclosed, hright] using hraw
981 exact
983 C psi.toMonoidHom hdir Dclosed hclosed_cross
984 (by
985 simpa [C, Dclosed] using
987 (G := G) (H := H) ProC psi family hfree htarget hφconv
988 hGproC hH hφHconv hφHgen)
990omit [Fintype X] in
991@[simp 900]
993 [T1Space (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))]
994 [Nonempty
995 (ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom)]
996 (hdir : Directed (· ≤ ·)
997 (id : ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom →
998 ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom))
999 (hGproC : ProCGroups.ProC.IsProCGroup ProC.finiteQuotientClass G)
1000 (hH : ProC (G := H))
1001 (hφHconv :
1002 ProCGroups.FreeProC.FamilyConvergesToOne
1003 (G := H) (fun i : X => psi (family i)))
1004 (hφHgen :
1006 (G := H) (Set.range (fun i : X => psi (family i))))
1007 (g : G) :
1009 (G := G) (H := H) ProC psi family hfree htarget hφconv
1010 hdir hGproC hH hφHconv hφHgen
1012 ProC.finiteQuotientClass psi.toMonoidHom g) =
1014 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g := by
1015 simp only [ContinuousMonoidHom.coe_toMonoidHom,
1019/-- The separated closed-generated coordinate lift is a left inverse to the separated finite family
1020map. -/
1022 [T1Space (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))]
1023 [Nonempty
1024 (ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom)]
1025 (hdir : Directed (· ≤ ·)
1026 (id : ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom →
1027 ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom))
1028 (hGproC : ProCGroups.ProC.IsProCGroup ProC.finiteQuotientClass G)
1029 (hH : ProC (G := H))
1030 (hφHconv :
1031 ProCGroups.FreeProC.FamilyConvergesToOne
1032 (G := H) (fun i : X => psi (family i)))
1033 (hφHgen :
1035 (G := H) (Set.range (fun i : X => psi (family i)))) :
1037 (G := G) (H := H) ProC psi family hfree htarget hφconv
1038 hdir hGproC hH hφHconv hφHgen).comp
1040 (G := G) (H := H) ProC.finiteQuotientClass psi family) =
1041 LinearMap.id := by
1042 let L :=
1044 (G := G) (H := H) ProC psi family hfree htarget hφconv
1045 hdir hGproC hH hφHconv hφHgen
1046 have hL_family :
1047 ∀ i : X,
1049 ProC.finiteQuotientClass psi.toMonoidHom (family i)) =
1050 Pi.single i (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
1051 intro i
1052 calc
1054 ProC.finiteQuotientClass psi.toMonoidHom (family i)) =
1056 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv
1057 (family i) := by
1058 simpa [L] using
1060 (G := G) (H := H) ProC psi family hfree htarget hφconv
1061 hdir hGproC hH hφHconv hφHgen (family i)
1062 _ = Pi.single i (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
1067 (R := ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)
1068 (generators := fun i : X =>
1070 ProC.finiteQuotientClass psi.toMonoidHom (family i))
1071 L hL_family)
1073/-- The closed-generated coordinate lift is a left inverse to the finite family map. -/
1075 (hH : ProC (G := H))
1076 (hφHconv :
1077 ProCGroups.FreeProC.FamilyConvergesToOne
1078 (G := H) (fun i : X => psi (family i)))
1079 (hφHgen :
1081 (G := H) (Set.range (fun i : X => psi (family i)))) :
1083 (G := G) (H := H) ProC psi family hfree htarget hφconv
1084 hH hφHconv hφHgen).comp
1086 (G := G) (H := H) ProC.finiteQuotientClass psi family) =
1087 LinearMap.id := by
1089 exact
1091 (G := G) (H := H) ProC psi family hfree htarget hφconv
1093 (ProC := ProC) X H hfree hH (fun i : X => psi (family i)) htarget hφconv
1094 hφHconv hφHgen psi (by intro i; rfl))
1096/-- The closed-generated fundamental formula after projection to any finite
1097source/target/coefficient stage.
1099This is the non-circular finite-stage form: both sides are continuous crossed differentials into
1100a finite discrete stage and agree on the topological free generators. It does not assume that the
1101finite-stage projections of `A_psi(C)` separate points. -/
1103 (hH : ProC (G := H))
1104 (hφHconv :
1105 ProCGroups.FreeProC.FamilyConvergesToOne
1106 (G := H) (fun i : X => psi (family i)))
1107 (hφHgen :
1109 (G := H) (Set.range (fun i : X => psi (family i))))
1111 ProC.finiteQuotientClass psi.toMonoidHom)
1112 (g : G) :
1114 ProC.finiteQuotientClass psi.toMonoidHom i
1116 (G := G) (H := H) ProC.finiteQuotientClass psi family
1118 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g)) =
1120 ProC.finiteQuotientClass psi.toMonoidHom i
1121 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) := by
1122 let C := ProC.finiteQuotientClass
1123 let φ : X → H := fun i => psi (family i)
1124 let M :=
1126 (G := G) (H := H) C psi family
1128 let Dclosed : G → ZCFreeFoxCoordinates C (X := X) (H := H) :=
1129 fun g =>
1131 (ProC := ProC) hfree φ htarget hφconv g
1132 let Dstage : G → ZCCompletedDifferentialModuleStage C psi.toMonoidHom i :=
1133 fun g => P (M (Dclosed g))
1134 have hright :
1136 (ProC := ProC) hfree φ htarget hφconv =
1137 psi.toMonoidHom := by
1138 exact
1140 (ProC := ProC) X H hfree hH φ htarget hφconv hφHconv hφHgen psi
1141 (by intro i; rfl)
1142 have hclosed_cross :
1145 Dclosed := by
1146 have hraw :=
1148 (ProC := ProC) hfree φ htarget hφconv
1149 simpa [C, Dclosed, φ, hright] using hraw
1150 have hstage_cross :
1153 Dstage := by
1154 exact IsCrossedDifferential.map_linear hclosed_cross (P.comp M)
1155 have huniv_stage_cross :
1160 have hstage_continuous : Continuous Dstage := by
1161 letI : TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
1163 have hmodule :
1164 @Continuous G
1166 inferInstance
1168 (fun g : G => M (Dclosed g)) := by
1169 simpa [C, φ, M, Dclosed] using
1171 (G := G) (H := H) ProC psi family hfree htarget hφconv)
1172 have hP :
1173 @Continuous
1177 inferInstance P := by
1178 simpa [C, P] using
1180 C psi.toMonoidHom i)
1181 simpa [Dstage, P] using hP.comp hmodule
1182 have huniv_stage_continuous :
1183 Continuous (zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i) := by
1184 letI : TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
1186 have huniv :
1187 @Continuous G
1189 inferInstance
1191 (zcUniversalDifferential C psi.toMonoidHom) :=
1193 have hP :
1194 @Continuous
1198 inferInstance P := by
1199 simpa [C, P] using
1201 C psi.toMonoidHom i)
1202 have hcomp : Continuous (fun g : G => P (zcUniversalDifferential C psi.toMonoidHom g)) :=
1203 hP.comp huniv
1204 have hfun :
1205 (fun g : G => P (zcUniversalDifferential C psi.toMonoidHom g)) =
1207 funext g
1208 simp only [ContinuousMonoidHom.coe_toMonoidHom, zcCompletedDifferentialModuleStageProjection_universal, P]
1209 rw [← hfun]
1210 exact hcomp
1211 have hEq :
1212 Dstage =
1214 refine
1215 IsCrossedDifferential.eq_of_continuous_of_topologicallyGenerates
1216 hstage_cross huniv_stage_cross hstage_continuous huniv_stage_continuous hfree.generates_range ?_
1217 rintro _ ⟨x, rfl⟩
1218 have hDclosed :
1219 Dclosed (family x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
1221 calc
1222 Dstage (family x) =
1223 P (M (Pi.single x (1 : ZCCompletedGroupAlgebra C H))) := by
1224 simp only [ContinuousMonoidHom.coe_toMonoidHom, hDclosed, Dstage]
1225 _ =
1226 P (zcUniversalDifferential C psi.toMonoidHom (family x)) := by
1227 simpa [M] using congrArg P
1229 (G := G) (H := H) C psi family x)
1230 _ =
1232 (family x) := by
1233 simp only [ContinuousMonoidHom.coe_toMonoidHom, zcCompletedDifferentialModuleStageProjection_universal, P]
1234 simpa [Dstage, Dclosed, M, P, C, φ,
1237/-- The separated finite family map is a left inverse to the separated closed-generated coordinate
1238lift. The proof uses only the finite-stage fundamental formula and separated finite-stage
1239projections. -/
1241 [T1Space (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))]
1242 [Nonempty
1243 (ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom)]
1244 (hdir : Directed (· ≤ ·)
1245 (id : ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom →
1246 ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom))
1247 (hGproC : ProCGroups.ProC.IsProCGroup ProC.finiteQuotientClass G)
1248 (hH : ProC (G := H))
1249 (hφHconv :
1250 ProCGroups.FreeProC.FamilyConvergesToOne
1251 (G := H) (fun i : X => psi (family i)))
1252 (hφHgen :
1254 (G := H) (Set.range (fun i : X => psi (family i)))) :
1256 (G := G) (H := H) ProC.finiteQuotientClass psi family).comp
1258 (G := G) (H := H) ProC psi family hfree htarget hφconv
1259 hdir hGproC hH hφHconv hφHgen) =
1260 LinearMap.id := by
1261 let C := ProC.finiteQuotientClass
1262 let Msep :=
1264 (G := G) (H := H) C psi family
1265 let M :=
1267 (G := G) (H := H) C psi family
1268 let Lsep :=
1270 (G := G) (H := H) ProC psi family hfree htarget hφconv
1271 hdir hGproC hH hφHconv hφHgen
1273 intro g
1274 rw [LinearMap.comp_apply]
1275 change Msep (Lsep (zcSeparatedUniversalDifferential C psi.toMonoidHom g)) =
1278 have hzero :
1279 Msep
1281 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) -
1282 zcSeparatedUniversalDifferential C psi.toMonoidHom g = 0 := by
1284 intro i
1285 rw [map_sub, sub_eq_zero]
1286 calc
1288 (Msep
1290 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g)) =
1292 (M
1294 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g)) := by
1295 have hstage :=
1297 (G := G) (H := H) C psi family i
1298 simpa [LinearMap.comp_apply, C, Msep, M] using
1299 congrArg
1300 (fun L : ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[
1305 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g))
1306 hstage
1307 _ =
1309 (zcUniversalDifferential C psi.toMonoidHom g) := by
1310 exact
1312 (G := G) (H := H) ProC psi family hfree htarget hφconv
1313 hH hφHconv hφHgen i g
1314 _ =
1316 (zcSeparatedUniversalDifferential C psi.toMonoidHom g) := by
1317 simp only [ContinuousMonoidHom.coe_toMonoidHom, zcCompletedDifferentialModuleStageProjection_universal,
1319 exact sub_eq_zero.mp hzero
1321/-- Coordinate equivalence for the separated completed differential module, obtained from the
1322closed-generated Fox coordinates without assuming algebraic relation-submodule closedness. -/
1324 [T1Space (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))]
1325 [Nonempty
1326 (ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom)]
1327 (hdir : Directed (· ≤ ·)
1328 (id : ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom →
1329 ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom))
1330 (hGproC : ProCGroups.ProC.IsProCGroup ProC.finiteQuotientClass G)
1331 (hH : ProC (G := H))
1332 (hφHconv :
1333 ProCGroups.FreeProC.FamilyConvergesToOne
1334 (G := H) (fun i : X => psi (family i)))
1335 (hφHgen :
1337 (G := H) (Set.range (fun i : X => psi (family i)))) :
1338 ZCSeparatedCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom
1339 ≃ₗ[ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
1340 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
1341 LinearEquiv.ofLinear
1343 (G := G) (H := H) ProC psi family hfree htarget hφconv
1344 hdir hGproC hH hφHconv hφHgen)
1346 (G := G) (H := H) ProC.finiteQuotientClass psi family)
1348 (G := G) (H := H) ProC psi family hfree htarget hφconv
1349 hdir hGproC hH hφHconv hφHgen)
1351 (G := G) (H := H) ProC psi family hfree htarget hφconv
1352 hdir hGproC hH hφHconv hφHgen)
1355 [T1Space (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))]
1356 [Nonempty
1357 (ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom)]
1358 (hdir : Directed (· ≤ ·)
1359 (id : ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom →
1360 ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom))
1361 (hGproC : ProCGroups.ProC.IsProCGroup ProC.finiteQuotientClass G)
1362 (hH : ProC (G := H))
1363 (hφHconv :
1364 ProCGroups.FreeProC.FamilyConvergesToOne
1365 (G := H) (fun i : X => psi (family i)))
1366 (hφHgen :
1368 (G := H) (Set.range (fun i : X => psi (family i)))) :
1370 (G := G) (H := H) ProC psi family hfree htarget hφconv
1371 hdir hGproC hH hφHconv hφHgen).toLinearMap =
1373 (G := G) (H := H) ProC psi family hfree htarget hφconv
1374 hdir hGproC hH hφHconv hφHgen :=
1375 rfl
1377@[simp 900]
1379 [T1Space (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))]
1380 [Nonempty
1381 (ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom)]
1382 (hdir : Directed (· ≤ ·)
1383 (id : ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom →
1384 ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom))
1385 (hGproC : ProCGroups.ProC.IsProCGroup ProC.finiteQuotientClass G)
1386 (hH : ProC (G := H))
1387 (hφHconv :
1388 ProCGroups.FreeProC.FamilyConvergesToOne
1389 (G := H) (fun i : X => psi (family i)))
1390 (hφHgen :
1392 (G := H) (Set.range (fun i : X => psi (family i))))
1393 (g : G) :
1395 (G := G) (H := H) ProC psi family hfree htarget hφconv
1396 hdir hGproC hH hφHconv hφHgen
1398 ProC.finiteQuotientClass psi.toMonoidHom g) =
1400 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g := by
1401 change
1403 (G := G) (H := H) ProC psi family hfree htarget hφconv
1404 hdir hGproC hH hφHconv hφHgen).toLinearMap
1406 ProC.finiteQuotientClass psi.toMonoidHom g) =
1408 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g
1410 exact
1412 (G := G) (H := H) ProC psi family hfree htarget hφconv
1413 hdir hGproC hH hφHconv hφHgen g
1415/-- Every finite stage projection of `A_psi(C)` factors through the closed-generated coordinate
1416lift.
1418This is a stagewise replacement for the completed fundamental formula: the equality is proved
1419after applying an arbitrary finite stage projection, so no finite-stage separation or closedness
1420of the relation submodule is used. -/
1422 (hH : ProC (G := H))
1423 (hφHconv :
1424 ProCGroups.FreeProC.FamilyConvergesToOne
1425 (G := H) (fun i : X => psi (family i)))
1426 (hφHgen :
1428 (G := H) (Set.range (fun i : X => psi (family i))))
1430 ProC.finiteQuotientClass psi.toMonoidHom) :
1432 ProC.finiteQuotientClass psi.toMonoidHom i =
1434 ProC.finiteQuotientClass psi.toMonoidHom i).comp
1436 (G := G) (H := H) ProC.finiteQuotientClass psi family)).comp
1438 (G := G) (H := H) ProC psi family hfree htarget hφconv
1439 hH hφHconv hφHgen) := by
1441 ProC.finiteQuotientClass psi.toMonoidHom
1442 intro g
1443 simp only [LinearMap.comp_apply]
1445 (G := G) (H := H) ProC psi family hfree htarget hφconv hH hφHconv hφHgen g]
1446 exact
1448 (G := G) (H := H) ProC psi family hfree htarget hφconv
1449 hH hφHconv hφHgen i g).symm
1451/-- Equality of closed-generated coordinates implies equality after every finite stage
1452projection. -/
1454 (hH : ProC (G := H))
1455 (hφHconv :
1456 ProCGroups.FreeProC.FamilyConvergesToOne
1457 (G := H) (fun i : X => psi (family i)))
1458 (hφHgen :
1460 (G := H) (Set.range (fun i : X => psi (family i))))
1462 ProC.finiteQuotientClass psi.toMonoidHom}
1463 (hab :
1465 (G := G) (H := H) ProC psi family hfree htarget hφconv
1466 hH hφHconv hφHgen a =
1468 (G := G) (H := H) ProC psi family hfree htarget hφconv
1469 hH hφHconv hφHgen b)
1471 ProC.finiteQuotientClass psi.toMonoidHom) :
1473 ProC.finiteQuotientClass psi.toMonoidHom i a =
1475 ProC.finiteQuotientClass psi.toMonoidHom i b := by
1476 let P :=
1478 ProC.finiteQuotientClass psi.toMonoidHom i
1479 let M :=
1481 (G := G) (H := H) ProC.finiteQuotientClass psi family
1482 let L :=
1484 (G := G) (H := H) ProC psi family hfree htarget hφconv
1485 hH hφHconv hφHgen
1486 have hfactor :=
1488 (G := G) (H := H) ProC psi family hfree htarget hφconv
1489 hH hφHconv hφHgen i
1490 have hfactor' : P = (P.comp M).comp L := by
1491 simpa [P, M, L] using hfactor
1492 calc
1494 ProC.finiteQuotientClass psi.toMonoidHom i a = ((P.comp M).comp L) a := by
1495 simpa [P, M, L] using congrArg (fun f => f a) hfactor'
1496 _ = ((P.comp M).comp L) b := by
1497 exact congrArg (fun x => (P.comp M) x) (by simpa [L] using hab)
1498 _ =
1500 ProC.finiteQuotientClass psi.toMonoidHom i b := by
1501 simpa [P, M, L] using (congrArg (fun f => f b) hfactor').symm
1503/-- If finite stage projections already separate points, then the closed-generated coordinate lift
1504is injective. The proof uses only the finite-stage fundamental formula above. -/
1506 (hH : ProC (G := H))
1507 (hφHconv :
1508 ProCGroups.FreeProC.FamilyConvergesToOne
1509 (G := H) (fun i : X => psi (family i)))
1510 (hφHgen :
1512 (G := H) (Set.range (fun i : X => psi (family i))))
1513 (hsep :
1515 ProC.finiteQuotientClass psi.toMonoidHom) :
1516 Function.Injective
1518 (G := G) (H := H) ProC psi family hfree htarget hφconv
1519 hH hφHconv hφHgen) := by
1520 intro a b hab
1521 apply hsep
1522 funext i
1526 (G := G) (H := H) ProC psi family hfree htarget hφconv
1527 hH hφHconv hφHgen hab i
1529/-- The completed fundamental formula for the closed-generated Fox coordinates is equivalent to
1530injectivity of the closed-generated coordinate lift `A_psi(C) -> Z_C[[H]]^X`.
1532The forward direction says that the family map and the coordinate lift are inverse linear maps.
1533The reverse direction is the non-circular reduction used in the Morishita-aligned route: since the
1534coordinate lift is already a left inverse to the family map, injectivity forces the formula
1535`Σ_i D_i(g) d x_i = d g` in the algebraic Crowell module. -/
1537 (hH : ProC (G := H))
1538 (hφHconv :
1539 ProCGroups.FreeProC.FamilyConvergesToOne
1540 (G := H) (fun i : X => psi (family i)))
1541 (hφHgen :
1543 (G := H) (Set.range (fun i : X => psi (family i)))) :
1544 (∀ g : G,
1546 (G := G) (H := H) ProC.finiteQuotientClass psi family
1548 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
1549 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) ↔
1550 Function.Injective
1552 (G := G) (H := H) ProC psi family hfree htarget hφconv
1553 hH hφHconv hφHgen) := by
1554 let M :=
1556 (G := G) (H := H) ProC.finiteQuotientClass psi family
1557 let L :=
1559 (G := G) (H := H) ProC psi family hfree htarget hφconv
1560 hH hφHconv hφHgen
1561 have hLM : L.comp M = LinearMap.id := by
1562 simpa [L, M] using
1564 (G := G) (H := H) ProC psi family hfree htarget hφconv
1565 hH hφHconv hφHgen
1566 constructor
1567 · intro hfundamental
1568 have hML : M.comp L = LinearMap.id := by
1570 ProC.finiteQuotientClass psi.toMonoidHom
1571 intro g
1572 calc
1573 (M.comp L)
1574 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) =
1577 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) := by
1578 change
1579 M (L (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)) =
1582 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g)
1584 (G := G) (H := H) ProC psi family hfree htarget hφconv
1585 hH hφHconv hφHgen g]
1586 _ = zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g :=
1587 hfundamental g
1588 _ = LinearMap.id
1589 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) := rfl
1590 intro a b hab
1591 calc
1592 a = (M.comp L) a := by rw [hML]; rfl
1593 _ = M (L a) := rfl
1594 _ = M (L b) := by rw [hab]
1595 _ = (M.comp L) b := rfl
1596 _ = b := by rw [hML]; rfl
1597 · intro hLinj g
1598 apply hLinj
1599 calc
1602 (G := G) (H := H) ProC.finiteQuotientClass psi family
1604 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g)) =
1605 (L.comp M)
1607 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) := rfl
1609 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g := by
1610 rw [hLM]
1611 rfl
1612 _ = L (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) := by
1614 (G := G) (H := H) ProC psi family hfree htarget hφconv
1615 hH hφHconv hφHgen g]
1617omit [Fintype X] in
1618/-- A direct non-circular closedness criterion through the closed-generated coordinate lift.
1620For a pro-`C` source the coordinate lift is continuous for the finite-stage natural topology.
1621Thus injectivity of this lift gives closedness of the defining crossed-differential relation
1622submodule by the general Hausdorff target reflection criterion. -/
1624 (hGproC : ProCGroups.ProC.IsProCGroup ProC.finiteQuotientClass G)
1625 (hH : ProC (G := H))
1626 (hφHconv :
1627 ProCGroups.FreeProC.FamilyConvergesToOne
1628 (G := H) (fun i : X => psi (family i)))
1629 (hφHgen :
1631 (G := H) (Set.range (fun i : X => psi (family i))))
1632 (hcoord_inj :
1633 Function.Injective
1635 (G := G) (H := H) ProC psi family hfree htarget hφconv
1636 hH hφHconv hφHgen)) :
1638 ProC.finiteQuotientClass psi.toMonoidHom := by
1639 exact
1641 ProC.finiteQuotientClass psi.toMonoidHom
1643 (G := G) (H := H) ProC psi family hfree htarget hφconv
1644 hH hφHconv hφHgen)
1645 hcoord_inj
1647 (G := G) (H := H) ProC psi family hfree htarget hφconv
1648 hGproC hH hφHconv hφHgen)
1650/-- On the genuine `A_psi(C)`, the Crowell boundary is obtained by first reading the
1651closed-generated Fox coordinates and then applying the completed Fox boundary. -/
1653 (hH : ProC (G := H))
1654 (hφHconv :
1655 ProCGroups.FreeProC.FamilyConvergesToOne
1656 (G := H) (fun i : X => psi (family i)))
1657 (hφHgen :
1659 (G := H) (Set.range (fun i : X => psi (family i)))) :
1661 (G := G) (H := H) ProC.finiteQuotientClass psi =
1662 (freeProCZCCompletedFoxBoundary ProC.finiteQuotientClass
1663 (fun i : X => psi (family i))).comp
1665 (G := G) (H := H) ProC psi family hfree htarget hφconv
1666 hH hφHconv hφHgen) := by
1667 apply
1669 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass psi.toMonoidHom)
1670 intro g
1671 change
1673 (G := G) (H := H) ProC.finiteQuotientClass psi
1674 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) =
1675 ((freeProCZCCompletedFoxBoundary ProC.finiteQuotientClass
1676 (fun i : X => psi (family i))).comp
1678 (G := G) (H := H) ProC psi family hfree htarget hφconv
1679 hH hφHconv hφHgen))
1680 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)
1682 LinearMap.comp_apply,
1684 have hright :
1686 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv =
1687 psi.toMonoidHom :=
1689 (ProC := ProC) X H hfree hH (fun i : X => psi (family i)) htarget hφconv
1690 hφHconv hφHgen psi (by intro i; rfl)
1691 exact
1693 ProC.finiteQuotientClass hfree.generates_range psi.toMonoidHom
1695 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv)
1696 (by
1697 have hraw :=
1699 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv
1700 simpa [hright] using hraw)
1702 (ProC := ProC) X H hfree (fun i : X => psi (family i)) htarget hφconv)
1703 psi.continuous_toFun
1705 g).symm
1707/-- Closed-generated module-valued fundamental formula from topological uniqueness of continuous
1708crossed differentials.
1710The extra continuity hypotheses are the precise topological input not supplied by the algebraic
1711definition of `ZCCompletedDifferentialModule`: they say that the displayed closed-generated
1712expansion and the universal differential are continuous into a Hausdorff topology on `A_psi(C)`. -/
1715 ProC.finiteQuotientClass psi.toMonoidHom)]
1717 ProC.finiteQuotientClass psi.toMonoidHom)]
1718 (hH : ProC (G := H))
1719 (hφHconv :
1720 ProCGroups.FreeProC.FamilyConvergesToOne
1721 (G := H) (fun i : X => psi (family i)))
1722 (hφHgen :
1724 (G := H) (Set.range (fun i : X => psi (family i))))
1725 (hmodule_continuous :
1726 Continuous
1727 (fun g : G =>
1729 (G := G) (H := H) ProC.finiteQuotientClass psi family
1731 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g)))
1732 (huniv_continuous :
1733 Continuous
1734 (fun g : G =>
1735 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)) :
1736 ∀ g : G,
1738 (G := G) (H := H) ProC.finiteQuotientClass psi family
1740 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
1741 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g := by
1742 let M :=
1744 (G := G) (H := H) ProC.finiteQuotientClass psi family
1745 let φ : X → H := fun i => psi (family i)
1746 let Dclosed : G → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
1748 (ProC := ProC) hfree φ htarget hφconv g
1750 ProC.finiteQuotientClass psi.toMonoidHom :=
1751 fun g => M (Dclosed g)
1752 have hright :
1754 (ProC := ProC) hfree φ htarget hφconv =
1755 psi.toMonoidHom := by
1756 exact
1758 (ProC := ProC) X H hfree hH φ htarget hφconv hφHconv hφHgen psi
1759 (by intro i; rfl)
1760 have hclosed_cross :
1762 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass psi.toMonoidHom)
1763 Dclosed := by
1764 have hraw :=
1766 (ProC := ProC) hfree φ htarget hφconv
1767 simpa [Dclosed, hright] using hraw
1768 have hmodule_cross :
1770 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass psi.toMonoidHom)
1771 Dmodule := by
1772 exact IsCrossedDifferential.map_linear hclosed_cross M
1773 have huniv_cross :
1775 (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass psi.toMonoidHom)
1776 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom) :=
1778 ProC.finiteQuotientClass psi.toMonoidHom
1779 have hEq :
1780 Dmodule =
1781 (fun g : G =>
1782 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) := by
1783 refine
1784 IsCrossedDifferential.eq_of_continuous_of_topologicallyGenerates
1785 hmodule_cross huniv_cross ?_ ?_ hfree.generates_range ?_
1786 · simpa [Dmodule, Dclosed, M, φ] using hmodule_continuous
1787 · simpa using huniv_continuous
1788 · rintro _ ⟨i, rfl⟩
1789 calc
1790 Dmodule (family i) =
1791 M (Pi.single i
1792 (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) := by
1793 simp only [ContinuousMonoidHom.coe_toMonoidHom,
1795 _ = zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom
1796 (family i) := by
1797 simpa [M] using
1799 (G := G) (H := H) ProC.finiteQuotientClass psi family i
1800 intro g
1801 exact congrFun hEq g
1803/-- Natural-topology form of the closed-generated fundamental formula, assuming the finite-stage
1804projections separate points of `A_psi(C)`. -/
1806 (hsep :
1808 ProC.finiteQuotientClass psi.toMonoidHom)
1809 (hH : ProC (G := H))
1810 (hφHconv :
1811 ProCGroups.FreeProC.FamilyConvergesToOne
1812 (G := H) (fun i : X => psi (family i)))
1813 (hφHgen :
1815 (G := H) (Set.range (fun i : X => psi (family i)))) :
1816 ∀ g : G,
1818 (G := G) (H := H) ProC.finiteQuotientClass psi family
1820 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
1821 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g := by
1822 letI : TopologicalSpace
1823 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom) :=
1824 zcCompletedDifferentialModuleNaturalTopology ProC.finiteQuotientClass psi.toMonoidHom
1825 letI : T2Space
1826 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom) :=
1828 ProC.finiteQuotientClass psi.toMonoidHom hsep
1829 exact
1831 (G := G) (H := H) ProC psi family hfree htarget hφconv
1832 hH hφHconv hφHgen
1833 (by
1834 simpa using
1836 (G := G) (H := H) ProC psi family hfree htarget hφconv)
1837 (by
1838 simpa using
1840 ProC.finiteQuotientClass psi.toMonoidHom)
1842/-- For a pro-`C` source, closedness of the algebraic crossed-differential relation submodule is
1843equivalent to injectivity of the closed-generated coordinate lift.
1845This is the precise non-circular frontier left by the Morishita-aligned route. The implication
1846from closedness to injectivity goes through finite-stage separation and the completed fundamental
1847formula. The converse uses only continuity of the coordinate lift for the finite-stage natural
1848topology and the Hausdorff target reflection criterion. -/
1850 [Nonempty
1851 (ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom)]
1852 (hdir : Directed (· ≤ ·)
1853 (id : ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom →
1854 ZCCompletedDifferentialModuleIndex ProC.finiteQuotientClass psi.toMonoidHom))
1855 (hGproC : ProCGroups.ProC.IsProCGroup ProC.finiteQuotientClass G)
1856 (hH : ProC (G := H))
1857 (hφHconv :
1858 ProCGroups.FreeProC.FamilyConvergesToOne
1859 (G := H) (fun i : X => psi (family i)))
1860 (hφHgen :
1862 (G := H) (Set.range (fun i : X => psi (family i)))) :
1864 ProC.finiteQuotientClass psi.toMonoidHom ↔
1865 Function.Injective
1867 (G := G) (H := H) ProC psi family hfree htarget hφconv
1868 hH hφHconv hφHgen) := by
1869 constructor
1870 · intro hclosed
1871 have hsep :
1873 ProC.finiteQuotientClass psi.toMonoidHom :=
1875 ProC.finiteQuotientClass psi.toMonoidHom hdir).1 hclosed
1876 exact
1878 (G := G) (H := H) ProC psi family hfree htarget hφconv
1879 hH hφHconv hφHgen hsep
1880 · intro hcoord_inj
1881 exact
1883 (G := G) (H := H) ProC psi family hfree htarget hφconv
1884 hGproC hH hφHconv hφHgen hcoord_inj
1886/-- Once the closed-generated Fox vector satisfies the universal fundamental formula in
1887`A_psi(C)`, the displayed family differentials form a finite coordinate basis of `A_psi(C)`. -/
1889 (hH : ProC (G := H))
1890 (hφHconv :
1891 ProCGroups.FreeProC.FamilyConvergesToOne
1892 (G := H) (fun i : X => psi (family i)))
1893 (hφHgen :
1895 (G := H) (Set.range (fun i : X => psi (family i))))
1896 (hfundamental :
1897 ∀ g : G,
1899 (G := G) (H := H) ProC.finiteQuotientClass psi family
1901 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
1902 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
1904 (G := G) (H := H) ProC.finiteQuotientClass psi family := by
1905 let M :=
1907 (G := G) (H := H) ProC.finiteQuotientClass psi family
1908 let L :=
1910 (G := G) (H := H) ProC psi family hfree htarget hφconv hH hφHconv hφHgen
1911 have hLM : L.comp M = LinearMap.id := by
1912 exact
1914 (G := G) (H := H) ProC psi family hfree htarget hφconv hH hφHconv hφHgen
1915 have hML : M.comp L = LinearMap.id := by
1916 apply zcCompletedDifferentialModuleHom_ext ProC.finiteQuotientClass psi.toMonoidHom
1917 intro g
1918 calc
1919 (M.comp L) (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) =
1922 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) := by
1923 change
1924 M (L (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)) =
1927 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g)
1929 (G := G) (H := H) ProC psi family hfree htarget hφconv hH hφHconv hφHgen g]
1930 _ = zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g :=
1931 hfundamental g
1932 _ = LinearMap.id
1933 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) := rfl
1934 constructor
1935 · intro x y hxy
1936 have h := congrArg L hxy
1937 calc
1938 x = (L.comp M) x := by rw [hLM]; rfl
1939 _ = L (M x) := rfl
1940 _ = L (M y) := h
1941 _ = (L.comp M) y := rfl
1942 _ = y := by rw [hLM]; rfl
1943 · intro m
1944 refine ⟨L m, ?_⟩
1945 have h := congrArg (fun f => f m) hML
1946 simpa [M, L, LinearMap.comp_apply] using h
1948end ClosedGeneratedCoordinates
1950omit [IsTopologicalGroup G] in
1951/-- A left inverse to a bijective family map is the coordinate inverse associated to the basis. -/
1953 (psi : ContinuousMonoidHom G H)
1954 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G)
1955 (hbasis_A :
1957 (G := G) (H := H) C psi family)
1958 (L :
1961 (hL :
1962 L.comp
1964 (G := G) (H := H) C psi family) =
1965 LinearMap.id) :
1966 L =
1968 (G := G) (H := H) C psi family hbasis_A).toLinearMap := by
1969 let coords :=
1971 (G := G) (H := H) C psi family hbasis_A
1972 let f :=
1974 (G := G) (H := H) C psi family
1975 have hcoords : coords.toLinearMap.comp f = LinearMap.id := by
1976 apply LinearMap.ext
1977 intro x
1978 change coords (coords.symm x) = x
1979 exact coords.apply_symm_apply x
1980 apply LinearMap.ext
1981 intro m
1982 rcases hbasis_A.2 m with ⟨x, hx⟩
1983 rw [← hx]
1984 calc
1985 L (f x) = (L.comp f) x := rfl
1986 _ = x := by
1987 rw [hL]
1988 rfl
1989 _ = (coords.toLinearMap.comp f) x := by
1990 rw [hcoords]
1991 rfl
1992 _ = coords.toLinearMap (f x) := rfl
1994section ClosedGeneratedCoordinateEquiv
1996variable (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
1997variable (psi : ContinuousMonoidHom G H)
1998variable {X : Type u} [Fintype X] [DecidableEq X]
1999variable (family : X → G)
2000variable
2001 (hfree :
2002 ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
2003 (ProC := ProC) X G family)
2004variable
2005 (htarget :
2006 ProC
2007 (G :=
2009 (ProC := ProC) (fun i : X => psi (family i)) : Subgroup
2010 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
2011variable
2012 (hφconv :
2013 ProCGroups.FreeProC.FamilyConvergesToOne
2014 (G :=
2016 (ProC := ProC) (fun i : X => psi (family i)) : Subgroup
2017 (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
2019 (ProC := ProC) (fun i : X => psi (family i))))
2021/-- Coordinate equivalence for `A_psi(C)` obtained from the closed-generated fundamental formula.
2023This is the algebraic packaging step: once the module-valued fundamental formula is proved in the
2024genuine Crowell module, the displayed family map is bijective and its inverse is the
2025closed-generated Fox coordinate map. -/
2027 (hH : ProC (G := H))
2028 (hφHconv :
2029 ProCGroups.FreeProC.FamilyConvergesToOne
2030 (G := H) (fun i : X => psi (family i)))
2031 (hφHgen :
2033 (G := H) (Set.range (fun i : X => psi (family i))))
2034 (hfundamental :
2035 ∀ g : G,
2037 (G := G) (H := H) ProC.finiteQuotientClass psi family
2039 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
2040 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
2041 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom
2042 ≃ₗ[ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
2043 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) :=
2045 (G := G) (H := H) ProC.finiteQuotientClass psi family
2047 (G := G) (H := H) ProC psi family hfree htarget hφconv
2048 hH hφHconv hφHgen hfundamental)
2050/-- The coordinate equivalence from the fundamental formula has the closed-generated coordinate
2051map as its forward linear map. -/
2053 (hH : ProC (G := H))
2054 (hφHconv :
2055 ProCGroups.FreeProC.FamilyConvergesToOne
2056 (G := H) (fun i : X => psi (family i)))
2057 (hφHgen :
2059 (G := H) (Set.range (fun i : X => psi (family i))))
2060 (hfundamental :
2061 ∀ g : G,
2063 (G := G) (H := H) ProC.finiteQuotientClass psi family
2065 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
2066 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
2068 (G := G) (H := H) ProC psi family hfree htarget hφconv
2069 hH hφHconv hφHgen hfundamental).toLinearMap =
2071 (G := G) (H := H) ProC psi family hfree htarget hφconv
2072 hH hφHconv hφHgen := by
2073 let hbasis_A :=
2075 (G := G) (H := H) ProC psi family hfree htarget hφconv
2076 hH hφHconv hφHgen hfundamental
2077 let L :=
2079 (G := G) (H := H) ProC psi family hfree htarget hφconv
2080 hH hφHconv hφHgen
2081 have hleft :
2082 L.comp
2084 (G := G) (H := H) ProC.finiteQuotientClass psi family) =
2085 LinearMap.id :=
2087 (G := G) (H := H) ProC psi family hfree htarget hφconv
2088 hH hφHconv hφHgen
2089 have hL :
2090 L =
2092 (G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A).toLinearMap :=
2094 (G := G) (H := H) ProC.finiteQuotientClass psi family hbasis_A L hleft
2096 hbasis_A, L] using hL.symm
2098/-- Closedness from a completed coordinate equivalence plus pre-quotient coordinate continuity.
2100This is the non-circular direction useful for the remaining completion problem: once the
2101module-valued fundamental formula has been proved by an independent route, it is enough to show
2102that the coordinate map, composed with the algebraic quotient map from the completed pre-module,
2103is continuous for the finite-stage pre-module topology. -/
2105 [T1Space (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))]
2106 (hH : ProC (G := H))
2107 (hφHconv :
2108 ProCGroups.FreeProC.FamilyConvergesToOne
2109 (G := H) (fun i : X => psi (family i)))
2110 (hφHgen :
2112 (G := H) (Set.range (fun i : X => psi (family i))))
2113 (hfundamental :
2114 ∀ g : G,
2116 (G := G) (H := H) ProC.finiteQuotientClass psi family
2118 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
2119 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)
2120 (hprecoord_continuous :
2121 @Continuous
2123 (ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) G)
2124 (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
2126 ProC.finiteQuotientClass psi.toMonoidHom)
2127 inferInstance
2128 (fun x =>
2130 (G := G) (H := H) ProC psi family hfree htarget hφconv
2131 hH hφHconv hφHgen hfundamental).toLinearMap
2134 ProC.finiteQuotientClass psi.toMonoidHom)).mkQ x))) :
2136 ProC.finiteQuotientClass psi.toMonoidHom := by
2137 let e :=
2139 (G := G) (H := H) ProC psi family hfree htarget hφconv
2140 hH hφHconv hφHgen hfundamental
2141 exact
2143 ProC.finiteQuotientClass psi.toMonoidHom e.toLinearMap e.injective hprecoord_continuous
2145/-- Closedness from the closed-generated coordinate equivalence, stated on the quotient
2146finite-stage natural topology.
2148Compared with the pre-quotient criterion above, this uses the already formalized continuity of
2149the algebraic quotient map `pre-module -> A_psi(C)`: it is enough to prove that the coordinate map
2150`A_psi(C) -> Z_C[[H]]^X` is continuous for the natural finite-stage topology on `A_psi(C)`. -/
2152 [T1Space (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))]
2153 (hH : ProC (G := H))
2154 (hφHconv :
2155 ProCGroups.FreeProC.FamilyConvergesToOne
2156 (G := H) (fun i : X => psi (family i)))
2157 (hφHgen :
2159 (G := H) (Set.range (fun i : X => psi (family i))))
2160 (hfundamental :
2161 ∀ g : G,
2163 (G := G) (H := H) ProC.finiteQuotientClass psi family
2165 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
2166 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)
2167 (hcoord_continuous :
2168 @Continuous
2169 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
2170 (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
2172 ProC.finiteQuotientClass psi.toMonoidHom)
2173 inferInstance
2175 (G := G) (H := H) ProC psi family hfree htarget hφconv
2176 hH hφHconv hφHgen hfundamental).toLinearMap) :
2178 ProC.finiteQuotientClass psi.toMonoidHom := by
2179 let e :=
2181 (G := G) (H := H) ProC psi family hfree htarget hφconv
2182 hH hφHconv hφHgen hfundamental
2183 exact
2185 ProC.finiteQuotientClass psi.toMonoidHom e.toLinearMap e.injective hcoord_continuous
2187/-- Closedness from the closed-generated fundamental formula and finite-stage coordinate
2188factorization.
2190The factorization hypothesis is the concrete finite-stage compatibility needed to make the
2191closed-generated coordinate map continuous for the natural topology on the algebraic
2192`A_psi(C)`. -/
2194 [T1Space (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))]
2195 (hH : ProC (G := H))
2196 (hφHconv :
2197 ProCGroups.FreeProC.FamilyConvergesToOne
2198 (G := H) (fun i : X => psi (family i)))
2199 (hφHgen :
2201 (G := H) (Set.range (fun i : X => psi (family i))))
2202 (hfundamental :
2203 ∀ g : G,
2205 (G := G) (H := H) ProC.finiteQuotientClass psi family
2207 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
2208 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
2209 (∀ (x : X) (j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H),
2211 ProC.finiteQuotientClass psi.toMonoidHom,
2212 ∃ stageCoord :
2214 ProC.finiteQuotientClass psi.toMonoidHom i →
2215 ZCCompletedGroupAlgebraStage ProC.finiteQuotientClass H j,
2216 ∀ a :
2217 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom,
2218 zcCompletedGroupAlgebraProjection ProC.finiteQuotientClass H j
2220 (G := G) (H := H) ProC psi family hfree htarget hφconv
2221 hH hφHconv hφHgen a x) =
2222 stageCoord
2224 ProC.finiteQuotientClass psi.toMonoidHom i a)) →
2226 ProC.finiteQuotientClass psi.toMonoidHom := by
2227 intro hfactor
2228 refine
2230 (G := G) (H := H) ProC psi family hfree htarget hφconv
2231 hH hφHconv hφHgen hfundamental ?_
2232 have hcoord :=
2234 (G := G) (H := H) ProC psi family hfree htarget hφconv
2235 hH hφHconv hφHgen hfactor
2236 have hmap :=
2238 (G := G) (H := H) ProC psi family hfree htarget hφconv
2239 hH hφHconv hφHgen hfundamental
2240 simpa [hmap] using hcoord
2242/-- Closedness from the completed fundamental formula once the source is a concrete pro-`C`
2243group.
2245The finite-stage factorization is supplied internally by the open-normal pro-`C` basis of the
2246source, so the only remaining mathematical input is the non-circular module-valued fundamental
2247formula. -/
2249 [T1Space (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))]
2250 (hGproC : ProCGroups.ProC.IsProCGroup ProC.finiteQuotientClass G)
2251 (hH : ProC (G := H))
2252 (hφHconv :
2253 ProCGroups.FreeProC.FamilyConvergesToOne
2254 (G := H) (fun i : X => psi (family i)))
2255 (hφHgen :
2257 (G := H) (Set.range (fun i : X => psi (family i))))
2258 (hfundamental :
2259 ∀ g : G,
2261 (G := G) (H := H) ProC.finiteQuotientClass psi family
2263 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
2264 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
2266 ProC.finiteQuotientClass psi.toMonoidHom :=
2268 (G := G) (H := H) ProC psi family hfree htarget hφconv
2269 hH hφHconv hφHgen hfundamental
2270 (fun x j =>
2272 (G := G) (H := H) ProC psi family hfree htarget hφconv hGproC
2273 hH hφHconv hφHgen x j)
2275@[simp 900]
2277 (hH : ProC (G := H))
2278 (hφHconv :
2279 ProCGroups.FreeProC.FamilyConvergesToOne
2280 (G := H) (fun i : X => psi (family i)))
2281 (hφHgen :
2283 (G := H) (Set.range (fun i : X => psi (family i))))
2284 (hfundamental :
2285 ∀ g : G,
2287 (G := G) (H := H) ProC.finiteQuotientClass psi family
2289 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
2290 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)
2291 (g : G) :
2293 (G := G) (H := H) ProC psi family hfree htarget hφconv
2294 hH hφHconv hφHgen hfundamental
2295 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) =
2297 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g := by
2298 have hmap :=
2299 congrArg
2300 (fun L :
2301 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom
2302 →ₗ[ZCCompletedGroupAlgebra ProC.finiteQuotientClass H]
2303 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) =>
2304 L (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g))
2306 (G := G) (H := H) ProC psi family hfree htarget hφconv
2307 hH hφHconv hφHgen hfundamental)
2308 calc
2310 (G := G) (H := H) ProC psi family hfree htarget hφconv
2311 hH hφHconv hφHgen hfundamental
2312 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)
2315 (G := G) (H := H) ProC psi family hfree htarget hφconv
2316 hH hφHconv hφHgen
2317 (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) := hmap
2318 _ =
2320 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g := by
2322 (G := G) (H := H) ProC psi family hfree htarget hφconv
2323 hH hφHconv hφHgen g
2325/-- The coordinate topology on `A_psi(C)` transported from the closed-generated coordinate
2326equivalence. -/
2328 (hH : ProC (G := H))
2329 (hφHconv :
2330 ProCGroups.FreeProC.FamilyConvergesToOne
2331 (G := H) (fun i : X => psi (family i)))
2332 (hφHgen :
2334 (G := H) (Set.range (fun i : X => psi (family i))))
2335 (hfundamental :
2336 ∀ g : G,
2338 (G := G) (H := H) ProC.finiteQuotientClass psi family
2340 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
2341 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
2342 TopologicalSpace
2343 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom) :=
2344 TopologicalSpace.induced
2346 (G := G) (H := H) ProC psi family hfree htarget hφconv
2347 hH hφHconv hφHgen hfundamental)
2348 inferInstance
2350/-- The closed-generated coordinate equivalence is continuous for the transported coordinate
2351topology on `A_psi(C)`. -/
2353 (hH : ProC (G := H))
2354 (hφHconv :
2355 ProCGroups.FreeProC.FamilyConvergesToOne
2356 (G := H) (fun i : X => psi (family i)))
2357 (hφHgen :
2359 (G := H) (Set.range (fun i : X => psi (family i))))
2360 (hfundamental :
2361 ∀ g : G,
2363 (G := G) (H := H) ProC.finiteQuotientClass psi family
2365 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
2366 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
2367 @Continuous
2368 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
2369 (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
2371 (G := G) (H := H) ProC psi family hfree htarget hφconv
2372 hH hφHconv hφHgen hfundamental)
2373 inferInstance
2375 (G := G) (H := H) ProC psi family hfree htarget hφconv
2376 hH hφHconv hφHgen hfundamental) := by
2377 exact continuous_induced_dom
2379/-- The coordinate topology transported to `A_psi(C)` is Hausdorff. -/
2381 (hH : ProC (G := H))
2382 (hφHconv :
2383 ProCGroups.FreeProC.FamilyConvergesToOne
2384 (G := H) (fun i : X => psi (family i)))
2385 (hφHgen :
2387 (G := H) (Set.range (fun i : X => psi (family i))))
2388 (hfundamental :
2389 ∀ g : G,
2391 (G := G) (H := H) ProC.finiteQuotientClass psi family
2393 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
2394 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
2395 @T2Space
2396 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
2398 (G := G) (H := H) ProC psi family hfree htarget hφconv
2399 hH hφHconv hφHgen hfundamental) := by
2400 letI : TopologicalSpace
2401 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom) :=
2403 (G := G) (H := H) ProC psi family hfree htarget hφconv
2404 hH hφHconv hφHgen hfundamental
2405 let e :=
2407 (G := G) (H := H) ProC psi family hfree htarget hφconv
2408 hH hφHconv hφHgen hfundamental
2409 have hcont : Continuous (e :
2410 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom →
2411 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)) := by
2412 simpa [e] using
2414 (G := G) (H := H) ProC psi family hfree htarget hφconv
2415 hH hφHconv hφHgen hfundamental)
2416 exact T2Space.of_injective_continuous e.injective hcont
2418/-- The inverse of the closed-generated coordinate equivalence is continuous for the transported
2419coordinate topology on `A_psi(C)`. Equivalently, the displayed family map
2420`Z_C[[H]]^X -> A_psi(C)` is continuous for this topology. -/
2422 (hH : ProC (G := H))
2423 (hφHconv :
2424 ProCGroups.FreeProC.FamilyConvergesToOne
2425 (G := H) (fun i : X => psi (family i)))
2426 (hφHgen :
2428 (G := H) (Set.range (fun i : X => psi (family i))))
2429 (hfundamental :
2430 ∀ g : G,
2432 (G := G) (H := H) ProC.finiteQuotientClass psi family
2434 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
2435 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
2436 @Continuous
2437 (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
2438 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
2439 inferInstance
2441 (G := G) (H := H) ProC psi family hfree htarget hφconv
2442 hH hφHconv hφHgen hfundamental)
2444 (G := G) (H := H) ProC psi family hfree htarget hφconv
2445 hH hφHconv hφHgen hfundamental).symm := by
2446 let e :=
2448 (G := G) (H := H) ProC psi family hfree htarget hφconv
2449 hH hφHconv hφHgen hfundamental
2450 rw [continuous_induced_rng]
2451 change Continuous
2452 (fun x : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) =>
2453 e (e.symm x))
2454 have hfun :
2455 (fun x : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) =>
2456 e (e.symm x)) =
2457 (fun x : ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H) => x) := by
2458 funext x
2459 exact e.apply_symm_apply x
2460 rw [hfun]
2461 exact continuous_id
2463/-- The displayed family map is continuous for the coordinate topology transported to
2464`A_psi(C)`. -/
2466 (hH : ProC (G := H))
2467 (hφHconv :
2468 ProCGroups.FreeProC.FamilyConvergesToOne
2469 (G := H) (fun i : X => psi (family i)))
2470 (hφHgen :
2472 (G := H) (Set.range (fun i : X => psi (family i))))
2473 (hfundamental :
2474 ∀ g : G,
2476 (G := G) (H := H) ProC.finiteQuotientClass psi family
2478 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
2479 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
2480 @Continuous
2481 (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
2482 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
2483 inferInstance
2485 (G := G) (H := H) ProC psi family hfree htarget hφconv
2486 hH hφHconv hφHgen hfundamental)
2488 (G := G) (H := H) ProC.finiteQuotientClass psi family) := by
2489 let e :=
2491 (G := G) (H := H) ProC psi family hfree htarget hφconv
2492 hH hφHconv hφHgen hfundamental
2493 change @Continuous
2494 (ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
2495 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
2496 inferInstance
2498 (G := G) (H := H) ProC psi family hfree htarget hφconv
2499 hH hφHconv hφHgen hfundamental)
2501 (G := G) (H := H) ProC.finiteQuotientClass psi family)
2502 have hsymm :
2503 e.symm.toLinearMap =
2505 (G := G) (H := H) ProC.finiteQuotientClass psi family := by
2507 using
2509 (G := G) (H := H) ProC.finiteQuotientClass psi family
2511 (G := G) (H := H) ProC psi family hfree htarget hφconv
2512 hH hφHconv hφHgen hfundamental))
2513 simpa [← hsymm] using
2515 (G := G) (H := H) ProC psi family hfree htarget hφconv
2516 hH hφHconv hφHgen hfundamental)
2518/-- The universal differential `g |-> d g` is continuous for the coordinate topology transported
2519to `A_psi(C)`. -/
2521 (hH : ProC (G := H))
2522 (hφHconv :
2523 ProCGroups.FreeProC.FamilyConvergesToOne
2524 (G := H) (fun i : X => psi (family i)))
2525 (hφHgen :
2527 (G := H) (Set.range (fun i : X => psi (family i))))
2528 (hfundamental :
2529 ∀ g : G,
2531 (G := G) (H := H) ProC.finiteQuotientClass psi family
2533 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
2534 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
2535 @Continuous G
2536 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom)
2537 inferInstance
2539 (G := G) (H := H) ProC psi family hfree htarget hφconv
2540 hH hφHconv hφHgen hfundamental)
2541 (fun g : G => zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) := by
2542 let e :=
2544 (G := G) (H := H) ProC psi family hfree htarget hφconv
2545 hH hφHconv hφHgen hfundamental
2546 rw [continuous_induced_rng]
2547 change Continuous
2548 (fun g : G =>
2549 e (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g))
2550 have hfun :
2551 (fun g : G =>
2552 e (zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g)) =
2553 (fun g : G =>
2555 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) := by
2556 funext g
2557 exact
2559 (G := G) (H := H) ProC psi family hfree htarget hφconv
2560 hH hφHconv hφHgen hfundamental g
2561 rw [hfun]
2562 exact
2564 (ProC := ProC) X H hfree (fun i : X => psi (family i)) htarget hφconv
2566/-- Addition is continuous for the transported coordinate topology on `A_psi(C)`. -/
2568 (hH : ProC (G := H))
2569 (hφHconv :
2570 ProCGroups.FreeProC.FamilyConvergesToOne
2571 (G := H) (fun i : X => psi (family i)))
2572 (hφHgen :
2574 (G := H) (Set.range (fun i : X => psi (family i))))
2575 (hfundamental :
2576 ∀ g : G,
2578 (G := G) (H := H) ProC.finiteQuotientClass psi family
2580 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
2581 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
2582 letI : TopologicalSpace
2583 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom) :=
2585 (G := G) (H := H) ProC psi family hfree htarget hφconv
2586 hH hφHconv hφHgen hfundamental
2587 Continuous (fun p :
2588 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom ×
2589 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom =>
2590 p.1 + p.2) := by
2591 letI : TopologicalSpace
2592 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom) :=
2594 (G := G) (H := H) ProC psi family hfree htarget hφconv
2595 hH hφHconv hφHgen hfundamental
2596 let e :=
2598 (G := G) (H := H) ProC psi family hfree htarget hφconv
2599 hH hφHconv hφHgen hfundamental
2600 have he : Continuous (e :
2601 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom →
2602 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)) := by
2603 simpa [e] using
2605 (G := G) (H := H) ProC psi family hfree htarget hφconv
2606 hH hφHconv hφHgen hfundamental)
2607 rw [continuous_induced_rng]
2608 change Continuous
2609 (fun p :
2610 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom ×
2611 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom =>
2612 e (p.1 + p.2))
2613 simpa [map_add] using (he.comp continuous_fst).add (he.comp continuous_snd)
2615/-- Negation is continuous for the transported coordinate topology on `A_psi(C)`. -/
2617 (hH : ProC (G := H))
2618 (hφHconv :
2619 ProCGroups.FreeProC.FamilyConvergesToOne
2620 (G := H) (fun i : X => psi (family i)))
2621 (hφHgen :
2623 (G := H) (Set.range (fun i : X => psi (family i))))
2624 (hfundamental :
2625 ∀ g : G,
2627 (G := G) (H := H) ProC.finiteQuotientClass psi family
2629 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
2630 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
2631 letI : TopologicalSpace
2632 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom) :=
2634 (G := G) (H := H) ProC psi family hfree htarget hφconv
2635 hH hφHconv hφHgen hfundamental
2636 Continuous
2637 (fun a : ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom => -a) := by
2638 letI : TopologicalSpace
2639 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom) :=
2641 (G := G) (H := H) ProC psi family hfree htarget hφconv
2642 hH hφHconv hφHgen hfundamental
2643 let e :=
2645 (G := G) (H := H) ProC psi family hfree htarget hφconv
2646 hH hφHconv hφHgen hfundamental
2647 have he : Continuous (e :
2648 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom →
2649 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)) := by
2650 simpa [e] using
2652 (G := G) (H := H) ProC psi family hfree htarget hφconv
2653 hH hφHconv hφHgen hfundamental)
2654 rw [continuous_induced_rng]
2655 change Continuous
2656 (fun a : ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom => e (-a))
2657 simpa [map_neg] using he.neg
2659/-- Scalar multiplication is continuous for the transported coordinate topology on `A_psi(C)`. -/
2661 (hH : ProC (G := H))
2662 (hφHconv :
2663 ProCGroups.FreeProC.FamilyConvergesToOne
2664 (G := H) (fun i : X => psi (family i)))
2665 (hφHgen :
2667 (G := H) (Set.range (fun i : X => psi (family i))))
2668 (hfundamental :
2669 ∀ g : G,
2671 (G := G) (H := H) ProC.finiteQuotientClass psi family
2673 (ProC := ProC) hfree (fun i : X => psi (family i)) htarget hφconv g) =
2674 zcUniversalDifferential ProC.finiteQuotientClass psi.toMonoidHom g) :
2675 letI : TopologicalSpace
2676 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom) :=
2678 (G := G) (H := H) ProC psi family hfree htarget hφconv
2679 hH hφHconv hφHgen hfundamental
2680 Continuous
2681 (fun p :
2682 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H ×
2683 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom =>
2684 p.1 • p.2) := by
2685 letI : TopologicalSpace
2686 (ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom) :=
2688 (G := G) (H := H) ProC psi family hfree htarget hφconv
2689 hH hφHconv hφHgen hfundamental
2690 let e :=
2692 (G := G) (H := H) ProC psi family hfree htarget hφconv
2693 hH hφHconv hφHgen hfundamental
2694 have he : Continuous (e :
2695 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom →
2696 ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H)) := by
2697 simpa [e] using
2699 (G := G) (H := H) ProC psi family hfree htarget hφconv
2700 hH hφHconv hφHgen hfundamental)
2701 rw [continuous_induced_rng]
2702 change Continuous
2703 (fun p :
2704 ZCCompletedGroupAlgebra ProC.finiteQuotientClass H ×
2705 ZCCompletedDifferentialModule ProC.finiteQuotientClass psi.toMonoidHom =>
2706 e (p.1 • p.2))
2707 simpa [map_smul] using (continuous_fst.smul (he.comp continuous_snd))
2709end ClosedGeneratedCoordinateEquiv
2711omit [IsTopologicalGroup G] in
2712/-- The displayed Crowell map after the family map is the finite BL map with boundary
2713generators `psi(family i) - 1`. -/
2715 (psi : ContinuousMonoidHom G H)
2716 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G) :
2718 (G := G) (H := H) C psi).comp
2720 (G := G) (H := H) C psi family) =
2723 (fun i : X =>
2725 (G := G) (H := H) C psi (family i)) := by
2726 apply LinearMap.ext
2727 intro x
2730 apply Finset.sum_congr rfl
2731 intro i _hi
2734omit [IsTopologicalGroup G] in
2735/-- The separated displayed Crowell map after the separated family map is the finite BL map with
2736boundary generators `psi(family i) - 1`. -/
2739 (psi : ContinuousMonoidHom G H)
2740 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G) :
2742 (G := G) (H := H) C hC psi).comp
2744 (G := G) (H := H) C psi family) =
2747 (fun i : X =>
2749 (G := G) (H := H) C psi (family i)) := by
2750 apply LinearMap.ext
2751 intro x
2754 apply Finset.sum_congr rfl
2755 intro i _hi
2759omit [IsTopologicalGroup G] in
2760/-- The finite Blanchfield--Lyndon boundary attached to the displayed family is exactly the
2761source-shaped completed Fox boundary for the abstract free group on that family.
2763This removes one layer from the remaining density statement: a BL-coordinate cycle is the same
2764as a vector killed by the completed Fox boundary
2765`zcFreeGroupFoxBoundary C (FreeGroup.lift (fun i => psi (family i)))`. -/
2767 (psi : ContinuousMonoidHom G H)
2768 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G) :
2771 (fun i : X =>
2773 (G := G) (H := H) C psi (family i)) =
2775 C (FreeGroup.lift (fun i : X => psi (family i))) := by
2776 apply LinearMap.ext
2777 intro v
2779 ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.coe_coe, blanchfieldLyndonFiniteFamilyMap_apply, smul_eq_mul,
2780 zcFreeGroupFoxBoundary_apply, FreeGroup.lift_apply_of]
2782omit [IsTopologicalGroup G] in
2783/-- If the pushed-forward finite family topologically generates `H`, the finite BL map is
2784exact at the completed group algebra. -/
2789 (psi : ContinuousMonoidHom G H)
2790 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G)
2791 (hgen :
2793 (G := H) (Set.range (fun i : X => psi (family i)))) :
2794 Function.Exact
2797 (fun i : X =>
2799 (G := G) (H := H) C psi (family i)))
2802 have hfoxExact :
2803 Function.Exact
2804 (FoxDifferential.foxBoundaryMap
2805 (fun i : X => zcGroupLike C H (psi (family i)) - 1) :
2811 (C := C) (hForm := hForm)
2812 (φ := fun i : X => psi (family i)) hgen
2813 have hmap :
2816 (fun i : X =>
2818 (G := G) (H := H) C psi (family i)) =
2819 FoxDifferential.foxBoundaryMap
2820 (fun i : X => zcGroupLike C H (psi (family i)) - 1) := by
2821 ext x
2823 ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.coe_coe, LinearMap.coe_comp, LinearMap.coe_single,
2825 rw [hmap]
2826 exact hfoxExact
2828omit [IsTopologicalGroup G] in
2829/-- Exactness of the finite BL map implies exactness of the displayed Crowell map; no
2830coordinate basis hypothesis is needed in this direction. -/
2833 (psi : ContinuousMonoidHom G H)
2834 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G)
2835 (hbl :
2836 Function.Exact
2839 (fun i : X =>
2841 (G := G) (H := H) C psi (family i)))
2844 Function.Exact
2849 let familyMap :=
2851 (G := G) (H := H) C psi family
2852 let delta :=
2854 (G := G) (H := H) C psi
2855 let blDelta :=
2858 (fun i : X =>
2860 (G := G) (H := H) C psi (family i))
2861 have hcomp : delta.comp familyMap = blDelta :=
2863 (G := G) (H := H) C psi family
2864 have hdelta_family : ∀ x, delta (familyMap x) = blDelta x := by
2865 intro x
2866 simpa [delta, blDelta, familyMap, LinearMap.comp_apply] using
2867 congrArg (fun f => f x) hcomp
2868 intro z
2869 constructor
2870 · intro hz
2871 rcases (hbl z).1 hz with ⟨x, hx⟩
2872 exact ⟨familyMap x, (hdelta_family x).trans hx⟩
2873 · rintro ⟨m, rfl⟩
2874 have hmem :
2876 have hstd :
2880 C H psi.toMonoidHom m
2883 (C := C) (H := H) (x := delta m)).1 hmem
2885omit [IsTopologicalGroup G] in
2886/-- If the pushed-forward finite family topologically generates `H`, then the displayed Crowell
2887map is exact at the completed group algebra. -/
2892 (psi : ContinuousMonoidHom G H)
2893 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G)
2894 (hgen :
2896 (G := H) (Set.range (fun i : X => psi (family i)))) :
2897 Function.Exact
2903 (G := G) (H := H) C psi family
2905 (G := G) (H := H) C hForm psi family hgen)
2907omit [IsTopologicalGroup G] in
2908/-- Exactness of the finite BL map implies exactness of the separated displayed Crowell map at
2909`Z_C[[H]]`. -/
2913 (psi : ContinuousMonoidHom G H)
2914 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G)
2915 (hbl :
2916 Function.Exact
2919 (fun i : X =>
2921 (G := G) (H := H) C psi (family i)))
2924 Function.Exact
2926 (G := G) (H := H) C hC psi :
2931 let familyMap :=
2933 (G := G) (H := H) C psi family
2934 let delta :=
2936 (G := G) (H := H) C hC psi
2937 let blDelta :=
2940 (fun i : X =>
2942 (G := G) (H := H) C psi (family i))
2943 have hcomp : delta.comp familyMap = blDelta :=
2945 (G := G) (H := H) C hC psi family
2946 have hdelta_family : ∀ x, delta (familyMap x) = blDelta x := by
2947 intro x
2948 simpa [delta, blDelta, familyMap, LinearMap.comp_apply] using
2949 congrArg (fun f => f x) hcomp
2950 have hcompleted :
2951 Function.Exact
2953 (G := G) (H := H) C psi :
2958 (G := G) (H := H) C psi family hbl
2959 have htoSep_surj :
2960 Function.Surjective (zcCompletedDifferentialModuleToSeparated C psi.toMonoidHom) := by
2961 intro a
2962 refine Submodule.Quotient.induction_on
2964 (C := fun a =>
2965 ∃ b : ZCCompletedDifferentialModule C psi.toMonoidHom,
2967 a ?_
2968 intro x
2970 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)).mkQ x, ?_⟩
2971 rfl
2972 intro z
2973 constructor
2974 · intro hz
2975 rcases (hbl z).1 hz with ⟨x, hx⟩
2976 exact ⟨familyMap x, (hdelta_family x).trans hx⟩
2977 · rintro ⟨m, rfl⟩
2978 rcases htoSep_surj m with ⟨b, hb⟩
2979 have hdelta_lift :
2980 delta m =
2982 (G := G) (H := H) C psi b := by
2983 rw [← hb]
2984 have hcomp_toSep :=
2985 congrArg (fun f => f b)
2987 (G := G) (H := H) C hC psi)
2988 simpa [delta, LinearMap.comp_apply] using hcomp_toSep
2989 rw [hdelta_lift]
2990 exact
2991 (hcompleted
2993 (G := G) (H := H) C psi b)).2 ⟨b, rfl⟩
2995omit [IsTopologicalGroup G] in
2996/-- If the pushed-forward finite family topologically generates `H`, then the separated
2997displayed Crowell map is exact at the completed group algebra. -/
3003 (psi : ContinuousMonoidHom G H)
3004 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G)
3005 (hgen :
3007 (G := H) (Set.range (fun i : X => psi (family i)))) :
3008 Function.Exact
3010 (G := G) (H := H) C hC psi :
3016 (G := G) (H := H) C hC psi family
3018 (G := G) (H := H) C hForm psi family hgen)
3020omit [IsTopologicalGroup G] in
3021/-- Exactness of the displayed Crowell map implies exactness of the finite BL map as soon as
3022the chosen family map is surjective. Full basis/injectivity is not needed for this implication. -/
3025 (psi : ContinuousMonoidHom G H)
3026 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G)
3027 (hbasis_A_surj :
3028 Function.Surjective
3030 (G := G) (H := H) C psi family))
3031 (hexact_CompletedGroupAlgebra :
3032 Function.Exact
3037 Function.Exact
3040 (fun i : X =>
3042 (G := G) (H := H) C psi (family i)))
3045 let familyMap :=
3047 (G := G) (H := H) C psi family
3048 let delta :=
3050 (G := G) (H := H) C psi
3051 let blDelta :=
3054 (fun i : X =>
3056 (G := G) (H := H) C psi (family i))
3057 have hcomp : delta.comp familyMap = blDelta :=
3059 (G := G) (H := H) C psi family
3060 have hdelta_family : ∀ x, delta (familyMap x) = blDelta x := by
3061 intro x
3062 simpa [delta, blDelta, familyMap, LinearMap.comp_apply] using
3063 congrArg (fun f => f x) hcomp
3064 intro z
3065 constructor
3066 · intro hz
3067 rcases (hexact_CompletedGroupAlgebra z).1 hz with ⟨m, hm⟩
3068 rcases hbasis_A_surj m with ⟨x, hx⟩
3069 refine ⟨x, ?_⟩
3070 calc
3071 blDelta x = delta (familyMap x) := (hdelta_family x).symm
3072 _ = delta m := by rw [hx]
3073 _ = z := hm
3074 · rintro ⟨x, rfl⟩
3075 exact (hexact_CompletedGroupAlgebra (blDelta x)).2 ⟨familyMap x, hdelta_family x⟩
3077omit [IsTopologicalGroup G] in
3078/-- A basis family identifies exactness of the displayed Crowell map with exactness of the
3079finite Blanchfield--Lyndon map obtained by evaluating the displayed boundary on that family. -/
3082 (psi : ContinuousMonoidHom G H)
3083 {X : Type v} [Fintype X] [DecidableEq X] (family : X -> G)
3084 (hbasis_A :
3086 (G := G) (H := H) C psi family) :
3087 Function.Exact
3090 (fun i : X =>
3092 (G := G) (H := H) C psi (family i)))
3095 Function.Exact
3100 constructor
3101 · exact
3103 (G := G) (H := H) C psi family
3104 · exact
3106 (G := G) (H := H) C psi family hbasis_A.2
3108omit [IsTopologicalGroup G] in
3109@[simp]
3111 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H) (n : psi.toMonoidHom.ker) :
3113 (zcUniversalDifferential C psi.toMonoidHom n.1) =
3114 0 := by
3117 (C := C) (H := H) psi.toMonoidHom n.2
3119omit [IsTopologicalGroup G] in
3120@[simp]
3122 (C : ProCGroups.FiniteGroupClass.{u})
3124 (psi : ContinuousMonoidHom G H) (n : psi.toMonoidHom.ker) :
3126 (G := G) (H := H) C hC psi
3127 (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1) =
3128 0 := by
3131 (C := C) (H := H) psi.toMonoidHom n.2
3133end
3135end CrowellExactSequence