Source: ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Basic
1import ProCGroups.FoxDifferential.Completed.Continuous.PresentedCoordinates
2import ProCGroups.FoxDifferential.Completed.Continuous.TopologicalGeneration
4/-!
5# Fox differential: completed — continuous — closed generated coordinates — basic
7The principal declarations in this module are:
9- `closedGeneratedDerivativeCoordinatesLinearMapProCIntegerOfRightHom`
10 The closed-generated Fox vector, read as a crossed differential with the intended scalar \(\psi\),
11 gives a linear map from \(A_{\psi}(C)\) to finite completed Fox coordinates.
12- `closedGeneratedDerivativeCoordinatesLinearMapProCInteger`
13 Closed-generated coordinates with the right component identified by the epimorphic
14 generated-target lifting property.
15- `continuous_closedGenerated_module_expansion_naturalTopology`
16 The closed-generated expansion into \(A_{\psi}(C)\) is continuous for the finite-stage completed
17 topology on \(A_{\psi}(C)\).
18- `closedGeneratedDerivativeCoordinatesLinearMapProCIntegerOfRightHom_universal`
19 Evaluation of the closed-generated coordinate lift on universal differentials.
20-/
22namespace CrowellExactSequence
24noncomputable section
26open scoped BigOperators
27open FoxDifferential
29universe u v w
31variable {G H : Type u}
32variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
33variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
35section ClosedGeneratedCoordinates
37variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
38variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
39variable (C : ProCGroups.FiniteGroupClass.{u})
40variable (psi : ContinuousMonoidHom G H)
41variable {X : Type u} [Fintype X] [DecidableEq X]
42variable (family : X → G)
43variable
44 (hfree :
46 (C := C) X G family)
47variable
48 (htarget :
50 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
51 (C := C) (fun i : X => psi (family i)) : Subgroup
52 (ZCCompletedFoxSemidirect C X H)))
53variable
54 (hφconv :
56 (G :=
57 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
58 (C := C) (fun i : X => psi (family i)) : Subgroup
59 (ZCCompletedFoxSemidirect C X H)))
60 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
61 (C := C) (fun i : X => psi (family i))))
64/--
65The closed-generated expansion into \(A_{\psi}(C)\) is continuous for the finite-stage
66completed topology on \(A_{\psi}(C)\).
67-/
68theorem continuous_closedGenerated_module_expansion_naturalTopology :
69 @Continuous G
70 (ZCCompletedDifferentialModule C psi.toMonoidHom)
71 inferInstance
72 (zcCompletedDifferentialModuleNaturalTopology
73 C psi.toMonoidHom)
74 (fun g : G =>
75 presentedCompletedDifferentialFamilyMapProCInteger
76 (G := G) (H := H) C psi family
77 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
78 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g)) := by
79 letI : TopologicalSpace
80 (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
81 zcCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
82 change Continuous
83 (fun g : G =>
84 presentedCompletedDifferentialFamilyMapProCInteger
85 (G := G) (H := H) C psi family
86 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
87 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g))
88 exact
89 (continuous_presentedCompletedDifferentialFamilyMapProCInteger_naturalTopology
90 (G := G) (H := H) C psi family).comp
91 (continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
92 (C := C) X H hfree (fun i : X => psi (family i)) htarget hφconv)
94/--
95The closed-generated Fox vector, read as a crossed differential with the intended scalar
96\(\psi\), gives a linear map from \(A_{\psi}(C)\) to finite completed Fox coordinates.
97-/
98def closedGeneratedDerivativeCoordinatesLinearMapProCIntegerOfRightHom
99 (hright :
100 freeProCZCCompletedFoxRightHomViaClosedGenerated
101 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv =
102 psi.toMonoidHom) :
103 ZCCompletedDifferentialModule C psi.toMonoidHom →ₗ[
104 ZCCompletedGroupAlgebra C H]
105 ZCFreeFoxCoordinates C (X := X) (H := H) :=
106 crossedHomModuleLift
107 (A := ZCFreeFoxCoordinates C (X := X) (H := H))
108 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
109 { toFun := fun g =>
110 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
111 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g
112 map_mul' := by
113 intro g h
114 rw [← hright]
115 exact
116 ScalarCrossedHom.map_mul
117 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
118 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv)
119 g h }
121omit [Fintype X] in
122/-- Evaluation of the closed-generated coordinate lift on universal differentials. -/
123@[simp]
124theorem closedGeneratedDerivativeCoordinatesLinearMapProCIntegerOfRightHom_universal
125 (hright :
126 freeProCZCCompletedFoxRightHomViaClosedGenerated
127 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv =
128 psi.toMonoidHom)
129 (g : G) :
130 closedGeneratedDerivativeCoordinatesLinearMapProCIntegerOfRightHom
131 (G := G) (H := H) C psi family hfree htarget hφconv hright
132 (zcUniversalDifferential C psi.toMonoidHom g) =
133 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
134 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g := by
135 change
136 crossedHomModuleLift
137 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom) _
138 (universalCrossedDifferential
139 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom) g) =
140 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
141 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g
142 rw [crossedHomModuleLift_universal]
143 rfl
144/-- The closed-generated coordinate lift is a left inverse to the family map. -/
145theorem closedGenDerivativeCoordinatesLinearMapZCOfRightHom_comp_familyMap
146 (hright :
147 freeProCZCCompletedFoxRightHomViaClosedGenerated
148 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv =
149 psi.toMonoidHom) :
150 (closedGeneratedDerivativeCoordinatesLinearMapProCIntegerOfRightHom
151 (G := G) (H := H) C psi family hfree htarget hφconv hright).comp
152 (presentedCompletedDifferentialFamilyMapProCInteger
153 (G := G) (H := H) C psi family) =
154 LinearMap.id := by
155 let L :=
156 closedGeneratedDerivativeCoordinatesLinearMapProCIntegerOfRightHom
157 (G := G) (H := H) C psi family hfree htarget hφconv hright
158 have hL_family :
159 ∀ i : X,
160 L (zcUniversalDifferential C psi.toMonoidHom (family i)) =
161 Pi.single i (1 : ZCCompletedGroupAlgebra C H) := by
162 intro i
163 calc
164 L (zcUniversalDifferential C psi.toMonoidHom (family i)) =
165 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
166 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv
167 (family i) := by
168 simpa [L] using
169 closedGeneratedDerivativeCoordinatesLinearMapProCIntegerOfRightHom_universal
170 (G := G) (H := H) C psi family hfree htarget hφconv hright
171 (family i)
172 _ = Pi.single i (1 : ZCCompletedGroupAlgebra C H) := by
173 simp only [freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_generator]
174 simpa [L, presentedCompletedDifferentialFamilyMapProCInteger,
175 finiteFamilyLinearMap] using
176 (finiteFamilyLinearMap_leftInverse_of_mapsToSingle
177 (R := ZCCompletedGroupAlgebra C H)
178 (generators := fun i : X =>
179 zcUniversalDifferential C psi.toMonoidHom (family i))
180 L hL_family)
182/-- Closed-generated coordinates with the right component identified by the epimorphic
183generated-target lifting property. -/
184def closedGeneratedDerivativeCoordinatesLinearMapProCInteger
185 (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
186 (hφHconv :
188 (G := H) (fun i : X => psi (family i)))
189 (hφHgen :
191 (G := H) (Set.range (fun i : X => psi (family i)))) :
192 ZCCompletedDifferentialModule C psi.toMonoidHom →ₗ[
193 ZCCompletedGroupAlgebra C H]
194 ZCFreeFoxCoordinates C (X := X) (H := H) :=
195 closedGeneratedDerivativeCoordinatesLinearMapProCIntegerOfRightHom
196 (G := G) (H := H) C psi family hfree htarget hφconv
197 (freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom
198 (C := C) X H hfree hH (fun i : X => psi (family i)) htarget hφconv
199 hφHconv hφHgen psi (by intro i; rfl))
201omit [Fintype X] in
202/--
203The closed-generated coordinate map sends the universal completed differential of `g` to the
204closed-generated Fox derivative vector of `g`.
205-/
206@[simp]
207theorem closedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal
208 (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
209 (hφHconv :
211 (G := H) (fun i : X => psi (family i)))
212 (hφHgen :
214 (G := H) (Set.range (fun i : X => psi (family i))))
215 (g : G) :
216 closedGeneratedDerivativeCoordinatesLinearMapProCInteger
217 (G := G) (H := H) C psi family hfree htarget hφconv
218 hH hφHconv hφHgen
219 (zcUniversalDifferential C psi.toMonoidHom g) =
220 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
221 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g := by
222 unfold closedGeneratedDerivativeCoordinatesLinearMapProCInteger
223 exact
224 closedGeneratedDerivativeCoordinatesLinearMapProCIntegerOfRightHom_universal
225 (G := G) (H := H) C psi family hfree htarget hφconv
226 (freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom
227 (C := C) X H hfree hH (fun i : X => psi (family i)) htarget hφconv
228 hφHconv hφHgen psi (by intro i; rfl))
229 g
230omit [Fintype X] in
231/--
232The coordinate map \(A_{\psi}(C) \to \mathbb{Z}_C\llbracket H\rrbracket^{X}\) is continuous for
233the natural finite-stage topology when every finite coefficient coordinate factors through a
234finite source, target, and coefficient stage.
235-/
236theorem continuous_closedGenDerivCoordsZC_of_stageFactorization
237 (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
238 (hφHconv :
240 (G := H) (fun i : X => psi (family i)))
241 (hφHgen :
243 (G := H) (Set.range (fun i : X => psi (family i))))
244 (hfactor :
245 ∀ (x : X) (j : ZCCompletedGroupAlgebraIndex C H),
246 ∃ i : ZCCompletedDifferentialModuleIndex
247 C psi.toMonoidHom,
248 ∃ stageCoord :
249 ZCCompletedDifferentialModuleStage
250 C psi.toMonoidHom i →
251 ZCCompletedGroupAlgebraStage C H j,
252 ∀ a :
253 ZCCompletedDifferentialModule C psi.toMonoidHom,
254 zcCompletedGroupAlgebraProjection C H j
255 (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
256 (G := G) (H := H) C psi family hfree htarget hφconv
257 hH hφHconv hφHgen a x) =
258 stageCoord
259 (zcCompletedDifferentialModuleStageProjection
260 C psi.toMonoidHom i a)) :
261 @Continuous
262 (ZCCompletedDifferentialModule C psi.toMonoidHom)
263 (ZCFreeFoxCoordinates C (X := X) (H := H))
264 (zcCompletedDifferentialModuleNaturalTopology
265 C psi.toMonoidHom)
266 inferInstance
267 (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
268 (G := G) (H := H) C psi family hfree htarget hφconv
269 hH hφHconv hφHgen) := by
270 letI : TopologicalSpace
271 (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
272 zcCompletedDifferentialModuleNaturalTopology
273 C psi.toMonoidHom
274 let L :=
275 closedGeneratedDerivativeCoordinatesLinearMapProCInteger
276 (G := G) (H := H) C psi family hfree htarget hφconv
277 hH hφHconv hφHgen
278 change @Continuous
279 (ZCCompletedDifferentialModule C psi.toMonoidHom)
280 (X → ZCCompletedGroupAlgebra C H)
281 (zcCompletedDifferentialModuleNaturalTopology
282 C psi.toMonoidHom)
283 inferInstance L
284 refine continuous_pi fun x => ?_
285 refine Continuous.subtype_mk (p := ZCCompletedGroupAlgebraCompatible
286 C H) ?_ (fun a => (L a x).property)
287 refine continuous_pi fun j => ?_
288 rcases hfactor x j with ⟨i, stageCoord, hstageCoord⟩
289 letI : TopologicalSpace
290 (ZCCompletedDifferentialModuleStage
291 C psi.toMonoidHom i) := inferInstance
292 letI : DiscreteTopology
293 (ZCCompletedDifferentialModuleStage
294 C psi.toMonoidHom i) := inferInstance
295 have hstage : Continuous stageCoord := continuous_of_discreteTopology
296 have hproj :
297 @Continuous
298 (ZCCompletedDifferentialModule C psi.toMonoidHom)
299 (ZCCompletedDifferentialModuleStage
300 C psi.toMonoidHom i)
301 (zcCompletedDifferentialModuleNaturalTopology
302 C psi.toMonoidHom)
303 inferInstance
304 (zcCompletedDifferentialModuleStageProjection
305 C psi.toMonoidHom i) :=
306 continuous_zcCompletedDifferentialModuleStageProjection_naturalTopology
307 C psi.toMonoidHom i
308 have hcomp : Continuous
309 (fun a :
310 ZCCompletedDifferentialModule C psi.toMonoidHom =>
311 stageCoord
312 (zcCompletedDifferentialModuleStageProjection
313 C psi.toMonoidHom i a)) :=
314 hstage.comp hproj
315 have hfun :
316 (fun a :
317 ZCCompletedDifferentialModule C psi.toMonoidHom =>
318 zcCompletedGroupAlgebraProjection C H j (L a x)) =
319 (fun a :
320 ZCCompletedDifferentialModule C psi.toMonoidHom =>
321 stageCoord
322 (zcCompletedDifferentialModuleStageProjection
323 C psi.toMonoidHom i a)) := by
324 funext a
325 simpa [L] using hstageCoord a
326 change Continuous
327 (fun a :
328 ZCCompletedDifferentialModule C psi.toMonoidHom =>
329 zcCompletedGroupAlgebraProjection C H j (L a x))
330 rw [hfun]
331 exact hcomp
333omit [Fintype X] in
334/--
335Concrete finite-stage factorization of each closed-generated coordinate. For a fixed coordinate
336x and finite coefficient/target stage j, the scalar-valued closed-generated Fox derivative is
337locally unchanged at \(1\) after intersecting with the target kernel. The pro-\(C\) open-normal
338basis supplies a source quotient in the same finite quotient class, and the
339crossed-differential rule descends the coordinate to that quotient.
340-/
341theorem closedGenDerivativeCoordinatesLinearMapZC_stage_factorization_of_hasOpenNormalBasisInClass
342 (hGbasis : ProCGroups.ProC.HasOpenNormalBasisInClass C (G))
343 (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
344 (hφHconv :
346 (G := H) (fun i : X => psi (family i)))
347 (hφHgen :
349 (G := H) (Set.range (fun i : X => psi (family i))))
350 (x : X) (j : ZCCompletedGroupAlgebraIndex C H) :
351 ∃ i : ZCCompletedDifferentialModuleIndex
352 C psi.toMonoidHom,
353 ∃ stageCoord :
354 ZCCompletedDifferentialModuleStage
355 C psi.toMonoidHom i →
356 ZCCompletedGroupAlgebraStage C H j,
357 ∀ a :
358 ZCCompletedDifferentialModule C psi.toMonoidHom,
359 zcCompletedGroupAlgebraProjection C H j
360 (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
361 (G := G) (H := H) C psi family hfree htarget hφconv
362 hH hφHconv hφHgen a x) =
363 stageCoord
364 (zcCompletedDifferentialModuleStageProjection
365 C psi.toMonoidHom i a) := by
366 let C := C
367 let φ : X → H := fun i => psi (family i)
368 let L :=
369 closedGeneratedDerivativeCoordinatesLinearMapProCInteger
370 (G := G) (H := H) C psi family hfree htarget hφconv
371 hH hφHconv hφHgen
372 let coordStage :
373 ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
374 ZCCompletedGroupAlgebraStage C H j :=
375 {
376 toFun v := zcCompletedGroupAlgebraProjection C H j (v x)
377 map_add' v w := by
378 simp only [Pi.add_apply, zcCompletedGroupAlgebraProjection_add]
379 map_smul' r v := by
380 change zcCompletedGroupAlgebraProjection C H j (r * v x) =
381 zcCompletedGroupAlgebraProjection C H j r *
382 zcCompletedGroupAlgebraProjection C H j (v x)
383 exact zcCompletedGroupAlgebraProjection_mul C H j r (v x)
384 }
385 have hright :
386 freeProCZCCompletedFoxRightHomViaClosedGenerated
387 (C := C) hfree φ htarget hφconv =
388 psi.toMonoidHom := by
389 exact
390 freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom
391 (C := C) X H hfree hH φ htarget hφconv hφHconv hφHgen psi
392 (by intro i; rfl)
393 let Dclosed : ScalarCrossedHom
394 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
395 (ZCFreeFoxCoordinates C (X := X) (H := H)) :=
396 { toFun := fun g =>
397 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
398 (C := C) hfree φ htarget hφconv g
399 map_mul' := by
400 intro g h
401 rw [← hright]
402 exact
403 ScalarCrossedHom.map_mul
404 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
405 (C := C) hfree φ htarget hφconv) g h }
406 let D : ScalarCrossedHom
407 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
408 (ZCCompletedGroupAlgebraStage C H j) :=
409 Dclosed.mapLinear coordStage
410 have hDcont : Continuous D := by
411 have hvec :
412 Continuous Dclosed := by
413 change Continuous
414 (fun g : G =>
415 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
416 (C := C) hfree φ htarget hφconv g)
417 exact
418 (continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
419 (C := C) X H hfree φ htarget hφconv)
420 have hcoord : Continuous (fun g : G => Dclosed g x) :=
421 (continuous_apply x).comp hvec
422 have hproj :
423 Continuous (fun a : ZCCompletedGroupAlgebra C H =>
424 zcCompletedGroupAlgebraProjection C H j a) :=
425 continuous_zcCompletedGroupAlgebraProjection C H j
426 change Continuous
427 (fun g : G =>
428 zcCompletedGroupAlgebraProjection C H j (Dclosed g x))
429 exact hproj.comp hcoord
430 let Utarget : OpenNormalSubgroup H := (OrderDual.ofDual j.2).1
431 let W : Set G :=
432 {g : G | D g = 0 ∧ psi.toMonoidHom g ∈ (Utarget : Subgroup H)}
433 have hDzero_open : IsOpen {g : G | D g = 0} := by
434 change IsOpen (D ⁻¹' ({0} : Set (ZCCompletedGroupAlgebraStage C H j)))
435 exact (isOpen_discrete _).preimage hDcont
436 have htarget_open :
437 IsOpen {g : G | psi.toMonoidHom g ∈ (Utarget : Subgroup H)} := by
438 change IsOpen (psi ⁻¹' (((Utarget : Subgroup H) : Set H)))
439 exact (ProCGroups.openNormalSubgroup_isOpen (G := H) Utarget).preimage
440 psi.continuous_toFun
441 have hWopen : IsOpen W := hDzero_open.inter htarget_open
442 have h1W : (1 : G) ∈ W := by
443 constructor
444 · exact ScalarCrossedHom.map_one D
445 · simp only [ContinuousMonoidHom.coe_toMonoidHom, map_one, one_mem, Utarget]
446 rcases hGbasis.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hWopen h1W with
447 ⟨V, hVW⟩
448 let i : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom :=
449 { source := V
450 target := j
451 compatible := by
452 intro g hg
453 exact (hVW hg).2 }
454 have hD_eq_of_mem :
455 ∀ a b : G, a⁻¹ * b ∈ (V.1 : Subgroup G) → D a = D b := by
456 intro a b hab
457 have hzero : D (a⁻¹ * b) = 0 := (hVW hab).1
458 have hmul := ScalarCrossedHom.map_mul D a (a⁻¹ * b)
459 have habmul : a * (a⁻¹ * b) = b := by simp only [mul_inv_cancel_left]
460 symm
461 calc
462 D b = D (a * (a⁻¹ * b)) := by rw [habmul]
463 _ = D a + zcCompletedGroupAlgebraScalar C psi.toMonoidHom a •
464 D (a⁻¹ * b) := hmul
465 _ = D a := by rw [hzero, smul_zero, add_zero]
466 let Dstage : ScalarCrossedHom
467 (zcCompletedDifferentialModuleStageScalar C psi.toMonoidHom i)
468 (ZCCompletedGroupAlgebraStage C H j) :=
469 { toFun := fun q => Quotient.liftOn' q D (by
470 intro a b hab
471 have habi : a⁻¹ * b ∈ (i.source.1 : Subgroup G) := by
472 have hq : (a : G ⧸ (i.source.1 : Subgroup G)) = b := Quotient.sound' hab
473 exact QuotientGroup.eq.1 hq
474 exact hD_eq_of_mem a b (by simpa [i] using habi))
475 map_mul' := by
476 intro q r
477 refine QuotientGroup.induction_on q ?_
478 intro a
479 refine QuotientGroup.induction_on r ?_
480 intro b
481 change D (a * b) =
482 D a + zcCompletedDifferentialModuleStageScalar C psi.toMonoidHom i
483 (QuotientGroup.mk' (i.source.1 : Subgroup G) a) • D b
484 have hscalar :
485 zcCompletedDifferentialModuleStageScalar C psi.toMonoidHom i
486 (QuotientGroup.mk' (i.source.1 : Subgroup G) a) =
487 zcCompletedGroupAlgebraProjectionRingHom C H j
488 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom a) := by
489 dsimp [i, C, zcCompletedGroupAlgebraScalar]
490 rfl
491 have h := ScalarCrossedHom.map_mul D a b
492 change D (a * b) =
493 D a + zcCompletedGroupAlgebraProjectionRingHom C H j
494 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom a) • D b at h
495 rw [hscalar]
496 exact h }
497 let stageCoordFinite :
498 ZCCompletedDifferentialModuleStage C psi.toMonoidHom i →ₗ[
499 zcCompletedDifferentialModuleStageRing C psi.toMonoidHom i]
500 ZCCompletedGroupAlgebraStage C H j :=
501 crossedHomModuleLift
502 (A := ZCCompletedGroupAlgebraStage C H j)
503 (zcCompletedDifferentialModuleStageScalar C psi.toMonoidHom i)
504 Dstage
505 letI : Module (ZCCompletedGroupAlgebra C H)
506 (ZCCompletedDifferentialModuleStage C psi.toMonoidHom i) :=
507 Module.compHom _ (zcCompletedGroupAlgebraProjectionRingHom C H i.target)
508 let stageCoordLinear :
509 ZCCompletedDifferentialModuleStage C psi.toMonoidHom i →ₗ[
510 ZCCompletedGroupAlgebra C H]
511 ZCCompletedGroupAlgebraStage C H j :=
512 {
513 toFun := stageCoordFinite
514 map_add' m n := by
515 exact map_add stageCoordFinite m n
516 map_smul' r m := by
517 change stageCoordFinite
518 ((zcCompletedGroupAlgebraProjectionRingHom C H i.target r) • m) =
519 (zcCompletedGroupAlgebraProjectionRingHom C H i.target r) • stageCoordFinite m
520 exact map_smul stageCoordFinite
521 (zcCompletedGroupAlgebraProjectionRingHom C H i.target r) m
522 }
523 have hcomp :
524 stageCoordLinear.comp
525 (zcCompletedDifferentialModuleStageProjection C psi.toMonoidHom i) =
526 coordStage.comp L := by
527 apply crossedDifferentialModuleHom_ext
528 (A := ZCCompletedGroupAlgebraStage C H j)
529 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
530 intro g
531 change stageCoordLinear
532 (zcCompletedDifferentialModuleStageProjection C psi.toMonoidHom i
533 (zcUniversalDifferential C psi.toMonoidHom g)) =
534 coordStage (L (zcUniversalDifferential C psi.toMonoidHom g))
535 calc
536 stageCoordLinear
537 (zcCompletedDifferentialModuleStageProjection C psi.toMonoidHom i
538 (zcUniversalDifferential C psi.toMonoidHom g)) =
539 stageCoordFinite
540 (zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i g) := by
541 rw [zcCompletedDifferentialModuleStageProjection_universal]
542 rfl
543 _ = Dstage (zcCompletedDifferentialModuleStageSourceProj C psi.toMonoidHom i g) := by
544 change
545 crossedHomModuleLift
546 (zcCompletedDifferentialModuleStageScalar C psi.toMonoidHom i)
547 Dstage
548 (universalCrossedDifferential
549 (zcCompletedDifferentialModuleStageScalar C psi.toMonoidHom i)
550 (zcCompletedDifferentialModuleStageSourceProj
551 C psi.toMonoidHom i g)) =
552 Dstage
553 (zcCompletedDifferentialModuleStageSourceProj C psi.toMonoidHom i g)
554 rw [crossedHomModuleLift_universal]
555 _ = D g := by
556 rfl
557 _ = coordStage (Dclosed g) := rfl
558 _ = coordStage (L (zcUniversalDifferential C psi.toMonoidHom g)) := by
559 change
560 coordStage
561 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
562 (C := C) hfree φ htarget hφconv g) =
563 coordStage (L (zcUniversalDifferential C psi.toMonoidHom g))
564 rw [closedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal
565 (G := G) (H := H) C psi family hfree htarget hφconv
566 hH hφHconv hφHgen g]
567 refine ⟨i, fun m => stageCoordLinear m, ?_⟩
568 intro a
569 have h := congrArg (fun f => f a) hcomp
570 change coordStage (L a) =
571 stageCoordLinear
572 (zcCompletedDifferentialModuleStageProjection C psi.toMonoidHom i a)
573 exact h.symm
575omit [Fintype X] in
576/--
577The closed-generated coordinate lift is continuous for the natural finite-stage topology once
578the source is a concrete pro-\(C\) group.
579-/
580theorem continuous_closedGenDerivativeCoordinatesLinearMapZC_naturalTopology_of_openNormalBasis
581 (hGbasis : ProCGroups.ProC.HasOpenNormalBasisInClass C (G))
582 (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
583 (hφHconv :
585 (G := H) (fun i : X => psi (family i)))
586 (hφHgen :
588 (G := H) (Set.range (fun i : X => psi (family i)))) :
589 @Continuous
590 (ZCCompletedDifferentialModule C psi.toMonoidHom)
591 (ZCFreeFoxCoordinates C (X := X) (H := H))
592 (zcCompletedDifferentialModuleNaturalTopology
593 C psi.toMonoidHom)
594 inferInstance
595 (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
596 (G := G) (H := H) C psi family hfree htarget hφconv
597 hH hφHconv hφHgen) :=
598 continuous_closedGenDerivCoordsZC_of_stageFactorization
599 (G := G) (H := H) C psi family hfree htarget hφconv hH hφHconv hφHgen
600 (fun x j =>
601 closedGenDerivativeCoordinatesLinearMapZC_stage_factorization_of_hasOpenNormalBasisInClass
602 (G := G) (H := H) C psi family hfree htarget hφconv hGbasis
603 hH hφHconv hφHgen x j)
605omit [Fintype X] in
606/--
607The pre-quotient closed-generated coordinate lift is continuous for the finite-stage pre-module
608topology once the source is a concrete pro-\(C\) group.
609-/
610theorem continuous_closedGenDerivativeCoordinatesPreliftZC_naturalTopology_of_openNormalBasis
611 (hGbasis : ProCGroups.ProC.HasOpenNormalBasisInClass C (G))
612 (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
613 (hφHconv :
615 (G := H) (fun i : X => psi (family i)))
616 (hφHgen :
618 (G := H) (Set.range (fun i : X => psi (family i)))) :
619 @Continuous
620 (CrossedDifferentialPreModule
621 (ZCCompletedGroupAlgebra C H) G)
622 (ZCFreeFoxCoordinates C (X := X) (H := H))
623 (zcCompletedDifferentialPreModuleNaturalTopology
624 C psi.toMonoidHom)
625 inferInstance
626 (crossedDifferentialModuleLiftLinear
627 (R := ZCCompletedGroupAlgebra C H)
628 (fun g : G =>
629 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
630 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g)) := by
631 let C := C
632 letI : TopologicalSpace
633 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G) :=
634 zcCompletedDifferentialPreModuleNaturalTopology C psi.toMonoidHom
635 letI : TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
636 zcCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
637 let Dclosed : G → ZCFreeFoxCoordinates C (X := X) (H := H) :=
638 fun g =>
639 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
640 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g
641 let L :=
642 closedGeneratedDerivativeCoordinatesLinearMapProCInteger
643 (G := G) (H := H) C psi family hfree htarget hφconv hH hφHconv hφHgen
644 let q :
645 CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G →ₗ[
646 ZCCompletedGroupAlgebra C H]
647 ZCFreeFoxCoordinates C (X := X) (H := H) :=
648 L.comp
649 (crossedDifferentialRelationSubmodule
650 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)).mkQ
651 have hqcont :
652 @Continuous
653 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
654 (ZCFreeFoxCoordinates C (X := X) (H := H))
655 (zcCompletedDifferentialPreModuleNaturalTopology C psi.toMonoidHom)
656 inferInstance q := by
657 have hLcont :=
658 continuous_closedGenDerivativeCoordinatesLinearMapZC_naturalTopology_of_openNormalBasis
659 (G := G) (H := H) C psi family hfree htarget hφconv
660 hGbasis hH hφHconv hφHgen
661 have hmk :=
662 continuous_zcCompletedDifferentialModule_mkQ_naturalTopology
663 C psi.toMonoidHom
664 exact hLcont.comp hmk
665 have hq :
666 q =
667 crossedDifferentialModuleLiftLinear
668 (R := ZCCompletedGroupAlgebra C H) Dclosed := by
669 apply Finsupp.lhom_ext
670 intro g r
671 have hsingle :
672 ((crossedDifferentialRelationSubmodule
673 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)).mkQ
674 (Finsupp.single g r) :
675 ZCCompletedDifferentialModule C psi.toMonoidHom) =
676 r • zcUniversalDifferential C psi.toMonoidHom g := by
677 rw [← Finsupp.smul_single_one]
678 rfl
679 calc
680 q (Finsupp.single g r) =
681 L ((crossedDifferentialRelationSubmodule
682 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)).mkQ
683 (Finsupp.single g r)) := rfl
684 _ = L (r • zcUniversalDifferential C psi.toMonoidHom g) := by
685 rw [hsingle]
686 _ = r • L (zcUniversalDifferential C psi.toMonoidHom g) := by
687 rw [map_smul]
688 _ = r • Dclosed g := by
689 rw [closedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal]
690 _ =
691 crossedDifferentialModuleLiftLinear
692 (R := ZCCompletedGroupAlgebra C H) Dclosed (Finsupp.single g r) := by
693 rw [crossedDifferentialModuleLiftLinear_single]
694 rw [hq] at hqcont
695 simpa [C, Dclosed] using hqcont
697omit [Fintype X] in
698/-- Closed-generated coordinates as a map out of the separated completed differential module. -/
699def separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger
700 [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
701 [Nonempty
702 (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
703 (hdir : Directed (· ≤ ·)
704 (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
705 ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
706 (hGbasis : ProCGroups.ProC.HasOpenNormalBasisInClass C (G))
707 (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
708 (hφHconv :
710 (G := H) (fun i : X => psi (family i)))
711 (hφHgen :
713 (G := H) (Set.range (fun i : X => psi (family i)))) :
714 ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom →ₗ[
715 ZCCompletedGroupAlgebra C H]
716 ZCFreeFoxCoordinates C (X := X) (H := H) := by
717 let C := C
718 have hright :
719 freeProCZCCompletedFoxRightHomViaClosedGenerated
720 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv =
721 psi.toMonoidHom :=
722 freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom
723 (C := C) X H hfree hH (fun i : X => psi (family i)) htarget hφconv
724 hφHconv hφHgen psi (by intro i; rfl)
725 let Dclosed : ScalarCrossedHom
726 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
727 (ZCFreeFoxCoordinates C (X := X) (H := H)) :=
728 { toFun := fun g =>
729 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
730 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g
731 map_mul' := by
732 intro g h
733 rw [← hright]
734 exact
735 ScalarCrossedHom.map_mul
736 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
737 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv)
738 g h }
739 exact
740 zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift
741 C psi.toMonoidHom hdir Dclosed
742 (by
743 change
744 @Continuous
745 (CrossedDifferentialPreModule (ZCCompletedGroupAlgebra C H) G)
746 (ZCFreeFoxCoordinates C (X := X) (H := H))
747 (zcCompletedDifferentialPreModuleNaturalTopology C psi.toMonoidHom)
748 inferInstance
749 (crossedDifferentialModuleLiftLinear
750 (R := ZCCompletedGroupAlgebra C H)
751 (fun g : G =>
752 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
753 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g))
754 exact
755 continuous_closedGenDerivativeCoordinatesPreliftZC_naturalTopology_of_openNormalBasis
756 (G := G) (H := H) C psi family hfree htarget hφconv
757 hGbasis hH hφHconv hφHgen)
759omit [Fintype X] in
760/--
761The separated closed-generated derivative-coordinate linear map has the stated universal
762property over the pro-\(C\) integers.
763-/
764@[simp 900]
765theorem separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal
766 [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
767 [Nonempty
768 (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
769 (hdir : Directed (· ≤ ·)
770 (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
771 ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
772 (hGbasis : ProCGroups.ProC.HasOpenNormalBasisInClass C (G))
773 (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
774 (hφHconv :
776 (G := H) (fun i : X => psi (family i)))
777 (hφHgen :
779 (G := H) (Set.range (fun i : X => psi (family i))))
780 (g : G) :
781 separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger
782 (G := G) (H := H) C psi family hfree htarget hφconv
783 hdir hGbasis hH hφHconv hφHgen
784 (zcSeparatedUniversalDifferential
785 C psi.toMonoidHom g) =
786 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
787 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g := by
788 unfold separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger
789 exact
790 zcSeparatedCompletedDifferentialModuleLiftOfContinuousPrelift_universal
791 C psi.toMonoidHom hdir _ _ g
793/--
794The separated closed-generated coordinate lift is a left inverse to the separated finite family
795map.
796-/
797theorem separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger_comp_familyMap
798 [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
799 [Nonempty
800 (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
801 (hdir : Directed (· ≤ ·)
802 (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
803 ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
804 (hGbasis : ProCGroups.ProC.HasOpenNormalBasisInClass C (G))
805 (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
806 (hφHconv :
808 (G := H) (fun i : X => psi (family i)))
809 (hφHgen :
811 (G := H) (Set.range (fun i : X => psi (family i)))) :
812 (separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger
813 (G := G) (H := H) C psi family hfree htarget hφconv
814 hdir hGbasis hH hφHconv hφHgen).comp
815 (presentedSeparatedDifferentialFamilyMapProCInteger
816 (G := G) (H := H) C psi family) =
817 LinearMap.id := by
818 let L :=
819 separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger
820 (G := G) (H := H) C psi family hfree htarget hφconv
821 hdir hGbasis hH hφHconv hφHgen
822 have hL_family :
823 ∀ i : X,
824 L (zcSeparatedUniversalDifferential
825 C psi.toMonoidHom (family i)) =
826 Pi.single i (1 : ZCCompletedGroupAlgebra C H) := by
827 intro i
828 calc
829 L (zcSeparatedUniversalDifferential
830 C psi.toMonoidHom (family i)) =
831 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
832 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv
833 (family i) := by
834 simpa [L] using
835 separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal
836 (G := G) (H := H) C psi family hfree htarget hφconv
837 hdir hGbasis hH hφHconv hφHgen (family i)
838 _ = Pi.single i (1 : ZCCompletedGroupAlgebra C H) := by
839 simp only [freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_generator]
840 simpa [L, presentedSeparatedDifferentialFamilyMapProCInteger,
841 finiteFamilyLinearMap] using
842 (finiteFamilyLinearMap_leftInverse_of_mapsToSingle
843 (R := ZCCompletedGroupAlgebra C H)
844 (generators := fun i : X =>
845 zcSeparatedUniversalDifferential
846 C psi.toMonoidHom (family i))
847 L hL_family)
849/--
850Composing the closed-generated derivative-coordinate lift with the completed differential
851family map is the identity.
852-/
853theorem closedGeneratedDerivativeCoordinatesLinearMapProCInteger_comp_familyMap
854 (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
855 (hφHconv :
857 (G := H) (fun i : X => psi (family i)))
858 (hφHgen :
860 (G := H) (Set.range (fun i : X => psi (family i)))) :
861 (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
862 (G := G) (H := H) C psi family hfree htarget hφconv
863 hH hφHconv hφHgen).comp
864 (presentedCompletedDifferentialFamilyMapProCInteger
865 (G := G) (H := H) C psi family) =
866 LinearMap.id := by
867 unfold closedGeneratedDerivativeCoordinatesLinearMapProCInteger
868 exact
869 closedGenDerivativeCoordinatesLinearMapZCOfRightHom_comp_familyMap
870 (G := G) (H := H) C psi family hfree htarget hφconv
871 (freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom
872 (C := C) X H hfree hH (fun i : X => psi (family i)) htarget hφconv
873 hφHconv hφHgen psi (by intro i; rfl))
875/-- The closed-generated fundamental formula after projection to any finite source, target, and
876coefficient stage; no point-separation hypothesis for the stage projections of
877\(A_{\psi}(C)\) is required. -/
878theorem closedGenerated_fundamental_formula_stageProj
879 (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
880 (hφHconv :
882 (G := H) (fun i : X => psi (family i)))
883 (hφHgen :
885 (G := H) (Set.range (fun i : X => psi (family i))))
886 (i : ZCCompletedDifferentialModuleIndex
887 C psi.toMonoidHom)
888 (g : G) :
889 zcCompletedDifferentialModuleStageProjection
890 C psi.toMonoidHom i
891 (presentedCompletedDifferentialFamilyMapProCInteger
892 (G := G) (H := H) C psi family
893 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
894 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g)) =
895 zcCompletedDifferentialModuleStageProjection
896 C psi.toMonoidHom i
897 (zcUniversalDifferential C psi.toMonoidHom g) := by
898 let C := C
899 let φ : X → H := fun i => psi (family i)
900 let M :=
901 presentedCompletedDifferentialFamilyMapProCInteger
902 (G := G) (H := H) C psi family
903 let P := zcCompletedDifferentialModuleStageProjection C psi.toMonoidHom i
904 have hright :
905 freeProCZCCompletedFoxRightHomViaClosedGenerated
906 (C := C) hfree φ htarget hφconv =
907 psi.toMonoidHom := by
908 exact
909 freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom
910 (C := C) X H hfree hH φ htarget hφconv hφHconv hφHgen psi
911 (by intro i; rfl)
912 let Dclosed : ScalarCrossedHom
913 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
914 (ZCFreeFoxCoordinates C (X := X) (H := H)) :=
915 { toFun := fun g =>
916 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
917 (C := C) hfree φ htarget hφconv g
918 map_mul' := by
919 intro g h
920 rw [← hright]
921 exact
922 ScalarCrossedHom.map_mul
923 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
924 (C := C) hfree φ htarget hφconv) g h }
925 let Dstage : ScalarCrossedHom
926 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
927 (ZCCompletedDifferentialModuleStage C psi.toMonoidHom i) :=
928 Dclosed.mapLinear (P.comp M)
929 have hstage_continuous : Continuous Dstage := by
930 letI : TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
931 zcCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
932 have hmodule :
933 @Continuous G
934 (ZCCompletedDifferentialModule C psi.toMonoidHom)
935 inferInstance
936 (zcCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
937 (fun g : G => M (Dclosed g)) := by
938 change Continuous
939 (fun g : G =>
940 presentedCompletedDifferentialFamilyMapProCInteger
941 (G := G) (H := H) C psi family
942 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
943 (C := C) hfree φ htarget hφconv g))
944 exact
945 (continuous_closedGenerated_module_expansion_naturalTopology
946 (G := G) (H := H) C psi family hfree htarget hφconv)
947 have hP :
948 @Continuous
949 (ZCCompletedDifferentialModule C psi.toMonoidHom)
950 (ZCCompletedDifferentialModuleStage C psi.toMonoidHom i)
951 (zcCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
952 inferInstance P := by
953 simpa [C, P] using
954 (continuous_zcCompletedDifferentialModuleStageProjection_naturalTopology
955 C psi.toMonoidHom i)
956 change Continuous (fun g : G => P (M (Dclosed g)))
957 exact hP.comp hmodule
958 have huniv_stage_continuous :
959 Continuous (zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i) := by
960 letI : TopologicalSpace (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
961 zcCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
962 have huniv :
963 @Continuous G
964 (ZCCompletedDifferentialModule C psi.toMonoidHom)
965 inferInstance
966 (zcCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
967 (zcUniversalDifferential C psi.toMonoidHom) :=
968 continuous_zcUniversalDifferential_naturalTopology C psi.toMonoidHom
969 have hP :
970 @Continuous
971 (ZCCompletedDifferentialModule C psi.toMonoidHom)
972 (ZCCompletedDifferentialModuleStage C psi.toMonoidHom i)
973 (zcCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom)
974 inferInstance P := by
975 simpa [C, P] using
976 (continuous_zcCompletedDifferentialModuleStageProjection_naturalTopology
977 C psi.toMonoidHom i)
978 have hcomp : Continuous (fun g : G => P (zcUniversalDifferential C psi.toMonoidHom g)) :=
979 hP.comp huniv
980 have hfun :
981 (fun g : G => P (zcUniversalDifferential C psi.toMonoidHom g)) =
982 zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i := by
983 funext g
984 change
985 zcCompletedDifferentialModuleStageProjection C psi.toMonoidHom i
986 (zcUniversalDifferential C psi.toMonoidHom g) =
987 zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i g
988 exact zcCompletedDifferentialModuleStageProjection_universal
989 C psi.toMonoidHom i g
990 rw [← hfun]
991 exact hcomp
992 have hEq :
993 Dstage =
994 zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i := by
995 refine
996 CrossedHom.eq_of_continuous_of_topologicallyGenerates
997 Dstage
998 (zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i)
999 hstage_continuous huniv_stage_continuous hfree.generates_range ?_
1000 rintro _ ⟨x, rfl⟩
1001 have hDclosed :
1002 Dclosed (family x) = Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
1003 change
1004 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
1005 (C := C) hfree φ htarget hφconv (family x) =
1006 Pi.single x (1 : ZCCompletedGroupAlgebra C H)
1007 exact
1008 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_generator
1009 (C := C) hfree φ htarget hφconv x
1010 calc
1011 Dstage (family x) =
1012 P (M (Pi.single x (1 : ZCCompletedGroupAlgebra C H))) := by
1013 change P (M (Dclosed (family x))) =
1014 P (M (Pi.single x (1 : ZCCompletedGroupAlgebra C H)))
1015 rw [hDclosed]
1016 _ =
1017 P (zcUniversalDifferential C psi.toMonoidHom (family x)) := by
1018 simpa [M] using congrArg P
1019 (presentedCompletedDifferentialFamilyMapProCInteger_single
1020 (G := G) (H := H) C psi family x)
1021 _ =
1022 zcCompletedDifferentialModuleStageDifferential C psi.toMonoidHom i
1023 (family x) := by
1024 change
1025 zcCompletedDifferentialModuleStageProjection C psi.toMonoidHom i
1026 (zcUniversalDifferential C psi.toMonoidHom (family x)) =
1027 zcCompletedDifferentialModuleStageDifferential
1028 C psi.toMonoidHom i (family x)
1029 exact zcCompletedDifferentialModuleStageProjection_universal
1030 C psi.toMonoidHom i (family x)
1031 have hEqg :=
1032 congrArg
1033 (fun d : ScalarCrossedHom
1034 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
1035 (ZCCompletedDifferentialModuleStage C psi.toMonoidHom i) => d g)
1036 hEq
1037 change Dstage g =
1038 P (zcUniversalDifferential C psi.toMonoidHom g)
1039 exact hEqg.trans
1040 (zcCompletedDifferentialModuleStageProjection_universal
1041 C psi.toMonoidHom i g).symm
1043/--
1044The separated finite family map is a left inverse to the separated closed-generated coordinate
1045lift.
1046-/
1047theorem presentedSepDifferentialFamilyMapZC_comp_sepClosedGenDerivativeCoordinatesLinearMapZC
1048 [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
1049 [Nonempty
1050 (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
1051 (hdir : Directed (· ≤ ·)
1052 (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
1053 ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
1054 (hGbasis : ProCGroups.ProC.HasOpenNormalBasisInClass C (G))
1055 (hH : ProCGroups.ProC.HasOpenNormalBasisInClass C (H))
1056 (hφHconv :
1058 (G := H) (fun i : X => psi (family i)))
1059 (hφHgen :
1061 (G := H) (Set.range (fun i : X => psi (family i)))) :
1062 (presentedSeparatedDifferentialFamilyMapProCInteger
1063 (G := G) (H := H) C psi family).comp
1064 (separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger
1065 (G := G) (H := H) C psi family hfree htarget hφconv
1066 hdir hGbasis hH hφHconv hφHgen) =
1067 LinearMap.id := by
1068 let C := C
1069 let Msep :=
1070 presentedSeparatedDifferentialFamilyMapProCInteger
1071 (G := G) (H := H) C psi family
1072 let M :=
1073 presentedCompletedDifferentialFamilyMapProCInteger
1074 (G := G) (H := H) C psi family
1075 let Lsep :=
1076 separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger
1077 (G := G) (H := H) C psi family hfree htarget hφconv
1078 hdir hGbasis hH hφHconv hφHgen
1079 apply zcSeparatedCompletedDifferentialModuleHom_ext C psi.toMonoidHom
1080 intro g
1081 rw [LinearMap.comp_apply]
1082 change Msep (Lsep (zcSeparatedUniversalDifferential C psi.toMonoidHom g)) =
1083 zcSeparatedUniversalDifferential C psi.toMonoidHom g
1084 rw [separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal]
1085 have hzero :
1086 Msep
1087 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
1088 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) -
1089 zcSeparatedUniversalDifferential C psi.toMonoidHom g = 0 := by
1090 apply zcSeparatedCompletedDifferentialModuleStageProjectionsSeparate C psi.toMonoidHom
1091 intro i
1092 rw [map_sub, sub_eq_zero]
1093 calc
1094 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C psi.toMonoidHom i
1095 (Msep
1096 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
1097 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g)) =
1098 zcCompletedDifferentialModuleStageProjection C psi.toMonoidHom i
1099 (M
1100 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
1101 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g)) := by
1102 have hstage :=
1103 zcSepDiffModuleStageProj_comp_presentedSepFamilyMap
1104 (G := G) (H := H) C psi family i
1105 have hstage_at :=
1106 congrArg
1107 (fun L : ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[
1108 ZCCompletedGroupAlgebra C H]
1109 ZCCompletedDifferentialModuleStage C psi.toMonoidHom i =>
1110 L
1111 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
1112 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g))
1113 hstage
1114 change
1115 zcSeparatedCompletedDifferentialModuleStageProjectionAdd
1116 C psi.toMonoidHom i
1117 (Msep
1118 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
1119 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g)) =
1120 zcCompletedDifferentialModuleStageProjection
1121 C psi.toMonoidHom i
1122 (M
1123 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
1124 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g))
1125 at hstage_at
1126 exact hstage_at
1127 _ =
1128 zcCompletedDifferentialModuleStageProjection C psi.toMonoidHom i
1129 (zcUniversalDifferential C psi.toMonoidHom g) := by
1130 exact
1131 closedGenerated_fundamental_formula_stageProj
1132 (G := G) (H := H) C psi family hfree htarget hφconv
1133 hH hφHconv hφHgen i g
1134 _ =
1135 zcSeparatedCompletedDifferentialModuleStageProjectionAdd C psi.toMonoidHom i
1136 (zcSeparatedUniversalDifferential C psi.toMonoidHom g) := by
1137 exact
1138 (zcCompletedDifferentialModuleStageProjection_universal
1139 C psi.toMonoidHom i g).trans
1140 (zcSeparatedCompletedDifferentialModuleStageProjectionAdd_universal
1141 C psi.toMonoidHom i g).symm
1142 exact sub_eq_zero.mp hzero
1144end ClosedGeneratedCoordinates
1146end
1148end CrowellExactSequence