Source: ProCGroups.FoxDifferential.Completed.Continuous.ChainRule.Iterated
1import ProCGroups.FoxDifferential.Completed.Continuous.ChainRule.Basic
3/-!
4# Fox differential: completed — continuous — chain rule — iterated
6The principal declarations in this module are:
8- `allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator`
9 The pulled-back target generator on the middle free source in a two-step source chain.
10- `allFinite_freeProCZCCompletedFoxFirstPullbackGenerator`
11 The pulled-back target generator on the first free source in a two-step source chain.
12- `allFinite_freeProCZCCompletedFoxJacobianLinearMap_comp_comp`
13 Completed Fox-Jacobian functoriality for two composable continuous free pro-\(C\) source maps, as
14 a composition of finite linear maps.
15- `allFinite_freeProCZCCompletedFoxJacobianMatrix_comp_comp`
16 Completed Fox-Jacobian functoriality for two composable continuous free pro-\(C\) source maps, as
17 a matrix product.
18-/
20namespace FoxDifferential
22noncomputable section
24open scoped BigOperators
26universe u
28section AllFiniteIteratedChainRule
30variable {X Y Z F F' F'' H : Type u}
31variable [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
32variable [Fintype Y] [DecidableEq Y] [TopologicalSpace Y] [DiscreteTopology Y]
33variable [DecidableEq Z] [TopologicalSpace Z] [DiscreteTopology Z]
34variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
35variable [Group F'] [TopologicalSpace F'] [IsTopologicalGroup F']
36variable [Group F''] [TopologicalSpace F''] [IsTopologicalGroup F'']
37variable [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
38variable [CompactSpace F'] [T2Space F'] [TotallyDisconnectedSpace F']
39variable [CompactSpace F''] [T2Space F''] [TotallyDisconnectedSpace F'']
40variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
41variable [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
43/-- The pulled-back target generator on the middle free source in a two-step source chain. -/
44abbrev allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
45 {mu : Z → F''}
47 (C := ProCGroups.FiniteGroupClass.allFinite) mu)
48 (θ : F' →* F'') (φ : Z → H) (κ : Y → F') : Y → H :=
49 allFinite_freeProCZCCompletedFoxPullbackGenerator
50 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ
52/-- The pulled-back target generator on the first free source in a two-step source chain. -/
53abbrev allFinite_freeProCZCCompletedFoxFirstPullbackGenerator
54 {κ : Y → F'} {mu : Z → F''}
56 (C := ProCGroups.FiniteGroupClass.allFinite) κ)
58 (C := ProCGroups.FiniteGroupClass.allFinite) mu)
59 (η : F →* F') (θ : F' →* F'') (φ : Z → H) (ι : X → F) : X → H :=
60 allFinite_freeProCZCCompletedFoxPullbackGenerator
61 (X := X) (Y := Y) (F := F) (F' := F') hκ η
62 (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
63 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
64 ι
66omit [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
67 [TopologicalSpace F] [IsTopologicalGroup F] in
68/--
69Completed Fox-Jacobian functoriality for two composable continuous free pro-\(C\) source maps,
70as a composition of finite linear maps.
71-/
72theorem allFinite_freeProCZCCompletedFoxJacobianLinearMap_comp_comp
73 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
75 (C := ProCGroups.FiniteGroupClass.allFinite) κ)
77 (C := ProCGroups.FiniteGroupClass.allFinite) mu)
78 (η : F →* F') (θ : F' →* F'') (hθ_continuous : Continuous θ) (φ : Z → H) :
79 allFinite_freeProCZCCompletedFoxJacobianLinearMap
80 (X := X) (Y := Z) (F := F) (F' := F'') hmu (θ.comp η) φ ι =
81 (allFinite_freeProCZCCompletedFoxJacobianLinearMap
82 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ).comp
83 (allFinite_freeProCZCCompletedFoxJacobianLinearMap
84 (X := X) (Y := Y) (F := F) (F' := F') hκ η
85 (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
86 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
87 ι) := by
88 classical
89 apply linearMap_ext_pi_single
90 intro x
91 have hchain := allFinite_freeProCZCCompletedFoxDerivativeVector_comp
92 (X := Y) (Y := Z) (F := F') (F' := F'') (H := H)
93 hκ hmu θ hθ_continuous φ (η (ι x))
94 simpa [LinearMap.comp_apply,
95 allFinite_freeProCZCCompletedFoxJacobianLinearMap,
96 allFinite_freeProCZCCompletedFoxJacobian,
97 allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator] using hchain
99omit [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
100 [TopologicalSpace F] [IsTopologicalGroup F] in
101/--
102Completed Fox-Jacobian functoriality for two composable continuous free pro-\(C\) source maps,
103as a matrix product.
104-/
105theorem allFinite_freeProCZCCompletedFoxJacobianMatrix_comp_comp
106 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
108 (C := ProCGroups.FiniteGroupClass.allFinite) κ)
110 (C := ProCGroups.FiniteGroupClass.allFinite) mu)
111 (η : F →* F') (θ : F' →* F'') (hθ_continuous : Continuous θ) (φ : Z → H) :
112 allFinite_freeProCZCCompletedFoxJacobianMatrix
113 (X := X) (Y := Z) (F := F) (F' := F'') hmu (θ.comp η) φ ι =
114 allFinite_freeProCZCCompletedFoxJacobianMatrix
115 (X := X) (Y := Y) (F := F) (F' := F') hκ η
116 (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
117 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
118 ι *
119 allFinite_freeProCZCCompletedFoxJacobianMatrix
120 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ := by
121 apply Matrix.ext
122 intro x z
123 have h := congrFun
124 (allFinite_freeProCZCCompletedFoxDerivativeVector_comp
125 (X := Y) (Y := Z) (F := F') (F' := F'') (H := H)
126 hκ hmu θ hθ_continuous φ (η (ι x))) z
127 simpa [Matrix.mul_apply,
128 allFinite_freeProCZCCompletedFoxJacobianMatrix,
129 allFinite_freeProCZCCompletedFoxJacobian,
130 allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator] using h
132/-- Three-term completed pro-\(C\) Fox chain rule in vector form. -/
133theorem allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp
134 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
136 (C := ProCGroups.FiniteGroupClass.allFinite) ι)
138 (C := ProCGroups.FiniteGroupClass.allFinite) κ)
140 (C := ProCGroups.FiniteGroupClass.allFinite) mu)
141 (η : F →* F') (hη_continuous : Continuous η)
142 (θ : F' →* F'') (hθ_continuous : Continuous θ) (φ : Z → H) (g : F) :
143 freeProCZCCompletedFoxDerivativeVector
144 (C := ProCGroups.FiniteGroupClass.allFinite) hmu
145 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
146 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
147 ProCGroups.FiniteGroupClass.allFinite) Z H φ) (θ (η g)) =
148 allFinite_freeProCZCCompletedFoxJacobianLinearMap
149 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ
150 (allFinite_freeProCZCCompletedFoxJacobianLinearMap
151 (X := X) (Y := Y) (F := F) (F' := F') hκ η
152 (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
153 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
154 ι
155 (freeProCZCCompletedFoxDerivativeVector
156 (C := ProCGroups.FiniteGroupClass.allFinite) hι
157 (ProCGrp.allFinite_property (ProfiniteGrp.of _))
158 (allFinite_freeProCZCCompletedFoxFirstPullbackGenerator
159 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
160 hκ hmu η θ φ ι)
161 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
163 (allFinite_freeProCZCCompletedFoxFirstPullbackGenerator
164 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
165 hκ hmu η θ φ ι)) g)) := by
166 calc
167 freeProCZCCompletedFoxDerivativeVector
168 (C := ProCGroups.FiniteGroupClass.allFinite) hmu
169 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
170 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
171 ProCGroups.FiniteGroupClass.allFinite) Z H φ) (θ (η g)) =
172 allFinite_freeProCZCCompletedFoxJacobianLinearMap
173 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ
174 (freeProCZCCompletedFoxDerivativeVector
175 (C := ProCGroups.FiniteGroupClass.allFinite) hκ
176 (ProCGrp.allFinite_property (ProfiniteGrp.of _))
177 (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
178 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
179 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
181 (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
182 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)) (η g)) := by
183 exact allFinite_freeProCZCCompletedFoxDerivativeVector_comp
184 (X := Y) (Y := Z) (F := F') (F' := F'') (H := H)
185 hκ hmu θ hθ_continuous φ (η g)
186 _ =
187 allFinite_freeProCZCCompletedFoxJacobianLinearMap
188 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ
189 (allFinite_freeProCZCCompletedFoxJacobianLinearMap
190 (X := X) (Y := Y) (F := F) (F' := F') hκ η
191 (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
192 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
193 ι
194 (freeProCZCCompletedFoxDerivativeVector
195 (C := ProCGroups.FiniteGroupClass.allFinite) hι
196 (ProCGrp.allFinite_property (ProfiniteGrp.of _))
197 (allFinite_freeProCZCCompletedFoxFirstPullbackGenerator
198 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
199 hκ hmu η θ φ ι)
200 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
202 (allFinite_freeProCZCCompletedFoxFirstPullbackGenerator
203 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
204 hκ hmu η θ φ ι)) g)) := by
205 exact congrArg
206 (allFinite_freeProCZCCompletedFoxJacobianLinearMap
207 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ)
208 (allFinite_freeProCZCCompletedFoxDerivativeVector_comp
209 (X := X) (Y := Y) (F := F) (F' := F') (H := H)
210 hι hκ η hη_continuous
211 (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
212 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ) g)
214/-- The three-term completed pro-\(C\) Fox chain rule in matrix form. -/
215theorem allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_matrix
216 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
218 (C := ProCGroups.FiniteGroupClass.allFinite) ι)
220 (C := ProCGroups.FiniteGroupClass.allFinite) κ)
222 (C := ProCGroups.FiniteGroupClass.allFinite) mu)
223 (η : F →* F') (hη_continuous : Continuous η)
224 (θ : F' →* F'') (hθ_continuous : Continuous θ) (φ : Z → H) (g : F) :
225 freeProCZCCompletedFoxDerivativeVector
226 (C := ProCGroups.FiniteGroupClass.allFinite) hmu
227 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
228 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
229 ProCGroups.FiniteGroupClass.allFinite) Z H φ) (θ (η g)) =
230 Matrix.vecMul
231 (Matrix.vecMul
232 (freeProCZCCompletedFoxDerivativeVector
233 (C := ProCGroups.FiniteGroupClass.allFinite) hι
234 (ProCGrp.allFinite_property (ProfiniteGrp.of _))
235 (allFinite_freeProCZCCompletedFoxFirstPullbackGenerator
236 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
237 hκ hmu η θ φ ι)
238 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
240 (allFinite_freeProCZCCompletedFoxFirstPullbackGenerator
241 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
242 hκ hmu η θ φ ι)) g)
243 (allFinite_freeProCZCCompletedFoxJacobianMatrix
244 (X := X) (Y := Y) (F := F) (F' := F') hκ η
245 (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
246 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
247 ι))
248 (allFinite_freeProCZCCompletedFoxJacobianMatrix
249 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ) := by
250 rw [allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp
251 (X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
252 hι hκ hmu η hη_continuous θ hθ_continuous φ g]
253 rw [allFinite_freeProCZCCompletedFoxJacobianLinearMap_eq_vecMul]
254 rw [allFinite_freeProCZCCompletedFoxJacobianLinearMap_eq_vecMul]
256/-- Three-term completed pro-\(C\) Fox chain rule in component form. -/
257theorem allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_apply
258 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
260 (C := ProCGroups.FiniteGroupClass.allFinite) ι)
262 (C := ProCGroups.FiniteGroupClass.allFinite) κ)
264 (C := ProCGroups.FiniteGroupClass.allFinite) mu)
265 (η : F →* F') (hη_continuous : Continuous η)
266 (θ : F' →* F'') (hθ_continuous : Continuous θ) (φ : Z → H) (g : F) (z : Z) :
267 freeProCZCCompletedFoxDerivativeVector
268 (C := ProCGroups.FiniteGroupClass.allFinite) hmu
269 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
270 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
271 ProCGroups.FiniteGroupClass.allFinite) Z H φ) (θ (η g)) z =
272 ∑ y : Y,
273 (∑ x : X,
274 freeProCZCCompletedFoxDerivativeVector
275 (C := ProCGroups.FiniteGroupClass.allFinite) hι
276 (ProCGrp.allFinite_property (ProfiniteGrp.of _))
277 (allFinite_freeProCZCCompletedFoxFirstPullbackGenerator
278 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
279 hκ hmu η θ φ ι)
280 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
282 (allFinite_freeProCZCCompletedFoxFirstPullbackGenerator
283 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
284 hκ hmu η θ φ ι)) g x *
285 allFinite_freeProCZCCompletedFoxJacobian
286 (X := X) (Y := Y) (F := F) (F' := F') hκ η
287 (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
288 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
289 ι x y) *
290 allFinite_freeProCZCCompletedFoxJacobian
291 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ y z := by
292 have h := congrFun
293 (allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_matrix
294 (X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
295 hι hκ hmu η hη_continuous θ hθ_continuous φ g) z
296 simpa [Matrix.vecMul, dotProduct,
297 allFinite_freeProCZCCompletedFoxJacobianMatrix] using h
299omit [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
300 [IsTopologicalGroup F] [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F] in
301/--
302Continuous-homomorphism form of completed Fox-Jacobian functoriality, as a composition of finite
303linear maps.
304-/
305theorem allFinite_freeProCZCCompletedFoxJacobianLinearMap_comp_comp_continuousMonoidHom
306 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
308 (C := ProCGroups.FiniteGroupClass.allFinite) κ)
310 (C := ProCGroups.FiniteGroupClass.allFinite) mu)
311 (η : F →ₜ* F') (θ : F' →ₜ* F'') (φ : Z → H) :
312 allFinite_freeProCZCCompletedFoxJacobianLinearMap
313 (X := X) (Y := Z) (F := F) (F' := F'') hmu
314 (θ.toMonoidHom.comp η.toMonoidHom) φ ι =
315 (allFinite_freeProCZCCompletedFoxJacobianLinearMap
316 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ.toMonoidHom φ κ).comp
317 (allFinite_freeProCZCCompletedFoxJacobianLinearMap
318 (X := X) (Y := Y) (F := F) (F' := F') hκ η.toMonoidHom
319 (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
320 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ.toMonoidHom φ κ)
321 ι) := by
322 exact allFinite_freeProCZCCompletedFoxJacobianLinearMap_comp_comp
323 (X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
324 hκ hmu η.toMonoidHom θ.toMonoidHom θ.continuous_toFun φ
326omit [Fintype X] [DecidableEq X] [TopologicalSpace X] [DiscreteTopology X]
327 [IsTopologicalGroup F] [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F] in
328/-- Continuous-homomorphism form of completed Fox-Jacobian functoriality, as a matrix product. -/
329theorem allFinite_freeProCZCCompletedFoxJacobianMatrix_comp_comp_continuousMonoidHom
330 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
332 (C := ProCGroups.FiniteGroupClass.allFinite) κ)
334 (C := ProCGroups.FiniteGroupClass.allFinite) mu)
335 (η : F →ₜ* F') (θ : F' →ₜ* F'') (φ : Z → H) :
336 allFinite_freeProCZCCompletedFoxJacobianMatrix
337 (X := X) (Y := Z) (F := F) (F' := F'') hmu
338 (θ.toMonoidHom.comp η.toMonoidHom) φ ι =
339 allFinite_freeProCZCCompletedFoxJacobianMatrix
340 (X := X) (Y := Y) (F := F) (F' := F') hκ η.toMonoidHom
341 (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
342 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ.toMonoidHom φ κ)
343 ι *
344 allFinite_freeProCZCCompletedFoxJacobianMatrix
345 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ.toMonoidHom φ κ := by
346 exact allFinite_freeProCZCCompletedFoxJacobianMatrix_comp_comp
347 (X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
348 hκ hmu η.toMonoidHom θ.toMonoidHom θ.continuous_toFun φ
350/-- Continuous-homomorphism form of the three-term completed pro-\(C\) Fox chain rule. -/
351theorem allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_continuousMonoidHom
352 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
354 (C := ProCGroups.FiniteGroupClass.allFinite) ι)
356 (C := ProCGroups.FiniteGroupClass.allFinite) κ)
358 (C := ProCGroups.FiniteGroupClass.allFinite) mu)
359 (η : F →ₜ* F') (θ : F' →ₜ* F'') (φ : Z → H) (g : F) :
360 freeProCZCCompletedFoxDerivativeVector
361 (C := ProCGroups.FiniteGroupClass.allFinite) hmu
362 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
363 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
364 ProCGroups.FiniteGroupClass.allFinite) Z H φ) (θ (η g)) =
365 allFinite_freeProCZCCompletedFoxJacobianLinearMap
366 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ.toMonoidHom φ κ
367 (allFinite_freeProCZCCompletedFoxJacobianLinearMap
368 (X := X) (Y := Y) (F := F) (F' := F') hκ η.toMonoidHom
369 (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
370 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ.toMonoidHom φ κ)
371 ι
372 (freeProCZCCompletedFoxDerivativeVector
373 (C := ProCGroups.FiniteGroupClass.allFinite) hι
374 (ProCGrp.allFinite_property (ProfiniteGrp.of _))
375 (allFinite_freeProCZCCompletedFoxFirstPullbackGenerator
376 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
377 hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)
378 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
380 (allFinite_freeProCZCCompletedFoxFirstPullbackGenerator
381 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
382 hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)) g)) := by
383 exact allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp
384 (X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
385 hι hκ hmu η.toMonoidHom η.continuous_toFun θ.toMonoidHom θ.continuous_toFun φ g
387/--
388The continuous-homomorphism form of the three-term completed pro-\(C\) Fox chain rule in matrix
389form.
390-/
391theorem allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_matrix_continuousMonoidHom
392 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
394 (C := ProCGroups.FiniteGroupClass.allFinite) ι)
396 (C := ProCGroups.FiniteGroupClass.allFinite) κ)
398 (C := ProCGroups.FiniteGroupClass.allFinite) mu)
399 (η : F →ₜ* F') (θ : F' →ₜ* F'') (φ : Z → H) (g : F) :
400 freeProCZCCompletedFoxDerivativeVector
401 (C := ProCGroups.FiniteGroupClass.allFinite) hmu
402 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
403 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
404 ProCGroups.FiniteGroupClass.allFinite) Z H φ) (θ (η g)) =
405 Matrix.vecMul
406 (Matrix.vecMul
407 (freeProCZCCompletedFoxDerivativeVector
408 (C := ProCGroups.FiniteGroupClass.allFinite) hι
409 (ProCGrp.allFinite_property (ProfiniteGrp.of _))
410 (allFinite_freeProCZCCompletedFoxFirstPullbackGenerator
411 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
412 hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)
413 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
415 (allFinite_freeProCZCCompletedFoxFirstPullbackGenerator
416 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
417 hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)) g)
418 (allFinite_freeProCZCCompletedFoxJacobianMatrix
419 (X := X) (Y := Y) (F := F) (F' := F') hκ η.toMonoidHom
420 (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
421 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ.toMonoidHom φ κ)
422 ι))
423 (allFinite_freeProCZCCompletedFoxJacobianMatrix
424 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ.toMonoidHom φ κ) := by
425 exact allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_matrix
426 (X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
427 hι hκ hmu η.toMonoidHom η.continuous_toFun θ.toMonoidHom θ.continuous_toFun φ g
429/--
430Continuous-homomorphism form of the three-term completed pro-\(C\) Fox chain rule in component
431form.
432-/
433theorem allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_apply_continuousMonoidHom
434 {ι : X → F} {κ : Y → F'} {mu : Z → F''}
436 (C := ProCGroups.FiniteGroupClass.allFinite) ι)
438 (C := ProCGroups.FiniteGroupClass.allFinite) κ)
440 (C := ProCGroups.FiniteGroupClass.allFinite) mu)
441 (η : F →ₜ* F') (θ : F' →ₜ* F'') (φ : Z → H) (g : F) (z : Z) :
442 freeProCZCCompletedFoxDerivativeVector
443 (C := ProCGroups.FiniteGroupClass.allFinite) hmu
444 (ProCGrp.allFinite_property (ProfiniteGrp.of _)) φ
445 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
446 ProCGroups.FiniteGroupClass.allFinite) Z H φ) (θ (η g)) z =
447 ∑ y : Y,
448 (∑ x : X,
449 freeProCZCCompletedFoxDerivativeVector
450 (C := ProCGroups.FiniteGroupClass.allFinite) hι
451 (ProCGrp.allFinite_property (ProfiniteGrp.of _))
452 (allFinite_freeProCZCCompletedFoxFirstPullbackGenerator
453 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
454 hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)
455 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (C :=
457 (allFinite_freeProCZCCompletedFoxFirstPullbackGenerator
458 (X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
459 hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)) g x *
460 allFinite_freeProCZCCompletedFoxJacobian
461 (X := X) (Y := Y) (F := F) (F' := F') hκ η.toMonoidHom
462 (allFinite_freeProCZCCompletedFoxMiddlePullbackGenerator
463 (Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ.toMonoidHom φ κ)
464 ι x y) *
465 allFinite_freeProCZCCompletedFoxJacobian
466 (X := Y) (Y := Z) (F := F') (F' := F'') hmu θ.toMonoidHom φ κ y z := by
467 exact allFinite_freeProCZCCompletedFoxDerivativeVector_comp_comp_apply
468 (X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
469 hι hκ hmu η.toMonoidHom η.continuous_toFun θ.toMonoidHom θ.continuous_toFun φ g z
471end AllFiniteIteratedChainRule
473end
475end FoxDifferential