FoxDifferential/Completed/Continuous/Universal/Basic.lean
1import FoxDifferential.Completed.Continuous.Free.DiscreteGenerators
2import FoxDifferential.Completed.Continuous.Free.Rules
3import FoxDifferential.Completed.Continuous.Topology
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FoxDifferential/Completed/Continuous/Universal/Basic.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Continuous crossed differentials
16Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
17-/
18namespace FoxDifferential
20noncomputable section
22open scoped BigOperators
24universe u v
26section UniversalTopology
28variable (C : ProCGroups.FiniteGroupClass.{v})
29variable {G : Type u} [Group G] [TopologicalSpace G]
30variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
32/-- The final topology on the completed universal differential module generated by the universal
33crossed differential `G -> d_{Z_C[[H]]} G`.
35Unlike the finite-rank free-coordinate topology, this topology is available for an arbitrary source
37its composite with the universal differential is continuous. -/
38def zcCompletedDifferentialModuleUniversalTopology (ψ : G →* H) :
39 TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
40 TopologicalSpace.coinduced (zcUniversalDifferential C ψ) inferInstance
42/-- The universal crossed differential is continuous for the final universal topology. -/
44 (ψ : G →* H) :
45 @Continuous G (ZCCompletedDifferentialModule C ψ) inferInstance
47 (zcUniversalDifferential C ψ) :=
48 continuous_coinduced_rng
50variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
51variable [TopologicalSpace A]
53/-- Topological universal property of the completed differential module with its final topology.
55For an arbitrary source group, the universal linear map representing a crossed differential is
56continuous exactly when the crossed differential itself is continuous. -/
58 {ψ : G →* H} {delta : G → A}
59 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta) :
60 @Continuous (ZCCompletedDifferentialModule C ψ) A
61 (zcCompletedDifferentialModuleUniversalTopology C ψ) inferInstance
62 (zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta) ↔
63 Continuous delta := by
64 rw [continuous_coinduced_dom]
65 have hcomp :
66 (zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta) ∘
67 (zcUniversalDifferential C ψ) = delta := by
68 funext g
70 (A := A) C ψ delta hdelta g
71 rw [hcomp]
73section ContinuousLinearMapPackaging
75variable (ψ : G →* H)
78 TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
81/-- The representing universal lift as a continuous linear map for the final universal topology,
82from a continuous crossed differential. -/
84 (delta : G → A)
85 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
86 (hcont : Continuous delta) :
87 ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A where
88 toLinearMap := zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta
89 cont :=
91 (C := C) (G := G) (H := H) (A := A) (ψ := ψ) (delta := delta) hdelta).2 hcont
93/-- Evaluation of the universal-topology continuous lift. -/
94@[simp]
96 (delta : G → A)
97 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
98 (hcont : Continuous delta)
99 (m : ZCCompletedDifferentialModule C ψ) :
101 (C := C) (G := G) (H := H) (A := A) ψ delta hdelta hcont m =
102 zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta m :=
103 rfl
105/-- Topological universal representation theorem for completed crossed differentials.
107With the final universal topology on the completed differential module, continuous crossed
108differentials `G -> A` are equivalent to continuous `Z_C[[H]]`-linear maps out of the completed
109universal differential module. -/
111 {delta : G → A //
112 IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta ∧ Continuous delta} ≃
113 (ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A) where
114 toFun delta :=
116 (C := C) (G := G) (H := H) (A := A) ψ delta.1 delta.2.1 delta.2.2
117 invFun f :=
118 ⟨fun g => f (zcUniversalDifferential C ψ g), by
119 constructor
120 · intro g h
121 change f (zcUniversalDifferential C ψ (g * h)) =
122 f (zcUniversalDifferential C ψ g) +
123 zcCompletedGroupAlgebraScalar C ψ g •
124 f (zcUniversalDifferential C ψ h)
126 simp only [zcCompletedGroupAlgebraScalar_apply, map_add, map_smul]
127 · exact f.cont.comp (continuous_zcUniversalDifferential_universalTopology C ψ)⟩
128 left_inv delta := by
129 apply Subtype.ext
130 funext g
132 (A := A) C ψ delta.1 delta.2.1 g
133 right_inv f := by
134 apply ContinuousLinearMap.ext
135 intro m
136 have hdelta :
138 (fun g => f (zcUniversalDifferential C ψ g)) := by
139 intro g h
140 change f (zcUniversalDifferential C ψ (g * h)) =
141 f (zcUniversalDifferential C ψ g) +
142 zcCompletedGroupAlgebraScalar C ψ g •
143 f (zcUniversalDifferential C ψ h)
145 simp only [zcCompletedGroupAlgebraScalar_apply, map_add, map_smul]
146 have hlin :
147 f.toLinearMap =
148 zcCompletedDifferentialModuleLift (A := A) C ψ
149 (fun g => f (zcUniversalDifferential C ψ g)) hdelta := by
150 apply zcCompletedDifferentialModuleLift_unique (A := A) C ψ
151 intro g
152 rfl
153 exact congrFun (congrArg DFunLike.coe hlin.symm) m
155end ContinuousLinearMapPackaging
157/-- The universal boundary map from the completed differential module to `Z_C[[H]]` is continuous
158for the final universal topology whenever the target homomorphism is continuous. -/
160 (ψ : G →* H) (hψ : Continuous ψ) :
161 @Continuous (ZCCompletedDifferentialModule C ψ) (ZCCompletedGroupAlgebra C H)
162 (zcCompletedDifferentialModuleUniversalTopology C ψ) inferInstance
163 (zcToCompletedGroupAlgebra C ψ) := by
164 exact
166 (C := C) (G := G) (H := H) (A := ZCCompletedGroupAlgebra C H)
167 (ψ := ψ) (delta := zcCompletedGroupAlgebraBoundary C ψ)
169 (continuous_zcCompletedGroupAlgebraBoundary (C := C) (G := H) ψ hψ)
171end UniversalTopology
173section FreeGroupUniversalTopology
175variable (C : ProCGroups.FiniteGroupClass.{v})
176variable [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)]
177variable {X : Type u} [Fintype X] [DecidableEq X]
178variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
180/-- The finite-rank topology on the completed universal module, induced by completed Fox
181coordinates. This is intentionally a named topology, not a global instance. -/
182def zcCompletedDifferentialModuleFreeTopology (ψ : FreeGroup X →* H) :
183 TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
184 TopologicalSpace.induced (zcDifferentialToFreeFoxCoordinates C ψ) inferInstance
186omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [Fintype X] in
187/-- The coordinate map out of the completed universal module is continuous for the finite-rank
188coordinate-induced topology. -/
190 (ψ : FreeGroup X →* H) :
191 @Continuous (ZCCompletedDifferentialModule C ψ)
192 (ZCFreeFoxCoordinates C (X := X) (H := H))
193 (zcCompletedDifferentialModuleFreeTopology C ψ) inferInstance
194 (zcDifferentialToFreeFoxCoordinates C ψ) :=
195 continuous_induced_dom
197omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
198/-- The coordinate-to-universal-module map is continuous for the finite-rank coordinate-induced
199topology. -/
201 (ψ : FreeGroup X →* H) :
202 @Continuous (ZCFreeFoxCoordinates C (X := X) (H := H))
203 (ZCCompletedDifferentialModule C ψ) inferInstance
205 (zcFreeFoxCoordinatesLinearMap C ψ) := by
206 rw [continuous_induced_rng]
207 have hcomp :
209 (zcFreeFoxCoordinatesLinearMap C ψ) =
210 id := by
211 funext v
212 exact congrFun
213 (congrArg DFunLike.coe
215 rw [hcomp]
216 exact continuous_id
218/-- The coordinate module `Z_C[[H]]^X` has continuous scalar multiplication. -/
219instance instContinuousSMulZCFreeFoxCoordinates :
220 ContinuousSMul (ZCCompletedGroupAlgebra C H)
221 (ZCFreeFoxCoordinates C (X := X) (H := H)) :=
222 inferInstance
224/-- The finite-rank completed universal module has continuous scalar multiplication for the
225coordinate-induced topology. -/
227 (ψ : FreeGroup X →* H) :
228 @ContinuousSMul (ZCCompletedGroupAlgebra C H)
230 inferInstance inferInstance (zcCompletedDifferentialModuleFreeTopology C ψ) :=
231 ContinuousSMul.induced (zcDifferentialToFreeFoxCoordinates C ψ)
233variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
235/-- The finite coordinate linear map attached to the generator values of a completed crossed
236differential. -/
238 (delta : FreeGroup X → A) :
239 ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H] A where
240 toFun v := ∑ x : X, v x • delta (FreeGroup.of x)
241 map_add' v w := by
242 simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
243 map_smul' r v := by
244 simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, Finset.smul_sum, smul_smul]
246omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [DecidableEq X] in
247/-- Evaluation formula for the coordinate lift attached to generator values. -/
249 (delta : FreeGroup X → A)
250 (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
251 zcFreeCrossedDifferentialCoordinateLift (H := H) C delta v =
252 ∑ x : X, v x • delta (FreeGroup.of x) :=
253 rfl
255omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
256/-- The coordinate lift applied to the completed free derivative vector recovers the crossed
257differential it represents. -/
259 (ψ : FreeGroup X →* H) (delta : FreeGroup X → A)
260 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
261 (w : FreeGroup X) :
262 zcFreeCrossedDifferentialCoordinateLift (H := H) C delta
263 (zcFreeGroupFoxDerivativeVector C ψ w) =
264 delta w := by
265 let L := zcFreeCrossedDifferentialCoordinateLift (H := H) C delta
266 let beta : FreeGroup X → A := fun w => L (zcFreeGroupFoxDerivativeVector C ψ w)
267 have hbeta :
268 IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) beta :=
269 IsCrossedDifferential.map_linear (zcFreeGroupFoxDerivativeVector_isCrossedDifferential C ψ) L
270 have hbasis : ∀ x : X, beta (FreeGroup.of x) = delta (FreeGroup.of x) := by
271 intro x
272 simp only [zcFreeCrossedDifferentialCoordinateLift, LinearMap.coe_mk, AddHom.coe_mk,
273 zcFreeGroupFoxDerivativeVector_of, Fintype.sum_single_smul, one_smul, beta, L]
274 have hbeta_eq :
275 beta =
277 (A := A) (zcCompletedGroupAlgebraScalar C ψ)
278 (fun x : X => delta (FreeGroup.of x)) := by
280 (A := A) (zcCompletedGroupAlgebraScalar C ψ)
281 (fun x : X => delta (FreeGroup.of x)) beta hbeta hbasis
282 have hdelta_eq :
283 delta =
285 (A := A) (zcCompletedGroupAlgebraScalar C ψ)
286 (fun x : X => delta (FreeGroup.of x)) := by
288 (A := A) (zcCompletedGroupAlgebraScalar C ψ)
289 (fun x : X => delta (FreeGroup.of x)) delta hdelta (by intro x; rfl)
290 simpa [beta, L] using congrFun (hbeta_eq.trans hdelta_eq.symm) w
292omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [DecidableEq X] in
293/-- The coordinate lift is the representing universal-module lift composed with the
294coordinate-to-module map. -/
296 (ψ : FreeGroup X →* H) (delta : FreeGroup X → A)
297 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta) :
298 zcFreeCrossedDifferentialCoordinateLift (H := H) C delta =
299 (zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta).comp
300 (zcFreeFoxCoordinatesLinearMap C ψ) := by
301 ext v
302 simp only [zcFreeCrossedDifferentialCoordinateLift, LinearMap.coe_mk, AddHom.coe_mk,
303 zcFreeFoxCoordinatesLinearMap, LinearMap.coe_comp, Function.comp_apply, map_sum, map_smul,
306omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
307/-- The representing universal-module lift factors through completed Fox coordinates. -/
309 (ψ : FreeGroup X →* H) (delta : FreeGroup X → A)
310 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta) :
311 zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta =
312 (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta).comp
313 (zcDifferentialToFreeFoxCoordinates C ψ) := by
314 apply zcCompletedDifferentialModuleHom_ext C ψ
315 intro w
316 simp only [zcCompletedDifferentialModuleLift_universal, LinearMap.comp_apply,
318 zcFreeCrossedDifferentialCoordinateLift_derivativeVector C ψ delta hdelta w]
320variable [TopologicalSpace A]
322omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
323variable {C} in
324/-- Continuous representation theorem for finite-rank completed universal modules.
326With the coordinate-induced topology on `ZCCompletedDifferentialModule`, the universal linear map
330 {ψ : FreeGroup X →* H} {delta : FreeGroup X → A}
331 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta) :
332 @Continuous (ZCCompletedDifferentialModule C ψ) A
333 (zcCompletedDifferentialModuleFreeTopology C ψ) inferInstance
334 (zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta) ↔
335 Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta) := by
336 constructor
337 · intro h
338 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
340 have h' : Continuous (zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta) := h
341 have hcoord :=
342 continuous_zcFreeFoxCoordinatesLinearMap_freeTopology (X := X) (H := H) C ψ
343 have heq :=
345 (A := A) C ψ delta hdelta
346 simpa [heq, LinearMap.comp_apply] using h'.comp hcoord
347 · intro h
348 letI : TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
350 have hcoord :=
351 continuous_zcDifferentialToFreeFoxCoordinates_freeTopology (X := X) (H := H) C ψ
352 have heq :=
354 (A := A) C ψ delta hdelta
355 simpa [heq, LinearMap.comp_apply] using h.comp hcoord
357section ContinuousLinearMapPackaging
359variable (ψ : FreeGroup X →* H)
362 TopologicalSpace (ZCCompletedDifferentialModule C ψ) :=
365/-- The completed coordinate map as a continuous linear map for the coordinate-induced topology. -/
367 ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H]
368 ZCFreeFoxCoordinates C (X := X) (H := H) where
369 toLinearMap := zcDifferentialToFreeFoxCoordinates C ψ
370 cont := continuous_zcDifferentialToFreeFoxCoordinates_freeTopology (X := X) (H := H) C ψ
372omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [Fintype X] in
373/-- Evaluation of the continuous completed coordinate map. -/
374@[simp]
376 (m : ZCCompletedDifferentialModule C ψ) :
377 zcDifferentialToFreeFoxCoordinatesContinuousLinearMap (X := X) (H := H) C ψ m =
378 zcDifferentialToFreeFoxCoordinates C ψ m :=
379 rfl
381/-- The coordinate-to-universal map as a continuous linear map for the coordinate-induced
382topology. -/
384 ZCFreeFoxCoordinates C (X := X) (H := H) →L[ZCCompletedGroupAlgebra C H]
385 ZCCompletedDifferentialModule C ψ where
386 toLinearMap := zcFreeFoxCoordinatesLinearMap C ψ
387 cont := continuous_zcFreeFoxCoordinatesLinearMap_freeTopology (X := X) (H := H) C ψ
389omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
390/-- Evaluation of the continuous coordinate-to-universal map. -/
391@[simp]
393 (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
394 zcFreeFoxCoordinatesContinuousLinearMap (X := X) (H := H) C ψ v =
395 zcFreeFoxCoordinatesLinearMap C ψ v :=
396 rfl
398/-- A finite coordinate lift bundled as a continuous linear map, once its continuity is known. -/
400 (delta : FreeGroup X → A)
401 (hcont : Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta)) :
402 ZCFreeFoxCoordinates C (X := X) (H := H) →L[ZCCompletedGroupAlgebra C H] A where
403 toLinearMap := zcFreeCrossedDifferentialCoordinateLift (H := H) C delta
404 cont := hcont
406omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [DecidableEq X] in
407/-- Evaluation of the continuous coordinate lift attached to generator values. -/
408@[simp]
410 (delta : FreeGroup X → A)
411 (hcont : Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta))
412 (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
414 (X := X) (H := H) (A := A) C delta hcont v =
415 ∑ x : X, v x • delta (FreeGroup.of x) :=
416 rfl
418/-- The representing universal lift bundled as a continuous linear map, once its continuity for
419the coordinate-induced topology is known. -/
421 (delta : FreeGroup X → A)
422 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
423 (hcont : Continuous (zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta)) :
424 ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A where
425 toLinearMap := zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta
426 cont := hcont
428omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] [Fintype X] in
429/-- Evaluation of the continuous representing universal lift. -/
430@[simp]
432 (delta : FreeGroup X → A)
433 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
434 (hcont : Continuous (zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta))
435 (m : ZCCompletedDifferentialModule C ψ) :
437 (X := X) (H := H) (A := A) C ψ delta hdelta hcont m =
438 zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta m :=
439 rfl
441/-- Continuous representation theorem packaged as a continuous linear map: it is enough to prove
444 (delta : FreeGroup X → A)
445 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
446 (hcoord : Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta)) :
447 ZCCompletedDifferentialModule C ψ →L[ZCCompletedGroupAlgebra C H] A :=
449 (X := X) (H := H) (A := A) C ψ delta hdelta
451 (X := X) (H := H) (A := A) (ψ := ψ) (delta := delta) hdelta).2 hcoord)
453omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)] in
454/-- Evaluation of the continuous universal lift obtained from a continuous finite coordinate
455lift. -/
456@[simp]
458 (delta : FreeGroup X → A)
459 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
460 (hcoord : Continuous (zcFreeCrossedDifferentialCoordinateLift (H := H) C delta))
461 (m : ZCCompletedDifferentialModule C ψ) :
463 (X := X) (H := H) (A := A) C ψ delta hdelta hcoord m =
464 zcCompletedDifferentialModuleLift (A := A) C ψ delta hdelta m :=
465 rfl
467end ContinuousLinearMapPackaging
469end FreeGroupUniversalTopology
471end
473end FoxDifferential