Yamaguchi Lean 4 Library
FoxDifferential/Completed/Continuous/ChainRule/Basic.lean
FoxDifferential/Completed/Continuous/ChainRule/Basic/Source

FoxDifferential/Completed/Continuous/ChainRule/Basic.lean

1import FoxDifferential.Completed.Continuous.Free.Rules
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/Continuous/ChainRule/Basic.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 v
24section AllFiniteChainRule
26variable {X Y F F' H : Type u}
27variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
28variable [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
29variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
30variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
31variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
32variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
34/-- The target generator map pulled back along a continuous homomorphism of free pro-`C` sources. -/
36 {κ : Y → F'}
39 (η : F →* F') (φ : Y → H) (ι : X → F) : X → H :=
40 fun x =>
43 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H) φ
45 (η (ι x))
47/-- The completed Fox-Jacobian family of a continuous homomorphism between free pro-`C` sources. -/
49 {κ : Y → F'}
52 (η : F →* F') (φ : Y → H) (ι : X → F) :
53 X → ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := Y) (H := H) :=
54 fun x =>
57 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H) φ
59 (η (ι x))
61/-- The completed Fox-Jacobian family as a finite linear map on completed coordinate vectors. -/
63 {κ : Y → F'}
66 (η : F →* F') (φ : Y → H) (ι : X → F) :
68 ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := X) (H := H) →ₗ[
69 ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H]
70 ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := Y) (H := H) :=
72 (allFiniteProC_freeProCZCCompletedFoxJacobian (X := X) (F := F) hκ η φ ι)
74/-- The completed Fox-Jacobian packaged as a matrix. -/
76 {κ : Y → F'}
79 (η : F →* F') (φ : Y → H) (ι : X → F) :
80 Matrix X Y (ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H) :=
82 (allFiniteProC_freeProCZCCompletedFoxJacobian (X := X) (F := F) hκ η φ ι)
84/-- A finite-stage projection of the completed Fox-Jacobian matrix. -/
86 {κ : Y → F'}
89 (η : F →* F') (φ : Y → H) (ι : X → F)
90 (j : ZCCompletedGroupAlgebraIndex ProCGroups.ProC.allFiniteProC.finiteQuotientClass H) :
91 Matrix X Y (ZCCompletedGroupAlgebraStage ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j) :=
92 fun x y =>
93 zcCompletedGroupAlgebraProjection ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j
95 (X := X) (F := F) hκ η φ ι x y)
97omit [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
98 [TopologicalSpace F] [IsTopologicalGroup F] in
99/-- Matrix evaluation is componentwise the completed Fox-Jacobian family. -/
100@[simp]
102 {κ : Y → F'}
105 (η : F →* F') (φ : Y → H) (ι : X → F)
106 (x : X) (y : Y) :
108 (X := X) (F := F) hκ η φ ι x y =
110 (X := X) (F := F) hκ η φ ι x y :=
111 rfl
113omit [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
114 [TopologicalSpace F] [IsTopologicalGroup F] in
115/-- Evaluation of the finite-stage completed Fox-Jacobian matrix. -/
116@[simp]
118 {κ : Y → F'}
121 (η : F →* F') (φ : Y → H) (ι : X → F)
122 (j : ZCCompletedGroupAlgebraIndex ProCGroups.ProC.allFiniteProC.finiteQuotientClass H) (x : X) (y : Y) :
124 (X := X) (F := F) hκ η φ ι j x y =
125 zcCompletedGroupAlgebraProjection ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j
127 (X := X) (F := F) hκ η φ ι x y) :=
128 rfl
130omit [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
131 [TopologicalSpace F] [IsTopologicalGroup F] in
132/-- Evaluation formula for the completed Fox-Jacobian linear map. -/
133@[simp]
135 {κ : Y → F'}
138 (η : F →* F') (φ : Y → H) (ι : X → F)
139 (v : ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := X) (H := H)) (y : Y) :
141 (X := X) (F := F) hκ η φ ι v y =
142 ∑ x : X,
144 (X := X) (F := F) hκ η φ ι x y :=
145 rfl
147omit [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
148 [TopologicalSpace F] [IsTopologicalGroup F] in
149/-- The completed Fox-Jacobian linear map is row-vector multiplication by its matrix. -/
151 {κ : Y → F'}
154 (η : F →* F') (φ : Y → H) (ι : X → F)
155 (v : ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := X) (H := H)) :
157 (X := X) (F := F) hκ η φ ι v =
158 Matrix.vecMul v
160 (X := X) (F := F) hκ η φ ι) := by
162 (allFiniteProC_freeProCZCCompletedFoxJacobian (X := X) (F := F) hκ η φ ι) v
164omit [Fintype X] in
165/-- The canonical right homomorphism for the pulled-back generator map is the composite of the
166target right homomorphism with the source homomorphism. -/
168 {ι : X → F} {κ : Y → F'}
173 (η : F →* F') (hη_continuous : Continuous η) (φ : Y → H) :
176 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
178 (X := X) (F := F) hκ η φ ι)
181 (X := X) (F := F) hκ η φ ι)) =
184 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H) φ
187 (G := ZCCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H) :=
188 allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H
190 (G := ZCCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H) :=
191 allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H
194 let φX : X → H :=
196 (X := X) (F := F) hκ η φ ι
199 have hHtarget : ProCGroups.ProC.allFiniteProC (G := H) :=
201 (G := H)
202 (by
203 exact
204 (⟨inferInstance, inferInstance, inferInstance, inferInstance⟩ :
206 apply hι.hom_ext hHtarget
208 (ProC := ProCGroups.ProC.allFiniteProC) X H hι htargetX φX hφX
210 (ProC := ProCGroups.ProC.allFiniteProC) Y H hκ htargetY φ hφY).comp hη_continuous
211 · intro x
214 MonoidHom.coe_comp, Function.comp_apply]
216/-- Completed pro-`C` Fox chain rule, vector form. -/
218 {ι : X → F} {κ : Y → F'}
223 (η : F →* F') (hη_continuous : Continuous η) (φ : Y → H) (g : F) :
226 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H) φ
229 (X := X) (F := F) hκ η φ ι
232 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
234 (X := X) (F := F) hκ η φ ι)
237 (X := X) (F := F) hκ η φ ι)) g) := by
239 (G := ZCCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H) :=
240 allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H
242 (G := ZCCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H) :=
243 allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H
246 let ρY : F' →* H :=
248 hκ htargetY φ hφY
249 let DY : F' → ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := Y) (H := H) :=
251 hκ htargetY φ hφY
252 let φX : X → H :=
254 (X := X) (F := F) hκ η φ ι
257 let ρX : F →* H :=
259 hι htargetX φX hφX
260 let DX : F → ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := X) (H := H) :=
262 hι htargetX φX hφX
263 let jac : X → ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := Y) (H := H) :=
265 (X := X) (F := F) hκ η φ ι
266 let L :
268 ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := X) (H := H) →ₗ[
269 ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H]
270 ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := Y) (H := H) :=
272 (X := X) (F := F) hκ η φ ι
273 let beta : F → ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := Y) (H := H) := fun g => DY (η g)
274 let gamma : F → ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := Y) (H := H) := fun g => L (DX g)
275 have hρX : ρX = ρY.comp η := by
276 simpa [ρX, ρY, φX, htargetX, htargetY, hφX, hφY] using
278 (X := X) (Y := Y) (F := F) (F' := F') (H := H) hι hκ η hη_continuous φ
279 have hbeta_cross : IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProCGroups.ProC.allFiniteProC.finiteQuotientClass ρX) beta := by
280 intro a b
282 (ProC := ProCGroups.ProC.allFiniteProC) hκ htargetY φ hφY (η a) (η b)
283 simpa [beta, DY, hρX, MonoidHom.comp_apply] using hDY
284 have hgamma_cross : IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProCGroups.ProC.allFiniteProC.finiteQuotientClass ρX) gamma := by
285 exact IsCrossedDifferential.map_linear
287 (ProC := ProCGroups.ProC.allFiniteProC) hι htargetX φX hφX) L
288 have hbeta_continuous : Continuous beta := by
290 (ProC := ProCGroups.ProC.allFiniteProC) Y H hκ htargetY φ hφY).comp hη_continuous
291 have hgamma_continuous : Continuous gamma := by
292 refine continuous_pi fun y => ?_
293 change Continuous (fun g : F => ∑ x : X, DX g x * jac x y)
294 exact continuous_finset_sum _ fun x _ =>
295 ((continuous_apply x).comp
297 (ProC := ProCGroups.ProC.allFiniteProC) X H hι htargetX φX hφX)).mul
298 continuous_const
299 have hgen : ∀ x : X, beta (ι x) = gamma (ι x) := by
300 intro x
301 have hsingle :
302 L ((Pi.single x (1 : ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H)) :
303 ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := X) (H := H)) = jac x := by
305 simpa [beta, gamma, DX, jac] using hsingle.symm
306 let f : F →* ZCCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H :=
308 (X := Y) (F := F) (H := H) ρX beta hbeta_cross
309 let h : F →* ZCCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H :=
311 (X := Y) (F := F) (H := H) ρX gamma hgamma_cross
312 have hf_continuous : Continuous f :=
314 (X := Y) (F := F) (H := H) ρX beta hbeta_cross hbeta_continuous
316 (ProC := ProCGroups.ProC.allFiniteProC) X H hι htargetX φX hφX)
317 have hh_continuous : Continuous h :=
319 (X := Y) (F := F) (H := H) ρX gamma hgamma_cross hgamma_continuous
321 (ProC := ProCGroups.ProC.allFiniteProC) X H hι htargetX φX hφX)
322 have hfg : ∀ x : X, f (ι x) = h (ι x) := by
323 intro x
324 apply ZCCompletedFoxSemidirect.ext
325 · exact hgen x
326 · rfl
327 have hfh : f = h := hι.hom_ext htargetY hf_continuous hh_continuous hfg
328 have hleft := congrArg (fun q : F →* ZCCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H => (q g).left) hfh
329 simpa [f, h, beta, gamma, L, DY, DX, jac, htargetX, htargetY, hφY, hφX, ρY, ρX, φX,
334/-- Completed pro-`C` Fox chain rule, component form. -/
336 {ι : X → F} {κ : Y → F'}
341 (η : F →* F') (hη_continuous : Continuous η) (φ : Y → H) (g : F) (y : Y) :
344 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H) φ
346 ∑ x : X,
349 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
351 (X := X) (F := F) hκ η φ ι)
354 (X := X) (F := F) hκ η φ ι)) g x *
356 (X := X) (F := F) hκ η φ ι x y := by
357 have h := congrFun
359 (X := X) (Y := Y) (F := F) (F' := F') (H := H)
360 hι hκ η hη_continuous φ g) y
361 simpa using h
363/-- Completed pro-`C` Fox chain rule, matrix form. -/
365 {ι : X → F} {κ : Y → F'}
370 (η : F →* F') (hη_continuous : Continuous η) (φ : Y → H) (g : F) :
373 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H) φ
375 Matrix.vecMul
378 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
380 (X := X) (F := F) hκ η φ ι)
383 (X := X) (F := F) hκ η φ ι)) g)
385 (X := X) (F := F) hκ η φ ι) := by
387 (X := X) (Y := Y) (F := F) (F' := F') (H := H)
388 hι hκ η hη_continuous φ g]
390 (X := X) (F := F) hκ η φ ι
393 (allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
395 (X := X) (F := F) hκ η φ ι)
398 (X := X) (F := F) hκ η φ ι)) g)
400omit [Fintype X] in
401/-- Continuous-homomorphism form of the right-homomorphism chain rule. -/
403 {ι : X → F} {κ : Y → F'}
408 (η : F →ₜ* F') (φ : Y → H) :
412 ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
414 (X := X) (F := F) hκ η.toMonoidHom φ ι)
418 (X := X) (F := F) hκ η.toMonoidHom φ ι)) =
422 ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H) φ
424 (ProC := ProCGroups.ProC.allFiniteProC) Y H φ)).comp η.toMonoidHom := by
426 (X := X) (Y := Y) (F := F) (F' := F') (H := H)
427 hι hκ η.toMonoidHom η.continuous_toFun φ
429/-- Continuous-homomorphism form of the completed pro-`C` Fox chain rule, vector form. -/
431 {ι : X → F} {κ : Y → F'}
436 (η : F →ₜ* F') (φ : Y → H) (g : F) :
440 ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H) φ
442 (ProC := ProCGroups.ProC.allFiniteProC) Y H φ) (η g) =
444 (X := X) (F := F) hκ η.toMonoidHom φ ι
448 ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
450 (X := X) (F := F) hκ η.toMonoidHom φ ι)
454 (X := X) (F := F) hκ η.toMonoidHom φ ι)) g) := by
456 (X := X) (Y := Y) (F := F) (F' := F') (H := H)
457 hι hκ η.toMonoidHom η.continuous_toFun φ g
459/-- Continuous-homomorphism form of the completed pro-`C` Fox chain rule, component form. -/
461 {ι : X → F} {κ : Y → F'}
466 (η : F →ₜ* F') (φ : Y → H) (g : F) (y : Y) :
470 ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H) φ
472 (ProC := ProCGroups.ProC.allFiniteProC) Y H φ) (η g) y =
473 ∑ x : X,
477 ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
479 (X := X) (F := F) hκ η.toMonoidHom φ ι)
483 (X := X) (F := F) hκ η.toMonoidHom φ ι)) g x *
485 (X := X) (F := F) hκ η.toMonoidHom φ ι x y := by
487 (X := X) (Y := Y) (F := F) (F' := F') (H := H)
488 hι hκ η.toMonoidHom η.continuous_toFun φ g y
490/-- Continuous-homomorphism form of the completed pro-`C` Fox chain rule, matrix form. -/
492 {ι : X → F} {κ : Y → F'}
497 (η : F →ₜ* F') (φ : Y → H) (g : F) :
501 ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H) φ
503 (ProC := ProCGroups.ProC.allFiniteProC) Y H φ) (η g) =
504 Matrix.vecMul
508 ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
510 (X := X) (F := F) hκ η.toMonoidHom φ ι)
514 (X := X) (F := F) hκ η.toMonoidHom φ ι)) g)
516 (X := X) (F := F) hκ η.toMonoidHom φ ι) := by
518 (X := X) (Y := Y) (F := F) (F' := F') (H := H)
519 hι hκ η.toMonoidHom η.continuous_toFun φ g
521end AllFiniteChainRule
523end
525end FoxDifferential