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

Source: ProCGroups.FoxDifferential.Completed.Continuous.ChainRule.Basic

1import ProCGroups.FoxDifferential.Completed.Continuous.Free.Rules
3/-!
4# Fox differential: completed — continuous — chain rule — basic
6The principal declarations in this module are:
8- `allFinite_freeProCZCCompletedFoxPullbackGenerator`
9 The target generator map pulled back along a continuous homomorphism of free pro-\(C\) sources.
10- `allFinite_freeProCZCCompletedFoxJacobian`
11 The completed Fox-Jacobian family of a continuous homomorphism between free pro-\(C\) sources.
12- `allFinite_freeProCZCCompletedFoxJacobianMatrix_apply`
13 The matrix evaluation is componentwise the completed Fox-Jacobian family.
14- `allFinite_freeProCZCCompletedFoxJacobianMatrixStage_apply`
15 Evaluation of the finite-stage completed Fox-Jacobian matrix.
16-/
18namespace FoxDifferential
20noncomputable section
22open scoped BigOperators
24universe u v
26section AllFiniteChainRule
28variable {X Y F F' H : Type u}
29variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
30variable [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
31variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
32variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
33variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
34variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
35variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
36variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
38/--
39The target generator map pulled back along a continuous homomorphism of free pro-\(C\) sources.
40-/
41def allFinite_freeProCZCCompletedFoxPullbackGenerator
42 {κ : Y → F'}
45 (η : F →* F') (φ : Y → H) (ι : X → F) : X → H :=
46 fun x =>
47 freeProCZCCompletedFoxRightHom
49 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
50 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
52 (η (ι x))
54/--
55The completed Fox-Jacobian family of a continuous homomorphism between free pro-\(C\) sources.
56-/
57def allFinite_freeProCZCCompletedFoxJacobian
58 {κ : Y → F'}
61 (η : F →* F') (φ : Y → H) (ι : X → F) :
62 X → ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := Y) (H := H) :=
63 fun x =>
64 freeProCZCCompletedFoxDerivativeVector
66 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
67 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
69 (η (ι x))
71/--
72The completed Fox-Jacobian family is bundled into a finite linear map on completed coordinate
73vectors.
74-/
75def allFinite_freeProCZCCompletedFoxJacobianLinearMap
76 {κ : Y → F'}
79 (η : F →* F') (φ : Y → H) (ι : X → F) :
80 ZCFreeFoxCoordinates
81 ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H) →ₗ[
82 ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H]
83 ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := Y) (H := H) :=
84 foxJacobianLinearMap
85 (allFinite_freeProCZCCompletedFoxJacobian (X := X) (F := F) hκ η φ ι)
87/-- The completed Fox-Jacobian is packaged as a matrix. -/
88def allFinite_freeProCZCCompletedFoxJacobianMatrix
89 {κ : Y → F'}
92 (η : F →* F') (φ : Y → H) (ι : X → F) :
93 Matrix X Y (ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H) :=
94 foxJacobianMatrix
95 (allFinite_freeProCZCCompletedFoxJacobian (X := X) (F := F) hκ η φ ι)
97/-- A finite-stage projection of the completed Fox-Jacobian matrix. -/
98def allFinite_freeProCZCCompletedFoxJacobianMatrixStage
99 {κ : Y → F'}
102 (η : F →* F') (φ : Y → H) (ι : X → F)
103 (j : ZCCompletedGroupAlgebraIndex ProCGroups.FiniteGroupClass.allFinite H) :
104 Matrix X Y (ZCCompletedGroupAlgebraStage ProCGroups.FiniteGroupClass.allFinite H j) :=
105 fun x y =>
106 zcCompletedGroupAlgebraProjection ProCGroups.FiniteGroupClass.allFinite H j
107 (allFinite_freeProCZCCompletedFoxJacobianMatrix
108 (X := X) (F := F) hκ η φ ι x y)
110omit [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
111 [TopologicalSpace F] [IsTopologicalGroup F] in
112/-- The matrix evaluation is componentwise the completed Fox-Jacobian family. -/
113@[simp]
114theorem allFinite_freeProCZCCompletedFoxJacobianMatrix_apply
115 {κ : Y → F'}
118 (η : F →* F') (φ : Y → H) (ι : X → F)
119 (x : X) (y : Y) :
120 allFinite_freeProCZCCompletedFoxJacobianMatrix
121 (X := X) (F := F) hκ η φ ι x y =
122 allFinite_freeProCZCCompletedFoxJacobian
123 (X := X) (F := F) hκ η φ ι x y :=
124 rfl
126omit [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
127 [TopologicalSpace F] [IsTopologicalGroup F] in
128/-- Evaluation of the finite-stage completed Fox-Jacobian matrix. -/
129@[simp]
130theorem allFinite_freeProCZCCompletedFoxJacobianMatrixStage_apply
131 {κ : Y → F'}
134 (η : F →* F') (φ : Y → H) (ι : X → F)
135 (j : ZCCompletedGroupAlgebraIndex ProCGroups.FiniteGroupClass.allFinite H) (x : X) (y : Y) :
136 allFinite_freeProCZCCompletedFoxJacobianMatrixStage
137 (X := X) (F := F) hκ η φ ι j x y =
138 zcCompletedGroupAlgebraProjection ProCGroups.FiniteGroupClass.allFinite H j
139 (allFinite_freeProCZCCompletedFoxJacobianMatrix
140 (X := X) (F := F) hκ η φ ι x y) :=
141 rfl
143omit [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
144 [TopologicalSpace F] [IsTopologicalGroup F] in
145/--
146The all-finite pro-\(C\) completed Fox-Jacobian linear map is evaluated coordinatewise at each
147finite quotient stage.
148-/
149@[simp]
150theorem allFinite_freeProCZCCompletedFoxJacobianLinearMap_apply
151 {κ : Y → F'}
154 (η : F →* F') (φ : Y → H) (ι : X → F)
155 (v : ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H)) (y : Y) :
156 allFinite_freeProCZCCompletedFoxJacobianLinearMap
157 (X := X) (F := F) hκ η φ ι v y =
158 ∑ x : X,
159 v x * allFinite_freeProCZCCompletedFoxJacobian
160 (X := X) (F := F) hκ η φ ι x y :=
161 rfl
163omit [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
164 [TopologicalSpace F] [IsTopologicalGroup F] in
165/-- The completed Fox-Jacobian linear map is row-vector multiplication by its matrix. -/
166theorem allFinite_freeProCZCCompletedFoxJacobianLinearMap_eq_vecMul
167 {κ : Y → F'}
170 (η : F →* F') (φ : Y → H) (ι : X → F)
171 (v : ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H)) :
172 allFinite_freeProCZCCompletedFoxJacobianLinearMap
173 (X := X) (F := F) hκ η φ ι v =
174 Matrix.vecMul v
175 (allFinite_freeProCZCCompletedFoxJacobianMatrix
176 (X := X) (F := F) hκ η φ ι) := by
177 exact foxJacobianLinearMap_eq_vecMul
178 (allFinite_freeProCZCCompletedFoxJacobian (X := X) (F := F) hκ η φ ι) v
180omit [Fintype X] in
181/--
182The canonical right homomorphism for the pulled-back generator map is the composite of the
183target right homomorphism with the source homomorphism.
184-/
185theorem allFinite_freeProCZCCompletedFoxRightHom_comp
186 {ι : X → F} {κ : Y → F'}
191 (η : F →* F') (hη_continuous : Continuous η) (φ : Y → H) :
192 freeProCZCCompletedFoxRightHom
194 (ProCGrp.allFinite_property (ProfiniteGrp.of _))
195 (allFinite_freeProCZCCompletedFoxPullbackGenerator
196 (X := X) (F := F) hκ η φ ι)
197 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
199 (allFinite_freeProCZCCompletedFoxPullbackGenerator
200 (X := X) (F := F) hκ η φ ι)) =
201 (freeProCZCCompletedFoxRightHom
203 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
204 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
206 let htargetX :
208 (ZCCompletedFoxSemidirect ProCGroups.FiniteGroupClass.allFinite X H) :=
209 ProCGrp.allFinite_property (ProfiniteGrp.of _)
210 let htargetY :
212 (ZCCompletedFoxSemidirect ProCGroups.FiniteGroupClass.allFinite Y H) :=
213 ProCGrp.allFinite_property (ProfiniteGrp.of _)
214 let hφY : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C :=
216 continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
218 let φX : X → H :=
219 allFinite_freeProCZCCompletedFoxPullbackGenerator
220 (X := X) (F := F) hκ η φ ι
221 let hφX : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C :=
223 continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
225 have hHtarget :
227 ProCGrp.allFinite_property (ProfiniteGrp.of H)
228 apply hι.hom_ext hHtarget
229 · exact continuous_freeProCZCCompletedFoxRightHom
230 (C := ProCGroups.FiniteGroupClass.allFinite) X H hι htargetX φX hφX
231 · exact (continuous_freeProCZCCompletedFoxRightHom
232 (C := ProCGroups.FiniteGroupClass.allFinite) Y H hκ htargetY φ hφY).comp hη_continuous
233 · intro x
234 simp only [freeProCZCCompletedFoxRightHom_apply, freeProCZCCompletedFoxSemidirectLift_generator,
235 freeProCZCCompletedFoxSemidirectGenerator_right,
236 allFinite_freeProCZCCompletedFoxPullbackGenerator,
237 MonoidHom.coe_comp, Function.comp_apply]
239/-- Completed pro-\(C\) Fox chain rule in vector form. -/
240theorem allFinite_freeProCZCCompletedFoxDerivativeVector_comp
241 {ι : X → F} {κ : Y → F'}
246 (η : F →* F') (hη_continuous : Continuous η) (φ : Y → H) (g : F) :
247 freeProCZCCompletedFoxDerivativeVector
249 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
250 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
252 allFinite_freeProCZCCompletedFoxJacobianLinearMap
253 (X := X) (F := F) hκ η φ ι
254 (freeProCZCCompletedFoxDerivativeVector
256 (ProCGrp.allFinite_property (ProfiniteGrp.of _))
257 (allFinite_freeProCZCCompletedFoxPullbackGenerator
258 (X := X) (F := F) hκ η φ ι)
259 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
261 (allFinite_freeProCZCCompletedFoxPullbackGenerator
262 (X := X) (F := F) hκ η φ ι)) g) := by
263 let htargetX :
265 (ZCCompletedFoxSemidirect ProCGroups.FiniteGroupClass.allFinite X H) :=
266 ProCGrp.allFinite_property (ProfiniteGrp.of _)
267 let htargetY :
269 (ZCCompletedFoxSemidirect ProCGroups.FiniteGroupClass.allFinite Y H) :=
270 ProCGrp.allFinite_property (ProfiniteGrp.of _)
271 let hφY : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C :=
273 continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
275 let ρY : F' →* H :=
276 freeProCZCCompletedFoxRightHom (C := ProCGroups.FiniteGroupClass.allFinite)
277 hκ htargetY φ hφY
278 let DY : ScalarCrossedHom
279 (zcCompletedGroupAlgebraScalar ProCGroups.FiniteGroupClass.allFinite ρY)
280 (ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := Y) (H := H)) :=
281 freeProCZCCompletedFoxDerivativeVector (C := ProCGroups.FiniteGroupClass.allFinite)
282 hκ htargetY φ hφY
283 let φX : X → H :=
284 allFinite_freeProCZCCompletedFoxPullbackGenerator
285 (X := X) (F := F) hκ η φ ι
286 let hφX : Continuous (freeProCZCCompletedFoxSemidirectGenerator (C :=
288 continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
290 let ρX : F →* H :=
291 freeProCZCCompletedFoxRightHom (C := ProCGroups.FiniteGroupClass.allFinite)
292 hι htargetX φX hφX
293 let DX : ScalarCrossedHom
294 (zcCompletedGroupAlgebraScalar ProCGroups.FiniteGroupClass.allFinite ρX)
295 (ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H)) :=
296 freeProCZCCompletedFoxDerivativeVector (C := ProCGroups.FiniteGroupClass.allFinite)
297 hι htargetX φX hφX
298 let jac : X → ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := Y) (H := H) :=
299 allFinite_freeProCZCCompletedFoxJacobian
300 (X := X) (F := F) hκ η φ ι
301 let L :
302 ZCFreeFoxCoordinates
303 ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H) →ₗ[
304 ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H]
305 ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := Y) (H := H) :=
306 allFinite_freeProCZCCompletedFoxJacobianLinearMap
307 (X := X) (F := F) hκ η φ ι
308 have hρX : ρX = ρY.comp η := by
309 simpa [ρX, ρY, φX, htargetX, htargetY, hφX, hφY] using
310 allFinite_freeProCZCCompletedFoxRightHom_comp
311 (X := X) (Y := Y) (F := F) (F' := F') (H := H) hι hκ η hη_continuous φ
312 let beta : ScalarCrossedHom
313 (zcCompletedGroupAlgebraScalar ProCGroups.FiniteGroupClass.allFinite ρX)
314 (ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := Y) (H := H)) := {
315 toFun g := DY (η g)
316 map_mul' a b := by
317 simpa [DY, hρX, map_mul, MonoidHom.comp_apply] using
318 ScalarCrossedHom.map_mul DY (η a) (η b) }
319 let gamma : ScalarCrossedHom
320 (zcCompletedGroupAlgebraScalar ProCGroups.FiniteGroupClass.allFinite ρX)
321 (ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := Y) (H := H)) :=
322 DX.mapLinear L
323 have hbeta_continuous : Continuous beta := by
324 change Continuous (fun g : F => DY (η g))
325 exact (continuous_freeProCZCCompletedFoxDerivativeVector
326 (C := ProCGroups.FiniteGroupClass.allFinite) Y H hκ htargetY φ hφY).comp hη_continuous
327 have hgamma_continuous : Continuous gamma := by
328 refine continuous_pi fun y => ?_
329 change Continuous (fun g : F => ∑ x : X, DX g x * jac x y)
330 exact continuous_finsetSum _ fun x _ =>
331 ((continuous_apply x).comp
332 (continuous_freeProCZCCompletedFoxDerivativeVector
333 (C := ProCGroups.FiniteGroupClass.allFinite) X H hι htargetX φX hφX)).mul
334 continuous_const
335 have hgen : ∀ x : X, beta (ι x) = gamma (ι x) := by
336 intro x
337 have hsingle :
338 L ((Pi.single x (1 : ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H)) :
339 ZCFreeFoxCoordinates ProCGroups.FiniteGroupClass.allFinite (X := X) (H := H)) = jac x
340 := by
341 simp only [allFinite_freeProCZCCompletedFoxJacobianLinearMap, foxJacobianLinearMap_single,
342 L, jac]
343 change DY (η (ι x)) = L (DX (ι x))
344 calc
345 DY (η (ι x)) = jac x := by rfl
346 _ = L (Pi.single x
347 (1 : ZCCompletedGroupAlgebra ProCGroups.FiniteGroupClass.allFinite H)) :=
348 hsingle.symm
349 _ = L (DX (ι x)) := by
350 rw [freeProCZCCompletedFoxDerivativeVector_generator
352 hι htargetX φX hφX x]
353 let f : F →* ZCCompletedFoxSemidirect ProCGroups.FiniteGroupClass.allFinite Y H :=
354 freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
355 (X := Y) (F := F) (H := H) ρX beta
356 let h : F →* ZCCompletedFoxSemidirect ProCGroups.FiniteGroupClass.allFinite Y H :=
357 freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
358 (X := Y) (F := F) (H := H) ρX gamma
359 have hf_continuous : Continuous f :=
360 continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
361 (X := Y) (F := F) (H := H) ρX beta hbeta_continuous
362 (continuous_freeProCZCCompletedFoxRightHom
363 (C := ProCGroups.FiniteGroupClass.allFinite) X H hι htargetX φX hφX)
364 have hh_continuous : Continuous h :=
365 continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
366 (X := Y) (F := F) (H := H) ρX gamma hgamma_continuous
367 (continuous_freeProCZCCompletedFoxRightHom
368 (C := ProCGroups.FiniteGroupClass.allFinite) X H hι htargetX φX hφX)
369 have hfg : ∀ x : X, f (ι x) = h (ι x) := by
370 intro x
371 apply ZCCompletedFoxSemidirect.ext
372 · exact hgen x
373 · rfl
374 have hfh : f = h := hι.hom_ext htargetY hf_continuous hh_continuous hfg
375 have hleft := congrArg (fun q : F →* ZCCompletedFoxSemidirect
377 convert hleft using 1
378 all_goals
379 simp [f, h, beta, gamma, L, DY, DX, ρY, ρX, φX,
380 allFinite_freeProCZCCompletedFoxJacobianLinearMap]
381 all_goals rfl
383/-- Completed pro-\(C\) Fox chain rule in component form. -/
384theorem allFinite_freeProCZCCompletedFoxDerivativeVector_comp_apply
385 {ι : X → F} {κ : Y → F'}
390 (η : F →* F') (hη_continuous : Continuous η) (φ : Y → H) (g : F) (y : Y) :
391 freeProCZCCompletedFoxDerivativeVector
393 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
394 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
396 ∑ x : X,
397 freeProCZCCompletedFoxDerivativeVector
399 (ProCGrp.allFinite_property (ProfiniteGrp.of _))
400 (allFinite_freeProCZCCompletedFoxPullbackGenerator
401 (X := X) (F := F) hκ η φ ι)
402 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
404 (allFinite_freeProCZCCompletedFoxPullbackGenerator
405 (X := X) (F := F) hκ η φ ι)) g x *
406 allFinite_freeProCZCCompletedFoxJacobian
407 (X := X) (F := F) hκ η φ ι x y := by
408 have h := congrFun
409 (allFinite_freeProCZCCompletedFoxDerivativeVector_comp
410 (X := X) (Y := Y) (F := F) (F' := F') (H := H)
411 hι hκ η hη_continuous φ g) y
412 simpa using h
414/-- The completed pro-\(C\) Fox chain rule in matrix form. -/
415theorem allFinite_freeProCZCCompletedFoxDerivativeVector_comp_matrix
416 {ι : X → F} {κ : Y → F'}
421 (η : F →* F') (hη_continuous : Continuous η) (φ : Y → H) (g : F) :
422 freeProCZCCompletedFoxDerivativeVector
424 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
425 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
427 Matrix.vecMul
428 (freeProCZCCompletedFoxDerivativeVector
430 (ProCGrp.allFinite_property (ProfiniteGrp.of _))
431 (allFinite_freeProCZCCompletedFoxPullbackGenerator
432 (X := X) (F := F) hκ η φ ι)
433 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
435 (allFinite_freeProCZCCompletedFoxPullbackGenerator
436 (X := X) (F := F) hκ η φ ι)) g)
437 (allFinite_freeProCZCCompletedFoxJacobianMatrix
438 (X := X) (F := F) hκ η φ ι) := by
439 rw [allFinite_freeProCZCCompletedFoxDerivativeVector_comp
440 (X := X) (Y := Y) (F := F) (F' := F') (H := H)
441 hι hκ η hη_continuous φ g]
442 exact allFinite_freeProCZCCompletedFoxJacobianLinearMap_eq_vecMul
443 (X := X) (F := F) hκ η φ ι
444 (freeProCZCCompletedFoxDerivativeVector
446 (ProCGrp.allFinite_property (ProfiniteGrp.of _))
447 (allFinite_freeProCZCCompletedFoxPullbackGenerator
448 (X := X) (F := F) hκ η φ ι)
449 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
451 (allFinite_freeProCZCCompletedFoxPullbackGenerator
452 (X := X) (F := F) hκ η φ ι)) g)
454omit [Fintype X] in
455/-- Continuous-homomorphism form of the right-homomorphism chain rule. -/
456theorem allFinite_freeProCZCCompletedFoxRightHom_comp_continuousMonoidHom
457 {ι : X → F} {κ : Y → F'}
462 (η : F →ₜ* F') (φ : Y → H) :
463 freeProCZCCompletedFoxRightHom
465 (ProCGrp.allFinite_property (ProfiniteGrp.of _))
466 (allFinite_freeProCZCCompletedFoxPullbackGenerator
467 (X := X) (F := F) hκ η.toMonoidHom φ ι)
468 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
470 (allFinite_freeProCZCCompletedFoxPullbackGenerator
471 (X := X) (F := F) hκ η.toMonoidHom φ ι)) =
472 (freeProCZCCompletedFoxRightHom
474 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
475 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
476 ProCGroups.FiniteGroupClass.allFinite) Y H φ)).comp η.toMonoidHom := by
477 exact allFinite_freeProCZCCompletedFoxRightHom_comp
478 (X := X) (Y := Y) (F := F) (F' := F') (H := H)
479 hι hκ η.toMonoidHom η.continuous_toFun φ
481/-- Continuous-homomorphism form of the completed pro-\(C\) Fox chain rule in vector form. -/
482theorem allFinite_freeProCZCCompletedFoxDerivativeVector_comp_continuousMonoidHom
483 {ι : X → F} {κ : Y → F'}
488 (η : F →ₜ* F') (φ : Y → H) (g : F) :
489 freeProCZCCompletedFoxDerivativeVector
491 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
492 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
494 allFinite_freeProCZCCompletedFoxJacobianLinearMap
495 (X := X) (F := F) hκ η.toMonoidHom φ ι
496 (freeProCZCCompletedFoxDerivativeVector
498 (ProCGrp.allFinite_property (ProfiniteGrp.of _))
499 (allFinite_freeProCZCCompletedFoxPullbackGenerator
500 (X := X) (F := F) hκ η.toMonoidHom φ ι)
501 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
503 (allFinite_freeProCZCCompletedFoxPullbackGenerator
504 (X := X) (F := F) hκ η.toMonoidHom φ ι)) g) := by
505 exact allFinite_freeProCZCCompletedFoxDerivativeVector_comp
506 (X := X) (Y := Y) (F := F) (F' := F') (H := H)
507 hι hκ η.toMonoidHom η.continuous_toFun φ g
509/-- Continuous-homomorphism form of the completed pro-\(C\) Fox chain rule in component form. -/
510theorem allFinite_freeProCZCCompletedFoxDerivativeVector_comp_apply_continuousMonoidHom
511 {ι : X → F} {κ : Y → F'}
516 (η : F →ₜ* F') (φ : Y → H) (g : F) (y : Y) :
517 freeProCZCCompletedFoxDerivativeVector
519 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
520 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
522 ∑ x : X,
523 freeProCZCCompletedFoxDerivativeVector
525 (ProCGrp.allFinite_property (ProfiniteGrp.of _))
526 (allFinite_freeProCZCCompletedFoxPullbackGenerator
527 (X := X) (F := F) hκ η.toMonoidHom φ ι)
528 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
530 (allFinite_freeProCZCCompletedFoxPullbackGenerator
531 (X := X) (F := F) hκ η.toMonoidHom φ ι)) g x *
532 allFinite_freeProCZCCompletedFoxJacobian
533 (X := X) (F := F) hκ η.toMonoidHom φ ι x y := by
534 exact allFinite_freeProCZCCompletedFoxDerivativeVector_comp_apply
535 (X := X) (Y := Y) (F := F) (F' := F') (H := H)
536 hι hκ η.toMonoidHom η.continuous_toFun φ g y
538/-- The continuous-homomorphism form of the completed pro-\(C\) Fox chain rule in matrix form. -/
539theorem allFinite_freeProCZCCompletedFoxDerivativeVector_comp_matrix_continuousMonoidHom
540 {ι : X → F} {κ : Y → F'}
545 (η : F →ₜ* F') (φ : Y → H) (g : F) :
546 freeProCZCCompletedFoxDerivativeVector
548 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
549 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
551 Matrix.vecMul
552 (freeProCZCCompletedFoxDerivativeVector
554 (ProCGrp.allFinite_property (ProfiniteGrp.of _))
555 (allFinite_freeProCZCCompletedFoxPullbackGenerator
556 (X := X) (F := F) hκ η.toMonoidHom φ ι)
557 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
559 (allFinite_freeProCZCCompletedFoxPullbackGenerator
560 (X := X) (F := F) hκ η.toMonoidHom φ ι)) g)
561 (allFinite_freeProCZCCompletedFoxJacobianMatrix
562 (X := X) (F := F) hκ η.toMonoidHom φ ι) := by
563 exact allFinite_freeProCZCCompletedFoxDerivativeVector_comp_matrix
564 (X := X) (Y := Y) (F := F) (F' := F') (H := H)
565 hι hκ η.toMonoidHom η.continuous_toFun φ g
567end AllFiniteChainRule
569end
571end FoxDifferential