FoxDifferential/Completed/Continuous/ChainRule/Iterated.lean
1import FoxDifferential.Completed.Continuous.ChainRule.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/Continuous/ChainRule/Iterated.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Continuous crossed differentials
14Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
15-/
16namespace FoxDifferential
18noncomputable section
20open scoped BigOperators
22universe u
24section AllFiniteIteratedChainRule
26variable {X Y Z F F' F'' H : Type u}
27variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
28variable [Fintype Y] [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
29variable [DecidableEq Z] [TopologicalSpace Z] [DiscreteTopology Z]
30variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
31variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
32variable [Group F''] [TopologicalSpace F''] [IsTopologicalGroup F'']
33variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
34variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
36/-- The pulled-back target generator on the middle free source in a two-step source chain. -/
38 {mu : Z → F''}
40 (ProC := ProCGroups.ProC.allFiniteProC) mu)
41 (θ : F' →* F'') (φ : Z → H) (κ : Y → F') : Y → H :=
43 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ
45/-- The pulled-back target generator on the first free source in a two-step source chain. -/
47 {κ : Y → F'} {mu : Z → F''}
49 (ProC := ProCGroups.ProC.allFiniteProC) κ)
51 (ProC := ProCGroups.ProC.allFiniteProC) mu)
52 (η : F →* F') (θ : F' →* F'') (φ : Z → H) (ι : X → F) : X → H :=
54 (X := X) (Y := Y) (F := F) (F' := F') hκ η
56 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
57 ι
59omit [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
60 [TopologicalSpace F] [IsTopologicalGroup F] in
61/-- Completed Fox-Jacobian functoriality for two composable continuous free pro-`C` source maps,
64 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
66 (ProC := ProCGroups.ProC.allFiniteProC) κ)
68 (ProC := ProCGroups.ProC.allFiniteProC) mu)
69 (η : F →* F') (θ : F' →* F'') (hθ_continuous : Continuous θ) (φ : Z → H) :
71 (X := X) (Y := Z) (F := F) (F' := F'') hmu (θ.comp η) φ ι =
73 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ).comp
75 (X := X) (Y := Y) (F := F) (F' := F') hκ η
77 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
78 ι) := by
79 classical
80 apply linearMap_ext_pi_single
81 intro x
82 have hchain := allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp
83 (X := Y) (Y := Z) (F := F') (F' := F'') (H := H)
84 hκ hmu θ hθ_continuous φ (η (ι x))
85 simpa [LinearMap.comp_apply,
90omit [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
91 [TopologicalSpace F] [IsTopologicalGroup F] in
92/-- Completed Fox-Jacobian functoriality for two composable continuous free pro-`C` source maps,
93as a matrix product. -/
95 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
97 (ProC := ProCGroups.ProC.allFiniteProC) κ)
99 (ProC := ProCGroups.ProC.allFiniteProC) mu)
100 (η : F →* F') (θ : F' →* F'') (hθ_continuous : Continuous θ) (φ : Z → H) :
102 (X := X) (Y := Z) (F := F) (F' := F'') hmu (θ.comp η) φ ι =
104 (X := X) (Y := Y) (F := F) (F' := F') hκ η
106 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
107 ι *
109 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ := by
110 apply Matrix.ext
111 intro x z
112 have h := congrFun
114 (X := Y) (Y := Z) (F := F') (F' := F'') (H := H)
115 hκ hmu θ hθ_continuous φ (η (ι x))) z
116 simpa [Matrix.mul_apply,
121/-- Three-term completed pro-`C` Fox chain rule, vector form. -/
123 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
125 (ProC := ProCGroups.ProC.allFiniteProC) ι)
127 (ProC := ProCGroups.ProC.allFiniteProC) κ)
129 (ProC := ProCGroups.ProC.allFiniteProC) mu)
130 (η : F →* F') (hη_continuous : Continuous η)
131 (θ : F' →* F'') (hθ_continuous : Continuous θ) (φ : Z → H) (g : F) :
133 (ProC := ProCGroups.ProC.allFiniteProC) hmu
134 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Z H) φ
135 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) Z H φ) (θ (η g)) =
137 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ
139 (X := X) (Y := Y) (F := F) (F' := F') hκ η
141 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
142 ι
144 (ProC := ProCGroups.ProC.allFiniteProC) hι
145 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
147 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
148 hκ hmu η θ φ ι)
149 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) X H
151 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
152 hκ hmu η θ φ ι)) g)) := by
153 calc
155 (ProC := ProCGroups.ProC.allFiniteProC) hmu
156 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Z H) φ
157 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) Z H φ) (θ (η g)) =
159 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ
161 (ProC := ProCGroups.ProC.allFiniteProC) hκ
162 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H)
164 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
165 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) Y H
167 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)) (η g)) := by
169 (X := Y) (Y := Z) (F := F') (F' := F'') (H := H)
170 hκ hmu θ hθ_continuous φ (η g)
171 _ =
173 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ
175 (X := X) (Y := Y) (F := F) (F' := F') hκ η
177 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
178 ι
180 (ProC := ProCGroups.ProC.allFiniteProC) hι
181 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
183 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
184 hκ hmu η θ φ ι)
185 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) X H
187 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
188 hκ hmu η θ φ ι)) g)) := by
189 exact congrArg
191 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ)
193 (X := X) (Y := Y) (F := F) (F' := F') (H := H)
194 hι hκ η hη_continuous
196 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ) g)
198/-- Three-term completed pro-`C` Fox chain rule, matrix form. -/
200 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
202 (ProC := ProCGroups.ProC.allFiniteProC) ι)
204 (ProC := ProCGroups.ProC.allFiniteProC) κ)
206 (ProC := ProCGroups.ProC.allFiniteProC) mu)
207 (η : F →* F') (hη_continuous : Continuous η)
208 (θ : F' →* F'') (hθ_continuous : Continuous θ) (φ : Z → H) (g : F) :
210 (ProC := ProCGroups.ProC.allFiniteProC) hmu
211 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Z H) φ
212 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) Z H φ) (θ (η g)) =
213 Matrix.vecMul
214 (Matrix.vecMul
216 (ProC := ProCGroups.ProC.allFiniteProC) hι
217 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
219 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
220 hκ hmu η θ φ ι)
221 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) X H
223 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
224 hκ hmu η θ φ ι)) g)
226 (X := X) (Y := Y) (F := F) (F' := F') hκ η
228 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
229 ι))
231 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ) := by
233 (X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
234 hι hκ hmu η hη_continuous θ hθ_continuous φ g]
238/-- Three-term completed pro-`C` Fox chain rule, component form. -/
240 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
242 (ProC := ProCGroups.ProC.allFiniteProC) ι)
244 (ProC := ProCGroups.ProC.allFiniteProC) κ)
246 (ProC := ProCGroups.ProC.allFiniteProC) mu)
247 (η : F →* F') (hη_continuous : Continuous η)
248 (θ : F' →* F'') (hθ_continuous : Continuous θ) (φ : Z → H) (g : F) (z : Z) :
250 (ProC := ProCGroups.ProC.allFiniteProC) hmu
251 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Z H) φ
252 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) Z H φ) (θ (η g)) z =
253 ∑ y : Y,
254 (∑ x : X,
256 (ProC := ProCGroups.ProC.allFiniteProC) hι
257 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
259 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
260 hκ hmu η θ φ ι)
261 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) X H
263 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
264 hκ hmu η θ φ ι)) g x *
266 (X := X) (Y := Y) (F := F) (F' := F') hκ η
268 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
269 ι x y) *
271 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ y z := by
272 have h := congrFun
274 (X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
275 hι hκ hmu η hη_continuous θ hθ_continuous φ g) z
276 simpa [Matrix.vecMul, dotProduct,
279omit [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X] [IsTopologicalGroup F] in
280/-- Continuous-homomorphism form of completed Fox-Jacobian functoriality, as a composition of
283 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
285 (ProC := ProCGroups.ProC.allFiniteProC) κ)
287 (ProC := ProCGroups.ProC.allFiniteProC) mu)
288 (η : F →ₜ* F') (θ : F' →ₜ* F'') (φ : Z → H) :
290 (X := X) (Y := Z) (F := F) (F' := F'') hmu
291 (θ.toMonoidHom.comp η.toMonoidHom) φ ι =
293 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ.toMonoidHom φ κ).comp
295 (X := X) (Y := Y) (F := F) (F' := F') hκ η.toMonoidHom
297 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ.toMonoidHom φ κ)
298 ι) := by
300 (X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
301 hκ hmu η.toMonoidHom θ.toMonoidHom θ.continuous_toFun φ
303omit [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
304 [IsTopologicalGroup F] in
305/-- Continuous-homomorphism form of completed Fox-Jacobian functoriality, as a matrix product. -/
307 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
309 (ProC := ProCGroups.ProC.allFiniteProC) κ)
311 (ProC := ProCGroups.ProC.allFiniteProC) mu)
312 (η : F →ₜ* F') (θ : F' →ₜ* F'') (φ : Z → H) :
314 (X := X) (Y := Z) (F := F) (F' := F'') hmu
315 (θ.toMonoidHom.comp η.toMonoidHom) φ ι =
317 (X := X) (Y := Y) (F := F) (F' := F') hκ η.toMonoidHom
319 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ.toMonoidHom φ κ)
320 ι *
322 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ.toMonoidHom φ κ := by
324 (X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
325 hκ hmu η.toMonoidHom θ.toMonoidHom θ.continuous_toFun φ
327/-- Continuous-homomorphism form of the three-term completed pro-`C` Fox chain rule. -/
329 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
331 (ProC := ProCGroups.ProC.allFiniteProC) ι)
333 (ProC := ProCGroups.ProC.allFiniteProC) κ)
335 (ProC := ProCGroups.ProC.allFiniteProC) mu)
336 (η : F →ₜ* F') (θ : F' →ₜ* F'') (φ : Z → H) (g : F) :
338 (ProC := ProCGroups.ProC.allFiniteProC) hmu
340 ProCGroups.ProC.allFiniteProC.finiteQuotientClass Z H) φ
342 (ProC := ProCGroups.ProC.allFiniteProC) Z H φ) (θ (η g)) =
344 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ.toMonoidHom φ κ
346 (X := X) (Y := Y) (F := F) (F' := F') hκ η.toMonoidHom
348 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ.toMonoidHom φ κ)
349 ι
351 (ProC := ProCGroups.ProC.allFiniteProC) hι
353 ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
355 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
356 hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)
358 (ProC := ProCGroups.ProC.allFiniteProC) X H
360 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
361 hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)) g)) := by
363 (X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
364 hι hκ hmu η.toMonoidHom η.continuous_toFun θ.toMonoidHom θ.continuous_toFun φ g
366/-- Continuous-homomorphism form of the three-term completed pro-`C` Fox chain rule, matrix
367form. -/
368theorem allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp_comp_matrix_continuousMonoidHom
369 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
371 (ProC := ProCGroups.ProC.allFiniteProC) ι)
373 (ProC := ProCGroups.ProC.allFiniteProC) κ)
375 (ProC := ProCGroups.ProC.allFiniteProC) mu)
376 (η : F →ₜ* F') (θ : F' →ₜ* F'') (φ : Z → H) (g : F) :
378 (ProC := ProCGroups.ProC.allFiniteProC) hmu
380 ProCGroups.ProC.allFiniteProC.finiteQuotientClass Z H) φ
382 (ProC := ProCGroups.ProC.allFiniteProC) Z H φ) (θ (η g)) =
383 Matrix.vecMul
384 (Matrix.vecMul
386 (ProC := ProCGroups.ProC.allFiniteProC) hι
388 ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
390 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
391 hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)
393 (ProC := ProCGroups.ProC.allFiniteProC) X H
395 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
396 hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)) g)
398 (X := X) (Y := Y) (F := F) (F' := F') hκ η.toMonoidHom
400 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ.toMonoidHom φ κ)
401 ι))
403 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ.toMonoidHom φ κ) := by
405 (X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
406 hι hκ hmu η.toMonoidHom η.continuous_toFun θ.toMonoidHom θ.continuous_toFun φ g
408/-- Continuous-homomorphism form of the three-term completed pro-`C` Fox chain rule, component
409form. -/
411 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
413 (ProC := ProCGroups.ProC.allFiniteProC) ι)
415 (ProC := ProCGroups.ProC.allFiniteProC) κ)
417 (ProC := ProCGroups.ProC.allFiniteProC) mu)
418 (η : F →ₜ* F') (θ : F' →ₜ* F'') (φ : Z → H) (g : F) (z : Z) :
420 (ProC := ProCGroups.ProC.allFiniteProC) hmu
422 ProCGroups.ProC.allFiniteProC.finiteQuotientClass Z H) φ
424 (ProC := ProCGroups.ProC.allFiniteProC) Z H φ) (θ (η g)) z =
425 ∑ y : Y,
426 (∑ x : X,
428 (ProC := ProCGroups.ProC.allFiniteProC) hι
430 ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
432 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
433 hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)
435 (ProC := ProCGroups.ProC.allFiniteProC) X H
437 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
438 hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)) g x *
440 (X := X) (Y := Y) (F := F) (F' := F') hκ η.toMonoidHom
442 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ.toMonoidHom φ κ)
443 ι x y) *
445 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ.toMonoidHom φ κ y z := by
447 (X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
448 hι hκ hmu η.toMonoidHom η.continuous_toFun θ.toMonoidHom θ.continuous_toFun φ g z
450end AllFiniteIteratedChainRule
452end
454end FoxDifferential