Source: ProCGroups.FoxDifferential.Completed.Continuous.Universal.Basic
1import ProCGroups.FoxDifferential.Completed.Continuous.Free.DiscreteGenerators
2import ProCGroups.FoxDifferential.Completed.Continuous.Free.Rules
3import ProCGroups.FoxDifferential.Completed.Continuous.Topology
5/-!
6# Fox differential: completed — continuous — universal — basic
8The principal declarations in this module are:
10- `zcUniversalDifferentialFinalTopology`
11 The final topology on the completed universal differential module generated by the universal
12 crossed differential \(G \to d_{\mathbb{Z}_C\llbracket H\rrbracket}G\). Unlike the finite-rank
13 free-coordinate topology, this topology is available for an arbitrary source group and states the
14 genuine topological universal property: a map out is continuous exactly when its composite with
15 the universal differential is continuous.
16- `zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap`
17 The representing universal lift as a continuous linear map for the final universal topology, from
18 a continuous crossed differential.
19- `continuous_zcUniversalDifferential_universalTopology`
20 The universal crossed differential is continuous for the final universal topology.
21- `continuous_zcCompletedDifferentialModuleLift_universalTopology_iff`
22 The completed differential-module criterion is equivalent to the corresponding finite-stage
23 coordinate condition.
24-/
26namespace FoxDifferential
28noncomputable section
30open scoped BigOperators
32universe u v
34section UniversalTopology
36variable (C : ProCGroups.FiniteGroupClass.{v})
37variable {G : Type u} [Group G] [TopologicalSpace G]
38variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
40/--
41The final topology on the completed universal differential module generated by the universal
42crossed differential \(G \to d_{\mathbb{Z}_C\llbracket H\rrbracket}G\). Unlike the finite-rank
43free-coordinate topology, this topology is available for an arbitrary source group and states
44the genuine topological universal property: a map out is continuous exactly when its composite
45with the universal differential is continuous.
46-/
47@[reducible] def zcUniversalDifferentialFinalTopology (ψ : G →* H) :
48 TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
49 TopologicalSpace.coinduced (zcUniversalDifferential C ψ) inferInstance
51/-- The universal crossed differential is continuous for the final universal topology. -/
52theorem continuous_zcUniversalDifferential_universalTopology
53 (ψ : G →* H) :
54 @Continuous G (ZCCompletedDifferentialModule C ψ) inferInstance
55 (zcUniversalDifferentialFinalTopology C ψ)
56 (zcUniversalDifferential C ψ) :=
57 continuous_coinduced_rng
59variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
60variable [TopologicalSpace A]
62/--
63The completed differential-module criterion is equivalent to the corresponding finite-stage
64coordinate condition.
65-/
66theorem continuous_zcCompletedDifferentialModuleLift_universalTopology_iff
67 {ψ : G →* H}
68 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A) :
69 @Continuous (ZCCompletedDifferentialModule C ψ) A
70 (zcUniversalDifferentialFinalTopology C ψ) inferInstance
71 (crossedHomModuleLift (A := A)
72 (zcCompletedGroupAlgebraScalar C ψ) delta) ↔
73 Continuous delta := by
74 change @Continuous (ZCCompletedDifferentialModule C ψ) A
75 (TopologicalSpace.coinduced (zcUniversalDifferential C ψ) inferInstance) inferInstance
76 (crossedHomModuleLift (A := A)
77 (zcCompletedGroupAlgebraScalar C ψ) delta) ↔
78 Continuous delta
79 rw [continuous_coinduced_dom]
80 have hcomp :
81 (crossedHomModuleLift (A := A)
82 (zcCompletedGroupAlgebraScalar C ψ) delta) ∘
83 (zcUniversalDifferential C ψ) = delta := by
84 funext g
85 exact crossedHomModuleLift_universal
86 (A := A) (zcCompletedGroupAlgebraScalar C ψ) delta g
87 rw [hcomp]
89section ContinuousLinearMapPackaging
91variable (ψ : G →* H)
93/-- The completed differential module carries the universal finite-stage topology. -/
94instance zcCompletedDifferentialModuleUniversalTopologyInst :
95 TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
96 zcUniversalDifferentialFinalTopology C ψ
98/--
99The representing universal lift as a continuous linear map for the final universal topology,
100from a continuous crossed differential.
101-/
102def zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap
103 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
104 (hcont : Continuous delta) :
105 ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A where
106 toLinearMap :=
107 crossedHomModuleLift (A := A) (zcCompletedGroupAlgebraScalar C ψ) delta
108 cont :=
109 (continuous_zcCompletedDifferentialModuleLift_universalTopology_iff
110 (C := C) (G := G) (H := H) (A := A) (ψ := ψ) delta).2 hcont
112/-- Evaluation of the universal-topology continuous lift. -/
113@[simp]
114theorem zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap_apply
115 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
116 (hcont : Continuous delta)
117 (m : ZCCompletedDifferentialModule C ψ) :
118 zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap
119 (C := C) (G := G) (H := H) (A := A) ψ delta hcont m =
120 crossedHomModuleLift (A := A)
121 (zcCompletedGroupAlgebraScalar C ψ) delta m :=
122 rfl
124/--
125Topological universal representation theorem for completed crossed differentials. With the final
126universal topology on the completed differential module, continuous crossed differentials \(G
127\to A\) are equivalent to continuous \(\mathbb{Z}_C\llbracket H\rrbracket\)-linear maps out of
128the completed universal differential module.
129-/
130def zcCompletedContinuousCrossedDifferentialEquivContinuousLinearMap :
131 {delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A //
132 Continuous delta} ≃
133 (ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A) where
134 toFun delta :=
135 zcCompletedDifferentialModuleLiftUniversalContinuousLinearMap
136 (C := C) (G := G) (H := H) (A := A) ψ delta.1 delta.2
137 invFun f :=
138 ⟨{ toFun := fun g => f (zcUniversalDifferential C ψ g)
139 map_mul' := by
140 intro g h
141 change f (zcUniversalDifferential C ψ (g * h)) =
142 f (zcUniversalDifferential C ψ g) +
143 zcCompletedGroupAlgebraScalar C ψ g •
144 f (zcUniversalDifferential C ψ h)
145 rw [ScalarCrossedHom.map_mul (zcUniversalDifferential C ψ)]
146 simp only [zcCompletedGroupAlgebraScalar_apply, map_add, map_smul] },
147 f.cont.comp (continuous_zcUniversalDifferential_universalTopology C ψ)⟩
148 left_inv delta := by
149 apply Subtype.ext
150 apply CrossedHom.ext
151 intro g
152 exact crossedHomModuleLift_universal
153 (A := A) (zcCompletedGroupAlgebraScalar C ψ) delta.1 g
154 right_inv f := by
155 apply ContinuousLinearMap.ext
156 intro m
157 let delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A :=
158 { toFun := fun g => f (zcUniversalDifferential C ψ g)
159 map_mul' := by
160 intro g h
161 change f (zcUniversalDifferential C ψ (g * h)) =
162 f (zcUniversalDifferential C ψ g) +
163 zcCompletedGroupAlgebraScalar C ψ g •
164 f (zcUniversalDifferential C ψ h)
165 rw [ScalarCrossedHom.map_mul (zcUniversalDifferential C ψ)]
166 simp only [zcCompletedGroupAlgebraScalar_apply, map_add, map_smul] }
167 have hlin :
168 f.toLinearMap =
169 crossedHomModuleLift (A := A)
170 (zcCompletedGroupAlgebraScalar C ψ) delta := by
171 apply crossedHomModuleLift_unique
172 (A := A) (zcCompletedGroupAlgebraScalar C ψ) delta
173 intro g
174 rfl
175 exact congrFun (congrArg DFunLike.coe hlin.symm) m
177end ContinuousLinearMapPackaging
179/-- The universal boundary map from the completed differential module to `Z_C[[H]]` is continuous
180for the final universal topology whenever the target homomorphism is continuous. -/
181theorem continuous_zcToCompletedGroupAlgebra_universalTopology
182 (ψ : G →* H) (hψ : Continuous ψ) :
183 @Continuous (ZCCompletedDifferentialModule C ψ) (ZCCompletedGroupAlgebra C H)
184 (zcUniversalDifferentialFinalTopology C ψ) inferInstance
185 (zcToCompletedGroupAlgebra C ψ) := by
186 exact
187 (continuous_zcCompletedDifferentialModuleLift_universalTopology_iff
188 (C := C) (G := G) (H := H) (A := ZCCompletedGroupAlgebra C H)
189 (ψ := ψ) (zcCompletedGroupAlgebraBoundary C ψ)).2
190 (continuous_zcCompletedGroupAlgebraBoundary (C := C) (G := H) ψ hψ)
192end UniversalTopology
194section FreeGroupUniversalTopology
196variable (C : ProCGroups.FiniteGroupClass.{v})
197variable {X : Type u} [Fintype X] [DecidableEq X]
198variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
200/--
201The finite-rank topology on the completed universal module, induced by completed Fox
202coordinates. This is intentionally a named topology, not a global instance.
203-/
204@[reducible] def zcCompletedDifferentialModuleFreeTopology (ψ : FreeGroup X →* H) :
205 TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
206 TopologicalSpace.induced (zcDifferentialToFreeFoxCoordinates C ψ) inferInstance
208omit [Fintype X] in
209/--
210The coordinate map out of the completed universal module is continuous for the finite-rank
211coordinate-induced topology.
212-/
213theorem continuous_zcDifferentialToFreeFoxCoordinates_freeTopology
214 (ψ : FreeGroup X →* H) :
215 @Continuous (ZCCompletedDifferentialModule C ψ)
216 (ZCFreeFoxCoordinates C (X := X) (H := H))
217 (zcCompletedDifferentialModuleFreeTopology C ψ) inferInstance
218 (zcDifferentialToFreeFoxCoordinates C ψ) :=
219 continuous_induced_dom
221/--
222The coordinate-to-universal-module map is continuous for the finite-rank coordinate-induced
223topology.
224-/
225theorem continuous_zcFreeFoxCoordinatesLinearMap_freeTopology
226 (ψ : FreeGroup X →* H) :
227 @Continuous (ZCFreeFoxCoordinates C (X := X) (H := H))
228 (ZCCompletedDifferentialModule C ψ) inferInstance
229 (zcCompletedDifferentialModuleFreeTopology C ψ)
230 (zcFreeFoxCoordinatesLinearMap C ψ) := by
231 change @Continuous (ZCFreeFoxCoordinates C (X := X) (H := H))
232 (ZCCompletedDifferentialModule C ψ) inferInstance
233 (TopologicalSpace.induced (zcDifferentialToFreeFoxCoordinates C ψ) inferInstance)
234 (zcFreeFoxCoordinatesLinearMap C ψ)
235 rw [continuous_induced_rng]
236 have hcomp :
237 (zcDifferentialToFreeFoxCoordinates C ψ) ∘
238 (zcFreeFoxCoordinatesLinearMap C ψ) =
239 id := by
240 funext v
241 exact congrFun
242 (congrArg DFunLike.coe
243 (zcDifferentialToFreeFoxCoordinates_comp_zcFreeFoxCoordinatesLinearMap C ψ)) v
244 simpa only [hcomp] using continuous_id
246/-- The coordinate module `Z_C[[H]]^X` has continuous scalar multiplication. -/
247instance instContinuousSMulZCFreeFoxCoordinates :
248 ContinuousSMul (ZCCompletedGroupAlgebra C H)
249 (ZCFreeFoxCoordinates C (X := X) (H := H)) :=
250 inferInstance
252/-- The finite-rank completed universal module has continuous scalar multiplication for the
253coordinate-induced topology. -/
254instance instContinuousSMulZCCompletedDifferentialModuleFreeTopology
255 (ψ : FreeGroup X →* H) :
256 @ContinuousSMul (ZCCompletedGroupAlgebra C H)
257 (ZCCompletedDifferentialModule C ψ)
258 inferInstance inferInstance (zcCompletedDifferentialModuleFreeTopology C ψ) :=
259 ContinuousSMul.induced (zcDifferentialToFreeFoxCoordinates C ψ)
261variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
263/--
264The finite coordinate linear map attached to the generator values of a completed crossed
265differential.
266-/
267def zcFreeCrossedDifferentialCoordinateLift
268 {ψ : FreeGroup X →* H}
269 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A) :
270 ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H] A where
271 toFun v := ∑ x : X, v x • delta (FreeGroup.of x)
272 map_add' v w := by
273 simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
274 map_smul' r v := by
275 simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, Finset.smul_sum, smul_smul]
277omit [DecidableEq X] in
278/-- Evaluation formula for the coordinate lift attached to generator values. -/
279theorem zcFreeCrossedDifferentialCoordinateLift_apply
280 {ψ : FreeGroup X →* H}
281 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
282 (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
283 zcFreeCrossedDifferentialCoordinateLift (H := H) C delta v =
284 ∑ x : X, v x • delta (FreeGroup.of x) :=
285 rfl
287/--
288The coordinate lift applied to the completed free derivative vector recovers the crossed
289differential it represents.
290-/
291theorem zcFreeCrossedDifferentialCoordinateLift_derivativeVector
292 (ψ : FreeGroup X →* H)
293 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
294 (w : FreeGroup X) :
295 zcFreeCrossedDifferentialCoordinateLift (H := H) C delta
296 (zcFreeGroupFoxDerivativeVector C ψ w) =
297 delta w := by
298 let L := zcFreeCrossedDifferentialCoordinateLift (H := H) C delta
299 let beta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A :=
300 (zcFreeGroupFoxDerivativeVector C ψ).mapLinear L
301 have hbasis : ∀ x : X, beta (FreeGroup.of x) = delta (FreeGroup.of x) := by
302 intro x
303 change L (zcFreeGroupFoxDerivativeVector C ψ (FreeGroup.of x)) =
304 delta (FreeGroup.of x)
305 rw [zcFreeGroupFoxDerivativeVector_of]
306 change (∑ y : X,
307 ((Pi.single x (1 : ZCCompletedGroupAlgebra C H) :
308 ZCFreeFoxCoordinates C (X := X) (H := H)) y) •
309 delta (FreeGroup.of y)) =
310 delta (FreeGroup.of x)
311 rw [Finset.sum_eq_single x]
312 · simp only [Pi.single_eq_same, one_smul]
313 · intro y _ hy
314 simp only [Pi.single_eq_of_ne hy, zero_smul]
315 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_smul,
316 IsEmpty.forall_iff]
317 have hbeta_eq :=
318 freeCrossedHomWithCoeff_unique
319 (A := A) (zcCompletedGroupAlgebraScalar C ψ)
320 (fun x : X => delta (FreeGroup.of x)) beta hbasis
321 have hdelta_eq :=
322 freeCrossedHomWithCoeff_unique
323 (A := A) (zcCompletedGroupAlgebraScalar C ψ)
324 (fun x : X => delta (FreeGroup.of x)) delta (by intro x; rfl)
325 simpa [beta, L] using
326 congrArg (fun d : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A => d w)
327 (hbeta_eq.trans hdelta_eq.symm)
329omit [DecidableEq X] in
330/-- The coordinate lift is the representing universal-module lift composed with the
331coordinate-to-module map. -/
332theorem zcFreeCrossedDifferentialCoordinateLift_eq_completedLift_comp_coordinates
333 (ψ : FreeGroup X →* H)
334 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A) :
335 zcFreeCrossedDifferentialCoordinateLift (H := H) C delta =
336 (crossedHomModuleLift (A := A)
337 (zcCompletedGroupAlgebraScalar C ψ) delta).comp
338 (zcFreeFoxCoordinatesLinearMap C ψ) := by
339 ext v
340 change (∑ x : X, v x • delta (FreeGroup.of x)) =
341 crossedHomModuleLift (A := A)
342 (zcCompletedGroupAlgebraScalar C ψ) delta
343 (∑ x : X, v x • zcUniversalDifferential C ψ (FreeGroup.of x))
344 have hlift : ∀ x : X,
345 crossedHomModuleLift (A := A)
346 (zcCompletedGroupAlgebraScalar C ψ) delta
347 (zcUniversalDifferential C ψ (FreeGroup.of x)) =
348 delta (FreeGroup.of x) := by
349 intro x
350 exact crossedHomModuleLift_universal
351 (A := A) (zcCompletedGroupAlgebraScalar C ψ) delta (FreeGroup.of x)
352 rw [map_sum]
353 simp only [map_smul, hlift]
355/-- The representing universal-module lift factors through completed Fox coordinates. -/
356theorem zcCompletedDifferentialModuleLift_eq_coordinateLift_comp
357 (ψ : FreeGroup X →* H)
358 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A) :
359 crossedHomModuleLift (A := A)
360 (zcCompletedGroupAlgebraScalar C ψ) delta =
361 (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta).comp
362 (zcDifferentialToFreeFoxCoordinates C ψ) := by
363 apply crossedDifferentialModuleHom_ext
364 (A := A) (zcCompletedGroupAlgebraScalar C ψ)
365 intro w
366 change
367 crossedHomModuleLift (A := A)
368 (zcCompletedGroupAlgebraScalar C ψ) delta
369 (zcUniversalDifferential C ψ w) =
370 zcFreeCrossedDifferentialCoordinateLift (H := H) C delta
371 (zcDifferentialToFreeFoxCoordinates C ψ
372 (zcUniversalDifferential C ψ w))
373 have hlift :
374 crossedHomModuleLift (A := A)
375 (zcCompletedGroupAlgebraScalar C ψ) delta
376 (zcUniversalDifferential C ψ w) =
377 delta w :=
378 crossedHomModuleLift_universal
379 (A := A) (zcCompletedGroupAlgebraScalar C ψ) delta w
380 rw [hlift, zcDifferentialToFreeFoxCoordinates_universal,
381 zcFreeCrossedDifferentialCoordinateLift_derivativeVector]
383variable [TopologicalSpace A]
385variable {C} in
386/-- Continuous representation theorem for finite-rank completed universal modules.
388With the coordinate-induced topology on `ZCCompletedDifferentialModule`, the universal linear map
389representing a completed crossed differential is continuous exactly when the finite coordinate
390linear map determined by its generator values is continuous. -/
391theorem continuous_zcCompletedDifferentialModuleLift_freeTopology_iff
392 {ψ : FreeGroup X →* H}
393 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A) :
394 @Continuous (ZCCompletedDifferentialModule C ψ) A
395 (zcCompletedDifferentialModuleFreeTopology C ψ) inferInstance
396 (crossedHomModuleLift (A := A)
397 (zcCompletedGroupAlgebraScalar C ψ) delta) ↔
398 Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta) := by
399 constructor
400 · intro h
401 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
402 zcCompletedDifferentialModuleFreeTopology C ψ
403 have h' : Continuous (crossedHomModuleLift (A := A)
404 (zcCompletedGroupAlgebraScalar C ψ) delta) := h
405 have hcoord :=
406 continuous_zcFreeFoxCoordinatesLinearMap_freeTopology (X := X) (H := H) C ψ
407 have heq :=
408 zcFreeCrossedDifferentialCoordinateLift_eq_completedLift_comp_coordinates
409 (A := A) C ψ delta
410 simpa [heq, LinearMap.comp_apply] using h'.comp hcoord
411 · intro h
412 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
413 zcCompletedDifferentialModuleFreeTopology C ψ
414 have hcoord :=
415 continuous_zcDifferentialToFreeFoxCoordinates_freeTopology (X := X) (H := H) C ψ
416 have heq :=
417 zcCompletedDifferentialModuleLift_eq_coordinateLift_comp
418 (A := A) C ψ delta
419 simpa [heq, LinearMap.comp_apply] using h.comp hcoord
421section ContinuousLinearMapPackaging
423variable (ψ : FreeGroup X →* H)
425/--
426The free completed differential pre-module carries the finite-stage topology used before
427quotienting by crossed-differential relations.
428-/
429@[reducible] def zcCompletedDifferentialModuleFreeTopologyInst :
430 TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
431 zcCompletedDifferentialModuleFreeTopology C ψ
433attribute [local instance] zcCompletedDifferentialModuleFreeTopologyInst
435/-- The completed coordinate map as a continuous linear map for the coordinate-induced topology. -/
436def zcDifferentialToFreeFoxCoordinatesContinuousLinearMap :
437 ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H]
438 ZCFreeFoxCoordinates C (X := X) (H := H) where
439 toLinearMap := zcDifferentialToFreeFoxCoordinates C ψ
440 cont := continuous_zcDifferentialToFreeFoxCoordinates_freeTopology (X := X) (H := H) C ψ
442omit [Fintype X] in
443/-- Evaluation of the continuous completed coordinate map. -/
444@[simp]
445theorem zcDifferentialToFreeFoxCoordinatesContinuousLinearMap_apply
446 (m : ZCCompletedDifferentialModule C ψ) :
447 zcDifferentialToFreeFoxCoordinatesContinuousLinearMap (X := X) (H := H) C ψ m =
448 zcDifferentialToFreeFoxCoordinates C ψ m :=
449 rfl
451/--
452The coordinate-to-universal map as a continuous linear map for the coordinate-induced topology.
453-/
454def zcFreeFoxCoordinatesContinuousLinearMap :
455 ZCFreeFoxCoordinates C (X := X) (H := H) →L[ZCCompletedGroupAlgebra C H]
456 ZCCompletedDifferentialModule C ψ where
457 toLinearMap := zcFreeFoxCoordinatesLinearMap C ψ
458 cont := continuous_zcFreeFoxCoordinatesLinearMap_freeTopology (X := X) (H := H) C ψ
460/-- Evaluation of the continuous coordinate-to-universal map. -/
461@[simp]
462theorem zcFreeFoxCoordinatesContinuousLinearMap_apply
463 (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
464 zcFreeFoxCoordinatesContinuousLinearMap (X := X) (H := H) C ψ v =
465 zcFreeFoxCoordinatesLinearMap C ψ v :=
466 rfl
468/-- A finite coordinate lift bundled as a continuous linear map, once its continuity is known. -/
469def zcFreeCrossedDifferentialCoordinateContinuousLinearMap
470 {ψ : FreeGroup X →* H}
471 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
472 (hcont : Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta)) :
473 ZCFreeFoxCoordinates C (X := X) (H := H) →L[ZCCompletedGroupAlgebra C H] A where
474 toLinearMap := zcFreeCrossedDifferentialCoordinateLift (H := H) C delta
475 cont := hcont
477omit [DecidableEq X] in
478/-- Evaluation of the continuous coordinate lift attached to generator values. -/
479@[simp]
480theorem zcFreeCrossedDifferentialCoordinateContinuousLinearMap_apply
481 {ψ : FreeGroup X →* H}
482 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
483 (hcont : Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta))
484 (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
485 zcFreeCrossedDifferentialCoordinateContinuousLinearMap
486 (X := X) (H := H) (A := A) C delta hcont v =
487 ∑ x : X, v x • delta (FreeGroup.of x) :=
488 rfl
490/-- The representing universal lift bundled as a continuous linear map, once its continuity for
491the coordinate-induced topology is known. -/
492def zcCompletedDifferentialModuleLiftContinuousLinearMap
493 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
494 (hcont : Continuous (crossedHomModuleLift (A := A)
495 (zcCompletedGroupAlgebraScalar C ψ) delta)) :
496 ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A where
497 toLinearMap :=
498 crossedHomModuleLift (A := A) (zcCompletedGroupAlgebraScalar C ψ) delta
499 cont := hcont
501omit [Fintype X] in
502/-- Evaluation of the continuous representing universal lift. -/
503@[simp]
504theorem zcCompletedDifferentialModuleLiftContinuousLinearMap_apply
505 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
506 (hcont : Continuous (crossedHomModuleLift (A := A)
507 (zcCompletedGroupAlgebraScalar C ψ) delta))
508 (m : ZCCompletedDifferentialModule C ψ) :
509 zcCompletedDifferentialModuleLiftContinuousLinearMap
510 (X := X) (H := H) (A := A) C ψ delta hcont m =
511 crossedHomModuleLift (A := A)
512 (zcCompletedGroupAlgebraScalar C ψ) delta m :=
513 rfl
515/-- Continuous representation theorem packaged as a continuous linear map under continuity of the
516finite coordinate lift. -/
517def zcCompletedDifferentialModuleLiftContinuousLinearMapOfCoordinate
518 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
519 (hcoord : Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta)) :
520 ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A :=
521 zcCompletedDifferentialModuleLiftContinuousLinearMap
522 (X := X) (H := H) (A := A) C ψ delta
523 ((continuous_zcCompletedDifferentialModuleLift_freeTopology_iff
524 (X := X) (H := H) (A := A) (ψ := ψ) delta).2 hcoord)
526/--
527Evaluation of the continuous universal lift obtained from a continuous finite coordinate lift.
528-/
529@[simp]
530theorem zcCompletedDifferentialModuleLiftContinuousLinearMapOfCoordinate_apply
531 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)
532 (hcoord : Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta))
533 (m : ZCCompletedDifferentialModule C ψ) :
534 zcCompletedDifferentialModuleLiftContinuousLinearMapOfCoordinate
535 (X := X) (H := H) (A := A) C ψ delta hcoord m =
536 crossedHomModuleLift (A := A)
537 (zcCompletedGroupAlgebraScalar C ψ) delta m :=
538 rfl
540end ContinuousLinearMapPackaging
542end FreeGroupUniversalTopology
544end
546end FoxDifferential