Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Equiv
ProCGroups/FoxDifferential/Completed/Continuous/ClosedGeneratedCoordinates/Equiv/Source

Source: ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Equiv

1import ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Basic
3/-!
4# Fox differential: completed — continuous — closed generated coordinates — equiv
6The principal declarations in this module are:
8- `separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger`
9 Coordinate equivalence for the separated completed differential module, obtained from the
10 closed-generated Fox coordinates without assuming algebraic relation-submodule closedness.
11- `closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula`
12 The closed-generated fundamental formula yields a coordinate equivalence for \(A_{\psi}(C)\); the
13 displayed family map is bijective with inverse given by the closed-generated Fox coordinate map.
14- `separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger_toLinearMap`
15 The linear map underlying the separated closed-generated derivative-coordinate equivalence is the
16 pro-\(C\) integer derivative-coordinate map.
17- `separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger_universal`
18 The separated finite family map is a left inverse to the separated closed-generated coordinate
19 lift.
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]
36variable (C : ProCGroups.FiniteGroupClass.{u})
38section ClosedGeneratedCoordinates
40variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
41variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
42variable (C : ProCGroups.FiniteGroupClass.{u})
43variable (psi : ContinuousMonoidHom G H)
44variable {X : Type u} [Fintype X] [DecidableEq X]
45variable (family : X → G)
46variable
47 (hfree :
49 (C := C) X G family)
50variable
51 (htarget :
53 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
54 (C := C) (fun i : X => psi (family i)) : Subgroup
55 (ZCCompletedFoxSemidirect C X H)))
56variable
57 (hφconv :
59 (G :=
60 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
61 (C := C) (fun i : X => psi (family i)) : Subgroup
62 (ZCCompletedFoxSemidirect C X H)))
63 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
64 (C := C) (fun i : X => psi (family i))))
67/--
68Coordinate equivalence for the separated completed differential module, obtained from the
69closed-generated Fox coordinates without assuming algebraic relation-submodule closedness.
70-/
71def separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger
72 [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
73 [Nonempty
74 (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
75 (hdir : Directed (· ≤ ·)
76 (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
77 ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
80 (hφHconv :
82 (G := H) (fun i : X => psi (family i)))
83 (hφHgen :
85 (G := H) (Set.range (fun i : X => psi (family i)))) :
86 ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom
87 ≃ₗ[ZCCompletedGroupAlgebra C H]
88 ZCFreeFoxCoordinates C (X := X) (H := H) :=
89 LinearEquiv.ofLinear
90 (separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger
91 (G := G) (H := H) C psi family hfree htarget hφconv
92 hdir hGbasis hH hφHconv hφHgen)
93 (presentedSeparatedDifferentialFamilyMapProCInteger
94 (G := G) (H := H) C psi family)
95 (separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger_comp_familyMap
96 (G := G) (H := H) C psi family hfree htarget hφconv
97 hdir hGbasis hH hφHconv hφHgen)
98 (presentedSepDifferentialFamilyMapZC_comp_sepClosedGenDerivativeCoordinatesLinearMapZC
99 (G := G) (H := H) C psi family hfree htarget hφconv
100 hdir hGbasis hH hφHconv hφHgen)
102/--
103The linear map underlying the separated closed-generated derivative-coordinate equivalence is
104the pro-\(C\) integer derivative-coordinate map.
105-/
106theorem separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger_toLinearMap
107 [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
108 [Nonempty
109 (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
110 (hdir : Directed (· ≤ ·)
111 (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
112 ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
115 (hφHconv :
117 (G := H) (fun i : X => psi (family i)))
118 (hφHgen :
120 (G := H) (Set.range (fun i : X => psi (family i)))) :
121 (separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger
122 (G := G) (H := H) C psi family hfree htarget hφconv
123 hdir hGbasis hH hφHconv hφHgen).toLinearMap =
124 separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger
125 (G := G) (H := H) C psi family hfree htarget hφconv
126 hdir hGbasis hH hφHconv hφHgen :=
127 rfl
129/--
130The separated finite family map is a left inverse to the separated closed-generated coordinate
131lift.
132-/
133@[simp 900]
134theorem separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger_universal
135 [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
136 [Nonempty
137 (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
138 (hdir : Directed (· ≤ ·)
139 (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
140 ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
143 (hφHconv :
145 (G := H) (fun i : X => psi (family i)))
146 (hφHgen :
148 (G := H) (Set.range (fun i : X => psi (family i))))
149 (g : G) :
150 separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger
151 (G := G) (H := H) C psi family hfree htarget hφconv
152 hdir hGbasis hH hφHconv hφHgen
153 (zcSeparatedUniversalDifferential
154 C psi.toMonoidHom g) =
155 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
156 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g := by
157 change
158 (separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger
159 (G := G) (H := H) C psi family hfree htarget hφconv
160 hdir hGbasis hH hφHconv hφHgen).toLinearMap
161 (zcSeparatedUniversalDifferential
162 C psi.toMonoidHom g) =
163 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
164 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g
165 rw [separatedClosedGeneratedDerivativeCoordinateLinearEquivProCInteger_toLinearMap]
166 exact
167 separatedClosedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal
168 (G := G) (H := H) C psi family hfree htarget hφconv
169 hdir hGbasis hH hφHconv hφHgen g
171/--
172Every finite-stage projection of \(A_{\psi}(C)\) factors through the closed-generated
173coordinate lift, without assuming finite-stage separation or closedness of the relation
174submodule.
175-/
176theorem zcDiffModuleStageProj_eq_familyMap_comp_closedGenCoord
178 (hφHconv :
180 (G := H) (fun i : X => psi (family i)))
181 (hφHgen :
183 (G := H) (Set.range (fun i : X => psi (family i))))
184 (i : ZCCompletedDifferentialModuleIndex
185 C psi.toMonoidHom) :
186 zcCompletedDifferentialModuleStageProjection
187 C psi.toMonoidHom i =
188 ((zcCompletedDifferentialModuleStageProjection
189 C psi.toMonoidHom i).comp
190 (presentedCompletedDifferentialFamilyMapProCInteger
191 (G := G) (H := H) C psi family)).comp
192 (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
193 (G := G) (H := H) C psi family hfree htarget hφconv
194 hH hφHconv hφHgen) := by
195 apply crossedDifferentialModuleHom_ext
196 (A := ZCCompletedDifferentialModuleStage C psi.toMonoidHom i)
197 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
198 intro g
199 change
200 zcCompletedDifferentialModuleStageProjection C psi.toMonoidHom i
201 (zcUniversalDifferential C psi.toMonoidHom g) =
202 zcCompletedDifferentialModuleStageProjection C psi.toMonoidHom i
203 (presentedCompletedDifferentialFamilyMapProCInteger
204 (G := G) (H := H) C psi family
205 (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
206 (G := G) (H := H) C psi family hfree htarget hφconv
207 hH hφHconv hφHgen
208 (zcUniversalDifferential C psi.toMonoidHom g)))
209 rw [closedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal
210 (G := G) (H := H) C psi family hfree htarget hφconv hH hφHconv hφHgen g]
211 exact
212 (closedGenerated_fundamental_formula_stageProj
213 (G := G) (H := H) C psi family hfree htarget hφconv
214 hH hφHconv hφHgen i g).symm
216omit [Fintype X] in
217/--
218Equality of closed-generated coordinates implies equality after every finite stage projection.
219-/
220theorem zcCompletedDifferentialModuleStageProjection_eq_of_closedGeneratedCoordinate_eq
221 [Finite X]
223 (hφHconv :
225 (G := H) (fun i : X => psi (family i)))
226 (hφHgen :
228 (G := H) (Set.range (fun i : X => psi (family i))))
229 {a b : ZCCompletedDifferentialModule
230 C psi.toMonoidHom}
231 (hab :
232 closedGeneratedDerivativeCoordinatesLinearMapProCInteger
233 (G := G) (H := H) C psi family hfree htarget hφconv
234 hH hφHconv hφHgen a =
235 closedGeneratedDerivativeCoordinatesLinearMapProCInteger
236 (G := G) (H := H) C psi family hfree htarget hφconv
237 hH hφHconv hφHgen b)
238 (i : ZCCompletedDifferentialModuleIndex
239 C psi.toMonoidHom) :
240 zcCompletedDifferentialModuleStageProjection
241 C psi.toMonoidHom i a =
242 zcCompletedDifferentialModuleStageProjection
243 C psi.toMonoidHom i b := by
244 letI : Fintype X := Fintype.ofFinite X
245 let P :=
246 zcCompletedDifferentialModuleStageProjection
247 C psi.toMonoidHom i
248 let M :=
249 presentedCompletedDifferentialFamilyMapProCInteger
250 (G := G) (H := H) C psi family
251 let L :=
252 closedGeneratedDerivativeCoordinatesLinearMapProCInteger
253 (G := G) (H := H) C psi family hfree htarget hφconv
254 hH hφHconv hφHgen
255 have hfactor :=
256 zcDiffModuleStageProj_eq_familyMap_comp_closedGenCoord
257 (G := G) (H := H) C psi family hfree htarget hφconv
258 hH hφHconv hφHgen i
259 have hfactor' : P = (P.comp M).comp L := by
260 simpa [P, M, L] using hfactor
261 calc
262 zcCompletedDifferentialModuleStageProjection
263 C psi.toMonoidHom i a = ((P.comp M).comp L) a := by
264 simpa [P, M, L] using congrArg (fun f => f a) hfactor'
265 _ = ((P.comp M).comp L) b := by
266 exact congrArg (fun x => (P.comp M) x) (by simpa [L] using hab)
267 _ =
268 zcCompletedDifferentialModuleStageProjection
269 C psi.toMonoidHom i b := by
270 simpa [P, M, L] using (congrArg (fun f => f b) hfactor').symm
272omit [Fintype X] in
273/--
274If finite stage projections already separate points, then the closed-generated coordinate lift
275is injective.
276-/
277theorem closedGenDerivativeCoordinatesLinearMapZC_inj_of_stageProjsSeparate
278 [Finite X]
280 (hφHconv :
282 (G := H) (fun i : X => psi (family i)))
283 (hφHgen :
285 (G := H) (Set.range (fun i : X => psi (family i))))
286 (hsep :
287 zcCompletedDifferentialModuleStageProjectionsSeparate
288 C psi.toMonoidHom) :
289 Function.Injective
290 (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
291 (G := G) (H := H) C psi family hfree htarget hφconv
292 hH hφHconv hφHgen) := by
293 letI : Fintype X := Fintype.ofFinite X
294 intro a b hab
295 apply hsep
296 funext i
297 change
298 zcCompletedDifferentialModuleStageProjection C psi.toMonoidHom i a =
299 zcCompletedDifferentialModuleStageProjection C psi.toMonoidHom i b
300 exact
301 zcCompletedDifferentialModuleStageProjection_eq_of_closedGeneratedCoordinate_eq
302 (G := G) (H := H) C psi family hfree htarget hφconv
303 hH hφHconv hφHgen hab i
305/--
306The completed fundamental formula for the closed-generated Fox coordinates is equivalent to
307injectivity of the closed-generated coordinate lift \(A_{\psi}(C) \to \mathbb{Z}_C\llbracket
308H\rrbracket^{X}\). The forward direction says that the family map and the coordinate lift are
309inverse linear maps. The reverse direction is the non-circular reduction used in the
310Morishita-aligned route: since the coordinate lift is already a left inverse to the family map,
311injectivity forces the formula \(\sum_i D_i(g) d x_i = d g\) in the algebraic Crowell module.
312-/
313theorem closedGenerated_fundamental_formula_iff_closedGeneratedCoordinate_injective
314 {C : ProCGroups.FiniteGroupClass.{u}}
315 {psi : ContinuousMonoidHom G H}
316 {family : X → G}
317 {hfree htarget hφconv}
319 (hφHconv :
321 (G := H) (fun i : X => psi (family i)))
322 (hφHgen :
324 (G := H) (Set.range (fun i : X => psi (family i)))) :
325 (∀ g : G,
326 presentedCompletedDifferentialFamilyMapProCInteger
327 (G := G) (H := H) C psi family
328 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
329 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
330 zcUniversalDifferential C psi.toMonoidHom g) ↔
331 Function.Injective
332 (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
333 (G := G) (H := H) (C := C) (psi := psi) (family := family)
334 (hfree := hfree) (htarget := htarget) (hφconv := hφconv)
335 hH hφHconv hφHgen) := by
336 let M :=
337 presentedCompletedDifferentialFamilyMapProCInteger
338 (G := G) (H := H) C psi family
339 let L :=
340 closedGeneratedDerivativeCoordinatesLinearMapProCInteger
341 (G := G) (H := H) C psi family hfree htarget hφconv
342 hH hφHconv hφHgen
343 have hLM : L.comp M = LinearMap.id := by
344 simpa [L, M] using
345 closedGeneratedDerivativeCoordinatesLinearMapProCInteger_comp_familyMap
346 (G := G) (H := H) C psi family hfree htarget hφconv
347 hH hφHconv hφHgen
348 constructor
349 · intro hfundamental
350 have hML : M.comp L = LinearMap.id := by
351 apply crossedDifferentialModuleHom_ext
352 (A := ZCCompletedDifferentialModule C psi.toMonoidHom)
353 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
354 intro g
355 calc
356 (M.comp L)
357 (zcUniversalDifferential C psi.toMonoidHom g) =
358 M
359 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
360 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) := by
361 change
362 M (L (zcUniversalDifferential C psi.toMonoidHom g)) =
363 M
364 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
365 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g)
366 rw [closedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal
367 (G := G) (H := H) C psi family hfree htarget hφconv
368 hH hφHconv hφHgen g]
369 _ = zcUniversalDifferential C psi.toMonoidHom g :=
370 hfundamental g
371 _ = LinearMap.id
372 (zcUniversalDifferential C psi.toMonoidHom g) := rfl
373 intro a b hab
374 calc
375 a = (M.comp L) a := by rw [hML]; rfl
376 _ = M (L a) := rfl
377 _ = M (L b) := by rw [hab]
378 _ = (M.comp L) b := rfl
379 _ = b := by rw [hML]; rfl
380 · intro hLinj g
381 apply hLinj
382 calc
383 L
384 (presentedCompletedDifferentialFamilyMapProCInteger
385 (G := G) (H := H) C psi family
386 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
387 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g)) =
388 (L.comp M)
389 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
390 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) := rfl
391 _ = freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
392 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g := by
393 rw [hLM]
394 rfl
395 _ = L (zcUniversalDifferential C psi.toMonoidHom g) := by
396 rw [closedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal
397 (G := G) (H := H) C psi family hfree htarget hφconv
398 hH hφHconv hφHgen g]
400omit [Fintype X] in
401/--
402A direct non-circular closedness criterion through the closed-generated coordinate lift. For a
403pro-\(C\) source the coordinate lift is continuous for the finite-stage natural topology. Thus
404injectivity of this lift gives closedness of the defining crossed-differential relation
405submodule by the general Hausdorff target reflection criterion.
406-/
407theorem zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_hasOpenNormalBasisInClass_of_inj
410 (hφHconv :
412 (G := H) (fun i : X => psi (family i)))
413 (hφHgen :
415 (G := H) (Set.range (fun i : X => psi (family i))))
416 (hcoord_inj :
417 Function.Injective
418 (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
419 (G := G) (H := H) C psi family hfree htarget hφconv
420 hH hφHconv hφHgen)) :
421 zcCompletedDifferentialModuleRelationSubmoduleClosed
422 C psi.toMonoidHom := by
423 exact
424 zcDiffModuleRelSubmoduleClosed_of_inj_continuous_naturalTopology
425 C psi.toMonoidHom
426 (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
427 (G := G) (H := H) C psi family hfree htarget hφconv
428 hH hφHconv hφHgen)
429 hcoord_inj
430 (continuous_closedGenDerivativeCoordinatesLinearMapZC_naturalTopology_of_openNormalBasis
431 (G := G) (H := H) C psi family hfree htarget hφconv
432 hGbasis hH hφHconv hφHgen)
434/--
435Closed-generated module-valued fundamental formula from topological uniqueness of continuous
436crossed differentials. The extra continuity hypotheses are the precise topological input not
437supplied by the algebraic definition of the \(\mathbb{Z}_C\)-completed differential module:
438they say that the displayed closed-generated expansion and the universal differential are
439continuous into a Hausdorff topology on \(A_{\psi}(C)\).
440-/
441theorem closedGenerated_fundamental_formula_of_continuous
442 [TopologicalSpace (ZCCompletedDifferentialModule
443 C psi.toMonoidHom)]
444 [T2Space (ZCCompletedDifferentialModule
445 C psi.toMonoidHom)]
447 (hφHconv :
449 (G := H) (fun i : X => psi (family i)))
450 (hφHgen :
452 (G := H) (Set.range (fun i : X => psi (family i))))
453 (hmodule_continuous :
454 Continuous
455 (fun g : G =>
456 presentedCompletedDifferentialFamilyMapProCInteger
457 (G := G) (H := H) C psi family
458 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
459 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g)))
460 (huniv_continuous :
461 Continuous
462 (fun g : G =>
463 zcUniversalDifferential C psi.toMonoidHom g)) :
464 ∀ g : G,
465 presentedCompletedDifferentialFamilyMapProCInteger
466 (G := G) (H := H) C psi family
467 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
468 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
469 zcUniversalDifferential C psi.toMonoidHom g := by
470 let M :=
471 presentedCompletedDifferentialFamilyMapProCInteger
472 (G := G) (H := H) C psi family
473 let φ : X → H := fun i => psi (family i)
474 have hright :
475 freeProCZCCompletedFoxRightHomViaClosedGenerated
476 (C := C) hfree φ htarget hφconv =
477 psi.toMonoidHom := by
478 exact
479 freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom
480 (C := C) X H hfree hH φ htarget hφconv hφHconv hφHgen psi
481 (by intro i; rfl)
482 let Dclosed : ScalarCrossedHom
483 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
484 (ZCFreeFoxCoordinates C (X := X) (H := H)) :=
485 { toFun := fun g =>
486 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
487 (C := C) hfree φ htarget hφconv g
488 map_mul' := by
489 intro a b
490 rw [← hright]
491 exact
492 ScalarCrossedHom.map_mul
493 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
494 (C := C) hfree φ htarget hφconv) a b }
495 let Dmodule : ScalarCrossedHom
496 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
497 (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
498 Dclosed.mapLinear M
499 have hEq :
500 Dmodule =
501 zcUniversalDifferential C psi.toMonoidHom := by
502 refine
503 CrossedHom.eq_of_continuous_of_topologicallyGenerates
504 Dmodule (zcUniversalDifferential C psi.toMonoidHom)
505 ?_ ?_ hfree.generates_range ?_
506 · change Continuous (fun g : G => M (Dclosed g))
507 exact hmodule_continuous
508 · simpa using huniv_continuous
509 · rintro _ ⟨i, rfl⟩
510 calc
511 Dmodule (family i) =
512 M (Pi.single i
513 (1 : ZCCompletedGroupAlgebra C H)) := by
514 change
515 M
516 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
517 (C := C) hfree φ htarget hφconv (family i)) =
518 M (Pi.single i (1 : ZCCompletedGroupAlgebra C H))
519 rw [freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated_generator]
520 _ = zcUniversalDifferential C psi.toMonoidHom
521 (family i) := by
522 simpa [M] using
523 presentedCompletedDifferentialFamilyMapProCInteger_single
524 (G := G) (H := H) C psi family i
525 intro g
526 exact congrArg
527 (fun d : ScalarCrossedHom
528 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
529 (ZCCompletedDifferentialModule C psi.toMonoidHom) => d g)
530 hEq
532/--
533Natural-topology form of the closed-generated fundamental formula, assuming the finite-stage
534projections separate points of \(A_{\psi}(C)\).
535-/
536theorem closedGenerated_fundamental_formula_naturalTopology_of_separating
537 (hsep :
538 zcCompletedDifferentialModuleStageProjectionsSeparate
539 C psi.toMonoidHom)
541 (hφHconv :
543 (G := H) (fun i : X => psi (family i)))
544 (hφHgen :
546 (G := H) (Set.range (fun i : X => psi (family i)))) :
547 ∀ g : G,
548 presentedCompletedDifferentialFamilyMapProCInteger
549 (G := G) (H := H) C psi family
550 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
551 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
552 zcUniversalDifferential C psi.toMonoidHom g := by
553 letI : TopologicalSpace
554 (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
555 zcCompletedDifferentialModuleNaturalTopology C psi.toMonoidHom
556 letI : T2Space
557 (ZCCompletedDifferentialModule C psi.toMonoidHom) :=
558 t2Space_zcCompletedDifferentialModuleNaturalTopology_of_separating
559 C psi.toMonoidHom hsep
560 exact
561 closedGenerated_fundamental_formula_of_continuous
562 (G := G) (H := H) C psi family hfree htarget hφconv
563 hH hφHconv hφHgen
564 (by
565 simpa using
566 continuous_closedGenerated_module_expansion_naturalTopology
567 (G := G) (H := H) C psi family hfree htarget hφconv)
568 (by
569 simpa using
570 continuous_zcUniversalDifferential_naturalTopology
571 C psi.toMonoidHom)
573omit [Fintype X] in
574/--
575For a pro-\(C\) source, closedness of the algebraic crossed-differential relation submodule is
576equivalent to injectivity of the closed-generated coordinate lift. This is the precise
577non-circular frontier left by the Morishita-aligned route. The implication from closedness to
578injectivity goes through finite-stage separation and the completed fundamental formula. The
579converse uses only continuity of the coordinate lift for the finite-stage natural topology and
580the Hausdorff target reflection criterion.
581-/
582theorem zcDiffModuleRelSubmoduleClosed_iff_closedGenCoord_inj_of_hasOpenNormalBasisInClass
583 {C : ProCGroups.FiniteGroupClass.{u}}
584 {psi : ContinuousMonoidHom G H}
585 (family : X → G) (hfree htarget hφconv) [Finite X]
586 [Nonempty
587 (ZCCompletedDifferentialModuleIndex C psi.toMonoidHom)]
588 (hdir : Directed (· ≤ ·)
589 (id : ZCCompletedDifferentialModuleIndex C psi.toMonoidHom →
590 ZCCompletedDifferentialModuleIndex C psi.toMonoidHom))
593 (hφHconv :
595 (G := H) (fun i : X => psi (family i)))
596 (hφHgen :
598 (G := H) (Set.range (fun i : X => psi (family i)))) :
599 zcCompletedDifferentialModuleRelationSubmoduleClosed
600 C psi.toMonoidHom ↔
601 Function.Injective
602 (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
603 (G := G) (H := H) (C := C) (psi := psi) (family := family)
604 (hfree := hfree) (htarget := htarget) (hφconv := hφconv)
605 hH hφHconv hφHgen) := by
606 letI : Fintype X := Fintype.ofFinite X
607 constructor
608 · intro hclosed
609 have hsep :
610 zcCompletedDifferentialModuleStageProjectionsSeparate
611 C psi.toMonoidHom :=
612 (zcDiffModuleRelSubmoduleClosed_iff_stageProjsSeparate
613 (C := C) (ψ := psi.toMonoidHom) hdir).1 hclosed
614 exact
615 closedGenDerivativeCoordinatesLinearMapZC_inj_of_stageProjsSeparate
616 (G := G) (H := H) C psi family hfree htarget hφconv
617 hH hφHconv hφHgen hsep
618 · intro hcoord_inj
619 exact
620 zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_hasOpenNormalBasisInClass_of_inj
621 (G := G) (H := H) C psi family hfree htarget hφconv
622 hGbasis hH hφHconv hφHgen hcoord_inj
624/--
625Once the closed-generated Fox vector satisfies the universal fundamental formula in
626\(A_{\psi}(C)\), the displayed family differentials form a finite coordinate basis of
627\(A_{\psi}(C)\).
628-/
629theorem isPresentedCompletedDifferentialFamilyBasisZC_of_closedGen_fundFormula
631 (hφHconv :
633 (G := H) (fun i : X => psi (family i)))
634 (hφHgen :
636 (G := H) (Set.range (fun i : X => psi (family i))))
637 (hfundamental :
638 ∀ g : G,
639 presentedCompletedDifferentialFamilyMapProCInteger
640 (G := G) (H := H) C psi family
641 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
642 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
643 zcUniversalDifferential C psi.toMonoidHom g) :
644 IsPresentedCompletedDifferentialFamilyBasisProCInteger
645 (G := G) (H := H) C psi family := by
646 let M :=
647 presentedCompletedDifferentialFamilyMapProCInteger
648 (G := G) (H := H) C psi family
649 let L :=
650 closedGeneratedDerivativeCoordinatesLinearMapProCInteger
651 (G := G) (H := H) C psi family hfree htarget hφconv hH hφHconv hφHgen
652 have hLM : L.comp M = LinearMap.id := by
653 exact
654 closedGeneratedDerivativeCoordinatesLinearMapProCInteger_comp_familyMap
655 (G := G) (H := H) C psi family hfree htarget hφconv hH hφHconv hφHgen
656 have hML : M.comp L = LinearMap.id := by
657 apply crossedDifferentialModuleHom_ext
658 (A := ZCCompletedDifferentialModule C psi.toMonoidHom)
659 (zcCompletedGroupAlgebraScalar C psi.toMonoidHom)
660 intro g
661 calc
662 (M.comp L) (zcUniversalDifferential C psi.toMonoidHom g) =
663 M
664 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
665 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) := by
666 change
667 M (L (zcUniversalDifferential C psi.toMonoidHom g)) =
668 M
669 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
670 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g)
671 rw [closedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal
672 (G := G) (H := H) C psi family hfree htarget hφconv hH hφHconv hφHgen g]
673 _ = zcUniversalDifferential C psi.toMonoidHom g :=
674 hfundamental g
675 _ = LinearMap.id
676 (zcUniversalDifferential C psi.toMonoidHom g) := rfl
677 constructor
678 · intro x y hxy
679 have h := congrArg L hxy
680 calc
681 x = (L.comp M) x := by rw [hLM]; rfl
682 _ = L (M x) := rfl
683 _ = L (M y) := h
684 _ = (L.comp M) y := rfl
685 _ = y := by rw [hLM]; rfl
686 · intro m
687 refine ⟨L m, ?_⟩
688 have h := congrArg (fun f => f m) hML
689 change M (L m) = m at h
690 exact h
693end ClosedGeneratedCoordinates
695omit [IsTopologicalGroup G] in
696/-- A left inverse to a bijective family map is the coordinate inverse associated to the basis. -/
697theorem presentedCompletedDifferentialFamilyCoordinatesProCInteger_eq_of_leftInverse
698 (psi : ContinuousMonoidHom G H)
699 {X : Type v} [Fintype X] (family : X -> G)
700 (hbasis_A :
701 IsPresentedCompletedDifferentialFamilyBasisProCInteger
702 (G := G) (H := H) C psi family)
703 (L :
704 ZCCompletedDifferentialModule C psi.toMonoidHom →ₗ[ZCCompletedGroupAlgebra C H]
705 (X → ZCCompletedGroupAlgebra C H))
706 (hL :
707 L.comp
708 (presentedCompletedDifferentialFamilyMapProCInteger
709 (G := G) (H := H) C psi family) =
710 LinearMap.id) :
711 L =
712 (presentedCompletedDifferentialFamilyCoordinatesProCInteger
713 (G := G) (H := H) C psi family hbasis_A).toLinearMap := by
714 let coords :=
715 presentedCompletedDifferentialFamilyCoordinatesProCInteger
716 (G := G) (H := H) C psi family hbasis_A
717 let f :=
718 presentedCompletedDifferentialFamilyMapProCInteger
719 (G := G) (H := H) C psi family
720 have hcoords : coords.toLinearMap.comp f = LinearMap.id := by
721 apply LinearMap.ext
722 intro x
723 change coords (coords.symm x) = x
724 exact coords.apply_symm_apply x
725 apply LinearMap.ext
726 intro m
727 rcases hbasis_A.2 m with ⟨x, hx⟩
728 rw [← hx]
729 calc
730 L (f x) = (L.comp f) x := rfl
731 _ = x := by
732 rw [hL]
733 rfl
734 _ = (coords.toLinearMap.comp f) x := by
735 rw [hcoords]
736 rfl
737 _ = coords.toLinearMap (f x) := rfl
739section ClosedGeneratedCoordinateEquiv
741variable [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
742variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
743variable (C : ProCGroups.FiniteGroupClass.{u})
744variable (psi : ContinuousMonoidHom G H)
745variable {X : Type u} [Fintype X] [DecidableEq X]
746variable (family : X → G)
747variable
748 (hfree :
750 (C := C) X G family)
751variable
752 (htarget :
754 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
755 (C := C) (fun i : X => psi (family i)) : Subgroup
756 (ZCCompletedFoxSemidirect C X H)))
757variable
758 (hφconv :
760 (G :=
761 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
762 (C := C) (fun i : X => psi (family i)) : Subgroup
763 (ZCCompletedFoxSemidirect C X H)))
764 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
765 (C := C) (fun i : X => psi (family i))))
768/--
769The closed-generated fundamental formula yields a coordinate equivalence for \(A_{\psi}(C)\);
770the displayed family map is bijective with inverse given by the closed-generated Fox coordinate
771map.
772-/
773def closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
775 (hφHconv :
777 (G := H) (fun i : X => psi (family i)))
778 (hφHgen :
780 (G := H) (Set.range (fun i : X => psi (family i))))
781 (hfundamental :
782 ∀ g : G,
783 presentedCompletedDifferentialFamilyMapProCInteger
784 (G := G) (H := H) C psi family
785 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
786 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
787 zcUniversalDifferential C psi.toMonoidHom g) :
788 ZCCompletedDifferentialModule C psi.toMonoidHom
789 ≃ₗ[ZCCompletedGroupAlgebra C H]
790 ZCFreeFoxCoordinates C (X := X) (H := H) :=
791 presentedCompletedDifferentialFamilyCoordinatesProCInteger
792 (G := G) (H := H) C psi family
793 (isPresentedCompletedDifferentialFamilyBasisZC_of_closedGen_fundFormula
794 (G := G) (H := H) C psi family hfree htarget hφconv
795 hH hφHconv hφHgen hfundamental)
797/--
798The coordinate equivalence from the fundamental formula has the closed-generated coordinate map
799as its forward linear map.
800-/
801theorem closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula_toLinearMap
803 (hφHconv :
805 (G := H) (fun i : X => psi (family i)))
806 (hφHgen :
808 (G := H) (Set.range (fun i : X => psi (family i))))
809 (hfundamental :
810 ∀ g : G,
811 presentedCompletedDifferentialFamilyMapProCInteger
812 (G := G) (H := H) C psi family
813 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
814 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
815 zcUniversalDifferential C psi.toMonoidHom g) :
816 (closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
817 (G := G) (H := H) C psi family hfree htarget hφconv
818 hH hφHconv hφHgen hfundamental).toLinearMap =
819 closedGeneratedDerivativeCoordinatesLinearMapProCInteger
820 (G := G) (H := H) C psi family hfree htarget hφconv
821 hH hφHconv hφHgen := by
822 let hbasis_A :=
823 isPresentedCompletedDifferentialFamilyBasisZC_of_closedGen_fundFormula
824 (G := G) (H := H) C psi family hfree htarget hφconv
825 hH hφHconv hφHgen hfundamental
826 let L :=
827 closedGeneratedDerivativeCoordinatesLinearMapProCInteger
828 (G := G) (H := H) C psi family hfree htarget hφconv
829 hH hφHconv hφHgen
830 have hleft :
831 L.comp
832 (presentedCompletedDifferentialFamilyMapProCInteger
833 (G := G) (H := H) C psi family) =
834 LinearMap.id :=
835 closedGeneratedDerivativeCoordinatesLinearMapProCInteger_comp_familyMap
836 (G := G) (H := H) C psi family hfree htarget hφconv
837 hH hφHconv hφHgen
838 have hL :
839 L =
840 (presentedCompletedDifferentialFamilyCoordinatesProCInteger
841 (G := G) (H := H) C psi family hbasis_A).toLinearMap :=
842 presentedCompletedDifferentialFamilyCoordinatesProCInteger_eq_of_leftInverse
843 (G := G) (H := H) C psi family hbasis_A L hleft
844 simpa [closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula,
845 hbasis_A, L] using hL.symm
847/--
848A completed coordinate equivalence and continuity of the coordinate map composed with the
849algebraic quotient map imply closedness for the finite-stage pre-module topology.
850-/
851theorem zcDiffModuleRelSubmoduleClosed_of_closedGenCoordPrequotient_continuous_of_fundFormula
852 [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
854 (hφHconv :
856 (G := H) (fun i : X => psi (family i)))
857 (hφHgen :
859 (G := H) (Set.range (fun i : X => psi (family i))))
860 (hfundamental :
861 ∀ g : G,
862 presentedCompletedDifferentialFamilyMapProCInteger
863 (G := G) (H := H) C psi family
864 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
865 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
866 zcUniversalDifferential C psi.toMonoidHom g)
867 (hprecoord_continuous :
868 @Continuous
869 (CrossedDifferentialPreModule
870 (ZCCompletedGroupAlgebra C H) G)
871 (ZCFreeFoxCoordinates C (X := X) (H := H))
872 (zcCompletedDifferentialPreModuleNaturalTopology
873 C psi.toMonoidHom)
874 inferInstance
875 (fun x =>
876 (closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
877 (G := G) (H := H) C psi family hfree htarget hφconv
878 hH hφHconv hφHgen hfundamental).toLinearMap
879 ((crossedDifferentialRelationSubmodule
880 (zcCompletedGroupAlgebraScalar
881 C psi.toMonoidHom)).mkQ x))) :
882 zcCompletedDifferentialModuleRelationSubmoduleClosed
883 C psi.toMonoidHom := by
884 let e :=
885 closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
886 (G := G) (H := H) C psi family hfree htarget hφconv
887 hH hφHconv hφHgen hfundamental
888 exact
889 zcDiffModuleRelSubmoduleClosed_of_inj_continuous_comp_mkQ
890 C psi.toMonoidHom e.toLinearMap e.injective hprecoord_continuous
892/--
893The closed-generated coordinate equivalence and continuity of the coordinate map \(A_{\psi}(C)
894\to \mathbb{Z}_C\llbracket H\rrbracket^{X}\) imply closedness for the quotient finite-stage
895natural topology.
896-/
897theorem zcDiffRelSubmoduleClosed_of_closedGenCoord_fundFormula
898 [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
900 (hφHconv :
902 (G := H) (fun i : X => psi (family i)))
903 (hφHgen :
905 (G := H) (Set.range (fun i : X => psi (family i))))
906 (hfundamental :
907 ∀ g : G,
908 presentedCompletedDifferentialFamilyMapProCInteger
909 (G := G) (H := H) C psi family
910 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
911 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
912 zcUniversalDifferential C psi.toMonoidHom g)
913 (hcoord_continuous :
914 @Continuous
915 (ZCCompletedDifferentialModule C psi.toMonoidHom)
916 (ZCFreeFoxCoordinates C (X := X) (H := H))
917 (zcCompletedDifferentialModuleNaturalTopology
918 C psi.toMonoidHom)
919 inferInstance
920 (closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
921 (G := G) (H := H) C psi family hfree htarget hφconv
922 hH hφHconv hφHgen hfundamental).toLinearMap) :
923 zcCompletedDifferentialModuleRelationSubmoduleClosed
924 C psi.toMonoidHom := by
925 let e :=
926 closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
927 (G := G) (H := H) C psi family hfree htarget hφconv
928 hH hφHconv hφHgen hfundamental
929 exact
930 zcDiffModuleRelSubmoduleClosed_of_inj_continuous_naturalTopology
931 C psi.toMonoidHom e.toLinearMap e.injective hcoord_continuous
933/--
934Closedness from the closed-generated fundamental formula and finite-stage coordinate
935factorization. The factorization hypothesis is the concrete finite-stage compatibility needed
936to make the closed-generated coordinate map continuous for the natural topology on the
937algebraic \(A_{\psi}(C)\).
938-/
939theorem zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_stage_factorization_of_fundFormula
940 [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
942 (hφHconv :
944 (G := H) (fun i : X => psi (family i)))
945 (hφHgen :
947 (G := H) (Set.range (fun i : X => psi (family i))))
948 (hfundamental :
949 ∀ g : G,
950 presentedCompletedDifferentialFamilyMapProCInteger
951 (G := G) (H := H) C psi family
952 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
953 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
954 zcUniversalDifferential C psi.toMonoidHom g) :
955 (∀ (x : X) (j : ZCCompletedGroupAlgebraIndex C H),
956 ∃ i : ZCCompletedDifferentialModuleIndex
957 C psi.toMonoidHom,
958 ∃ stageCoord :
959 ZCCompletedDifferentialModuleStage
960 C psi.toMonoidHom i →
961 ZCCompletedGroupAlgebraStage C H j,
962 ∀ a :
963 ZCCompletedDifferentialModule C psi.toMonoidHom,
964 zcCompletedGroupAlgebraProjection C H j
965 (closedGeneratedDerivativeCoordinatesLinearMapProCInteger
966 (G := G) (H := H) C psi family hfree htarget hφconv
967 hH hφHconv hφHgen a x) =
968 stageCoord
969 (zcCompletedDifferentialModuleStageProjection
970 C psi.toMonoidHom i a)) →
971 zcCompletedDifferentialModuleRelationSubmoduleClosed
972 C psi.toMonoidHom := by
973 intro hfactor
974 refine
975 zcDiffRelSubmoduleClosed_of_closedGenCoord_fundFormula
976 (G := G) (H := H) C psi family hfree htarget hφconv
977 hH hφHconv hφHgen hfundamental ?_
978 have hcoord :=
979 continuous_closedGenDerivCoordsZC_of_stageFactorization
980 (G := G) (H := H) C psi family hfree htarget hφconv
981 hH hφHconv hφHgen hfactor
982 have hmap :=
983 closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula_toLinearMap
984 (G := G) (H := H) C psi family hfree htarget hφconv
985 hH hφHconv hφHgen hfundamental
986 simpa [hmap] using hcoord
988/--
989Closedness from the completed fundamental formula once the source is a concrete pro-\(C\)
990group. The finite-stage factorization is supplied internally by the open-normal pro-\(C\) basis
991of the source, so the only remaining mathematical input is the non-circular module-valued
992fundamental formula.
993-/
994theorem zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_hasOpenNormalBasisInClass_of_fundFormula
995 [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
998 (hφHconv :
1000 (G := H) (fun i : X => psi (family i)))
1001 (hφHgen :
1003 (G := H) (Set.range (fun i : X => psi (family i))))
1004 (hfundamental :
1005 ∀ g : G,
1006 presentedCompletedDifferentialFamilyMapProCInteger
1007 (G := G) (H := H) C psi family
1008 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
1009 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
1010 zcUniversalDifferential C psi.toMonoidHom g) :
1011 zcCompletedDifferentialModuleRelationSubmoduleClosed
1012 C psi.toMonoidHom :=
1013 zcDiffModuleRelSubmoduleClosed_of_closedGenCoord_stage_factorization_of_fundFormula
1014 (G := G) (H := H) C psi family hfree htarget hφconv
1015 hH hφHconv hφHgen hfundamental
1016 (fun x j =>
1017 closedGenDerivativeCoordinatesLinearMapZC_stage_factorization_of_hasOpenNormalBasisInClass
1018 (G := G) (H := H) C psi family hfree htarget hφconv hGbasis
1019 hH hφHconv hφHgen x j)
1021/--
1022The closed-generated coordinate equivalence sends the universal differential of \(g\) to the
1023completed Fox-derivative coordinate vector of \(g\).
1025@[simp 900]
1026theorem closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula_universal
1028 (hφHconv :
1030 (G := H) (fun i : X => psi (family i)))
1031 (hφHgen :
1033 (G := H) (Set.range (fun i : X => psi (family i))))
1034 (hfundamental :
1035 ∀ g : G,
1036 presentedCompletedDifferentialFamilyMapProCInteger
1037 (G := G) (H := H) C psi family
1038 (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
1039 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g) =
1040 zcUniversalDifferential C psi.toMonoidHom g)
1041 (g : G) :
1042 closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
1043 (G := G) (H := H) C psi family hfree htarget hφconv
1044 hH hφHconv hφHgen hfundamental
1045 (zcUniversalDifferential C psi.toMonoidHom g) =
1046 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
1047 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g := by
1048 have hmap :=
1049 congrArg
1050 (fun L :
1051 ZCCompletedDifferentialModule C psi.toMonoidHom
1052 →ₗ[ZCCompletedGroupAlgebra C H]
1053 ZCFreeFoxCoordinates C (X := X) (H := H) =>
1054 L (zcUniversalDifferential C psi.toMonoidHom g))
1055 (closedGenDerivativeCoordinateLinearEquivZC_of_fundFormula_toLinearMap
1056 (G := G) (H := H) C psi family hfree htarget hφconv
1057 hH hφHconv hφHgen hfundamental)
1058 calc
1059 closedGeneratedDerivativeCoordinateLinearEquivProCInteger_of_fundamental_formula
1060 (G := G) (H := H) C psi family hfree htarget hφconv
1061 hH hφHconv hφHgen hfundamental
1062 (zcUniversalDifferential C psi.toMonoidHom g)
1064 closedGeneratedDerivativeCoordinatesLinearMapProCInteger
1065 (G := G) (H := H) C psi family hfree htarget hφconv
1066 hH hφHconv hφHgen
1067 (zcUniversalDifferential C psi.toMonoidHom g) := hmap
1068 _ =
1069 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
1070 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g := by
1071 exact closedGeneratedDerivativeCoordinatesLinearMapProCInteger_universal
1072 (G := G) (H := H) C psi family hfree htarget hφconv
1073 hH hφHconv hφHgen g
1075end ClosedGeneratedCoordinateEquiv
1077end
1079end CrowellExactSequence