Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Common.FreeCrossedDifferential
ProCGroups/FoxDifferential/Common/FreeCrossedDifferential/Source

Source: ProCGroups.FoxDifferential.Common.FreeCrossedDifferential

1import ProCGroups.FoxDifferential.Common.CrossedDifferential
2import ProCGroups.FoxDifferential.Common.Jacobian
3import Mathlib.GroupTheory.FreeGroup.Basic
5/-!
6# Fox differential: common — free crossed differential
8The principal declarations in this module are:
10- `freeCrossedHomActionLift`
11 The standard semidirect-product lift producing a free crossed homomorphism for an arbitrary
12 additive action.
13- `freeCrossedHomForAction`
14 The free crossed homomorphism with prescribed generator values for a general additive action.
15 This is the canonical action-level construction; scalar Fox differentials specialize it via
16 `scalarCrossedAction`.
17- `freeCrossedHomActionLift_right`
18 The free-group component of semidirect multiplication.
19- `freeCrossedHomForAction_of`
20 The free crossed homomorphism takes each free generator to its prescribed basis value.
21-/
23namespace FoxDifferential
25noncomputable section
27open scoped BigOperators
29universe u v
31variable {R : Type*} [Semiring R]
32variable {A : Type*} [AddCommGroup A] [Module R A]
33variable {X : Type u}
35section GeneralAction
37variable (action : FreeGroup X →* Multiplicative (AddAut A)) (basisValue : X → A)
39/-- The standard semidirect-product lift producing a free crossed homomorphism for an arbitrary
40additive action. -/
41def freeCrossedHomActionLift :
42 FreeGroup X →* CrossedSemidirectProduct action :=
43 FreeGroup.lift fun x => ⟨Multiplicative.ofAdd (basisValue x), FreeGroup.of x⟩
45/-- The free-group component of semidirect multiplication. -/
46@[simp]
47theorem freeCrossedHomActionLift_right (w : FreeGroup X) :
48 (freeCrossedHomActionLift action basisValue w).right = w := by
49 induction w using FreeGroup.induction_on with
50 | C1 => simp only [freeCrossedHomActionLift, map_one, SemidirectProduct.one_right]
51 | of x => simp only [freeCrossedHomActionLift, FreeGroup.lift_apply_of]
52 | inv_of x hx => simpa using congrArg Inv.inv hx
53 | mul x y hx hy =>
54 simp only [map_mul, SemidirectProduct.mul_right, hx, hy]
56/-- The free crossed homomorphism with prescribed generator values for a general additive
57action. This is the canonical action-level construction; scalar Fox differentials specialize it
58via `scalarCrossedAction`. -/
59def freeCrossedHomForAction : CrossedHom action :=
60 CrossedHom.ofSemidirectMonoidHom
61 (freeCrossedHomActionLift action basisValue)
62 (freeCrossedHomActionLift_right action basisValue)
64/-- The free crossed homomorphism takes each free generator to its prescribed basis value. -/
65@[simp]
66theorem freeCrossedHomForAction_of (x : X) :
67 freeCrossedHomForAction action basisValue (FreeGroup.of x) = basisValue x :=
68 by
69 simp only [freeCrossedHomForAction, CrossedHom.ofSemidirectMonoidHom_apply,
70 freeCrossedHomActionLift,
71 FreeGroup.lift_apply_of, toAdd_ofAdd]
73/-- A crossed homomorphism on a free group is determined by its values on the free generators,
74for an arbitrary additive action. -/
75theorem freeCrossedHomForAction_unique
76 (delta : CrossedHom action)
77 (hbasis : ∀ x : X, delta (FreeGroup.of x) = basisValue x) :
78 delta = freeCrossedHomForAction action basisValue := by
79 apply CrossedHom.ext
80 intro w
81 induction w using FreeGroup.induction_on with
82 | C1 => rw [CrossedHom.map_one, CrossedHom.map_one]
83 | of x => rw [hbasis x, freeCrossedHomForAction_of]
84 | inv_of x hx => rw [CrossedHom.map_inv, CrossedHom.map_inv, hx]
85 | mul u v hu hv => rw [CrossedHom.map_mul, CrossedHom.map_mul, hu, hv]
87/-- General-action crossed homomorphisms on a free group are equivalent to generator-value
88assignments. -/
89def crossedHomForActionEquivGeneratorValues : CrossedHom action ≃ (X → A) where
90 toFun delta x := delta (FreeGroup.of x)
91 invFun values := freeCrossedHomForAction action values
92 left_inv delta := (freeCrossedHomForAction_unique action
93 (fun x => delta (FreeGroup.of x)) delta (by intro x; rfl)).symm
94 right_inv values := by
95 funext x
96 exact freeCrossedHomForAction_of action values x
98end GeneralAction
100variable (coeff : FreeGroup X →* R) (basisValue : X → A)
102/--
103The semidirect lift whose left component is the free crossed differential with prescribed
104generator values.
105-/
106def freeCrossedDifferentialWithCoeffLift :
107 FreeGroup X →* CrossedSemidirectProduct (scalarCrossedAction (A := A) coeff) :=
108 freeCrossedHomActionLift (scalarCrossedAction (A := A) coeff) basisValue
110/-- The free crossed differential with coefficient homomorphism `coeff` and prescribed generator
111values `basisValue`. -/
112def freeCrossedDifferentialWithCoeff (w : FreeGroup X) : A :=
113 Multiplicative.toAdd
114 (freeCrossedDifferentialWithCoeffLift (A := A) coeff basisValue w).left
116/-- The right component of the free crossed-differential lift is the identity on the free group. -/
117@[simp]
118theorem freeCrossedDifferentialWithCoeffLift_right (w : FreeGroup X) :
119 (freeCrossedDifferentialWithCoeffLift (A := A) coeff basisValue w).right = w := by
120 exact freeCrossedHomActionLift_right
121 (scalarCrossedAction (A := A) coeff) basisValue w
123/-- The free crossed differential sends the identity word to zero. -/
124@[simp]
125theorem freeCrossedDifferentialWithCoeff_one :
126 freeCrossedDifferentialWithCoeff (A := A) coeff basisValue 1 = 0 := by
127 change
128 freeCrossedHomForAction (scalarCrossedAction (A := A) coeff) basisValue 1 = 0
129 exact CrossedHom.map_one
130 (freeCrossedHomForAction (scalarCrossedAction (A := A) coeff) basisValue)
132/-- The free crossed differential sends a free generator to its prescribed value. -/
133@[simp]
134theorem freeCrossedDifferentialWithCoeff_of (x : X) :
135 freeCrossedDifferentialWithCoeff (A := A) coeff basisValue (FreeGroup.of x) =
136 basisValue x := by
137 change
138 freeCrossedHomForAction (scalarCrossedAction (A := A) coeff) basisValue
139 (FreeGroup.of x) =
140 basisValue x
141 exact freeCrossedHomForAction_of
142 (scalarCrossedAction (A := A) coeff) basisValue x
144/-- Product rule for the free crossed differential with arbitrary coefficients. -/
145theorem freeCrossedDifferentialWithCoeff_mul (u v : FreeGroup X) :
146 freeCrossedDifferentialWithCoeff (A := A) coeff basisValue (u * v) =
147 freeCrossedDifferentialWithCoeff (A := A) coeff basisValue u +
148 coeff u • freeCrossedDifferentialWithCoeff (A := A) coeff basisValue v := by
149 change
150 freeCrossedHomForAction (scalarCrossedAction (A := A) coeff) basisValue (u * v) =
151 freeCrossedHomForAction (scalarCrossedAction (A := A) coeff) basisValue u +
152 coeff u •
153 freeCrossedHomForAction (scalarCrossedAction (A := A) coeff) basisValue v
154 exact ScalarCrossedHom.map_mul
155 (freeCrossedHomForAction (scalarCrossedAction (A := A) coeff) basisValue) u v
157/-- Inverse rule for the free crossed differential with arbitrary coefficients. -/
158theorem freeCrossedDifferentialWithCoeff_inv (w : FreeGroup X) :
159 freeCrossedDifferentialWithCoeff (A := A) coeff basisValue w⁻¹ =
160 -(coeff w⁻¹ • freeCrossedDifferentialWithCoeff (A := A) coeff basisValue w) := by
161 change
162 freeCrossedHomForAction (scalarCrossedAction (A := A) coeff) basisValue w⁻¹ =
163 -(coeff w⁻¹ •
164 freeCrossedHomForAction (scalarCrossedAction (A := A) coeff) basisValue w)
165 exact ScalarCrossedHom.map_inv
166 (freeCrossedHomForAction (scalarCrossedAction (A := A) coeff) basisValue) w
168/--
169The free crossed differential with coefficient homomorphism \(\mathrm{coeff}\) and prescribed
170generator values \(\mathrm{basisValue}\).
171-/
172def freeCrossedHomWithCoeff : ScalarCrossedHom coeff A :=
173 freeCrossedHomForAction (scalarCrossedAction (A := A) coeff) basisValue
175/-- Evaluating the bundled free crossed homomorphism gives the corresponding free crossed
176differential. -/
177@[simp]
178theorem freeCrossedHomWithCoeff_apply (w : FreeGroup X) :
179 freeCrossedHomWithCoeff (A := A) coeff basisValue w =
180 freeCrossedDifferentialWithCoeff (A := A) coeff basisValue w :=
181 rfl
183/-- The free crossed differential sends a free generator to its prescribed value. -/
184@[simp]
185theorem freeCrossedHomWithCoeff_of (x : X) :
186 freeCrossedHomWithCoeff (A := A) coeff basisValue (FreeGroup.of x) = basisValue x :=
187 freeCrossedDifferentialWithCoeff_of (A := A) coeff basisValue x
189/--
190Uniqueness of crossed differentials on a free group from their generator values, for an
191arbitrary coefficient homomorphism.
192-/
193theorem freeCrossedHomWithCoeff_unique
194 (delta : ScalarCrossedHom coeff A)
195 (hbasis : ∀ x : X, delta (FreeGroup.of x) = basisValue x) :
196 delta = freeCrossedHomWithCoeff (A := A) coeff basisValue := by
197 exact freeCrossedHomForAction_unique
198 (scalarCrossedAction (A := A) coeff) basisValue delta hbasis
200/--
201Existence and uniqueness of crossed differentials on a free group from arbitrary generator
202values and an arbitrary coefficient homomorphism.
203-/
204theorem existsUnique_freeCrossedHomWithCoeff :
205 ∃! delta : ScalarCrossedHom coeff A,
206 ∀ x : X, delta (FreeGroup.of x) = basisValue x := by
207 refine ⟨freeCrossedHomWithCoeff (A := A) coeff basisValue, ?_, ?_⟩
208 · exact freeCrossedHomWithCoeff_of (A := A) coeff basisValue
209 · intro delta hdelta
210 exact freeCrossedHomWithCoeff_unique (A := A) coeff basisValue delta hdelta
212/--
213Crossed differentials on a free group are equivalent to assignments of values on the free
214generators.
215-/
216def crossedHomEquivGeneratorValues : ScalarCrossedHom coeff A ≃ (X → A) where
217 toFun delta := fun x => delta (FreeGroup.of x)
218 invFun basisValue := freeCrossedHomWithCoeff (A := A) coeff basisValue
219 left_inv delta := by
220 exact (freeCrossedHomWithCoeff_unique (A := A) coeff
221 (fun x => delta (FreeGroup.of x)) delta (by intro x; rfl)).symm
222 right_inv basisValue := by
223 funext x
224 exact freeCrossedHomWithCoeff_of (A := A) coeff basisValue x
226section Coordinates
228variable {S : Type*} [Ring S]
229variable {B : Type*} [AddCommGroup B] [Module S B]
230variable {Y : Type v}
231variable [DecidableEq X]
233/-- The universal Fox-coordinate crossed differential for an arbitrary coefficient homomorphism
234to a ring. -/
235def freeCrossedDifferentialWithCoeffCoordinates
236 (coeff : FreeGroup X →* S) (w : FreeGroup X) : X → S :=
237 freeCrossedDifferentialWithCoeff
238 (A := X → S) coeff (fun x => Pi.single x (1 : S)) w
240/--
241The universal Fox-coordinate crossed differential for an arbitrary coefficient homomorphism to a
242ring.
243-/
244def freeCrossedHomWithCoeffCoordinates
245 (coeff : FreeGroup X →* S) : ScalarCrossedHom coeff (X → S) :=
246 freeCrossedHomWithCoeff
247 (A := X → S) coeff (fun x => Pi.single x (1 : S))
249/-- Evaluating the bundled coordinate crossed homomorphism gives the unbundled coordinate
250differential. -/
251@[simp]
252theorem freeCrossedHomWithCoeffCoordinates_apply
253 (coeff : FreeGroup X →* S) (w : FreeGroup X) :
254 freeCrossedHomWithCoeffCoordinates (X := X) coeff w =
255 freeCrossedDifferentialWithCoeffCoordinates (X := X) coeff w :=
256 rfl
258/-- The coordinate crossed differential sends the identity word to zero. -/
259@[simp]
260theorem freeCrossedDifferentialWithCoeffCoordinates_one
261 (coeff : FreeGroup X →* S) :
262 freeCrossedDifferentialWithCoeffCoordinates (X := X) coeff (1 : FreeGroup X) = 0 := by
263 simp only [freeCrossedDifferentialWithCoeffCoordinates, freeCrossedDifferentialWithCoeff_one]
265/-- The coordinate crossed differential sends a generator to the standard coordinate vector. -/
266@[simp]
267theorem freeCrossedDifferentialWithCoeffCoordinates_of
268 (coeff : FreeGroup X →* S) (x : X) :
269 freeCrossedDifferentialWithCoeffCoordinates (X := X) coeff (FreeGroup.of x) =
270 Pi.single x (1 : S) := by
271 simp only [freeCrossedDifferentialWithCoeffCoordinates, freeCrossedDifferentialWithCoeff_of]
273/-- The finite linear map evaluating a coordinate vector on prescribed generator values. -/
274def freeCrossedDifferentialWithCoeffExpansionLinearMap
275 [Fintype X] (basisValue : X → B) : (X → S) →ₗ[S] B where
276 toFun v := ∑ x : X, v x • basisValue x
277 map_add' v w := by
278 simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
279 map_smul' a v := by
280 simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, Finset.smul_sum, smul_smul]
282omit [DecidableEq X] in
283/-- The coefficient-expansion linear map evaluates `v` as `∑ x, v x • basisValue x`. -/
284@[simp]
285theorem freeCrossedDifferentialWithCoeffExpansionLinearMap_apply
286 [Fintype X] (basisValue : X → B) (v : X → S) :
287 freeCrossedDifferentialWithCoeffExpansionLinearMap (X := X) basisValue v =
288 ∑ x : X, v x • basisValue x :=
289 rfl
291/-- The expansion linear map sends a standard coordinate vector to the corresponding value. -/
292@[simp]
293theorem freeCrossedDifferentialWithCoeffExpansionLinearMap_single
294 [Fintype X] (basisValue : X → B) (x : X) :
295 freeCrossedDifferentialWithCoeffExpansionLinearMap (X := X) basisValue
296 (Pi.single x (1 : S)) =
297 basisValue x := by
298 rw [freeCrossedDifferentialWithCoeffExpansionLinearMap_apply]
299 rw [Finset.sum_eq_single x]
300 · simp only [Pi.single_eq_same, one_smul]
301 · intro y _ hy
302 simp only [Pi.single_eq_of_ne hy, zero_smul]
303 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_smul, IsEmpty.forall_iff]
305/-- The Fox-coordinate expansion determined by arbitrary coefficient coordinates. -/
306def freeCrossedDifferentialWithCoeffExpansion
307 [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B)
308 (w : FreeGroup X) : B :=
309 freeCrossedDifferentialWithCoeffExpansionLinearMap (X := X) basisValue
310 (freeCrossedDifferentialWithCoeffCoordinates (X := X) coeff w)
312/-- Arbitrary coefficient coordinates determine the Fox-coordinate expansion. -/
313def freeCrossedHomWithCoeffExpansion
314 [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B) :
315 ScalarCrossedHom coeff B :=
316 ScalarCrossedHom.mapLinear
317 (freeCrossedHomWithCoeffCoordinates (X := X) coeff)
318 (freeCrossedDifferentialWithCoeffExpansionLinearMap (X := X) basisValue)
320/-- Evaluating the bundled coordinate expansion gives the corresponding unbundled Fox
321expansion. -/
322@[simp]
323theorem freeCrossedHomWithCoeffExpansion_apply
324 [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B) (w : FreeGroup X) :
325 freeCrossedHomWithCoeffExpansion (X := X) coeff basisValue w =
326 freeCrossedDifferentialWithCoeffExpansion (X := X) coeff basisValue w :=
327 rfl
329/-- The coefficient-coordinate expansion sends each generator to its prescribed value. -/
330@[simp]
331theorem freeCrossedDifferentialWithCoeffExpansion_of
332 [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B) (x : X) :
333 freeCrossedDifferentialWithCoeffExpansion (X := X) coeff basisValue (FreeGroup.of x) =
334 basisValue x := by
335 rw [freeCrossedDifferentialWithCoeffExpansion,
336 freeCrossedDifferentialWithCoeffCoordinates_of,
337 freeCrossedDifferentialWithCoeffExpansionLinearMap_single]
339/-- A free crossed differential is its coefficient-coordinate expansion. -/
340theorem freeCrossedDifferentialWithCoeff_eq_expansion
341 [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B) (w : FreeGroup X) :
342 freeCrossedDifferentialWithCoeff (A := B) coeff basisValue w =
343 freeCrossedDifferentialWithCoeffExpansion (X := X) coeff basisValue w := by
344 have h := freeCrossedHomWithCoeff_unique
345 (A := B) coeff basisValue
346 (freeCrossedHomWithCoeffExpansion (X := X) coeff basisValue)
347 (freeCrossedDifferentialWithCoeffExpansion_of (X := X) coeff basisValue)
348 exact congrArg (fun d : ScalarCrossedHom coeff B => d w) h.symm
350/--
351Abstract Fox chain rule: composing a crossed differential with a free-group homomorphism is the
352coordinate expansion using the pulled-back coefficient homomorphism.
353-/
354theorem freeCrossedHomWithCoeff_comp_expansion
355 [Fintype X]
356 (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
357 (delta : ScalarCrossedHom coeff B) (w : FreeGroup X) :
358 delta (φ w) =
359 freeCrossedDifferentialWithCoeffExpansion
360 (X := X) (coeff.comp φ) (fun x : X => delta (φ (FreeGroup.of x))) w := by
361 let pulled : ScalarCrossedHom (coeff.comp φ) B :=
362 ScalarCrossedHom.compMonoidHom delta φ
363 have hunique :
364 pulled =
365 freeCrossedHomWithCoeff
366 (A := B) (coeff.comp φ) (fun x : X => delta (φ (FreeGroup.of x))) :=
367 freeCrossedHomWithCoeff_unique
368 (A := B) (coeff.comp φ) (fun x : X => delta (φ (FreeGroup.of x)))
369 pulled (by intro x; rfl)
370 calc
371 delta (φ w) = pulled w := rfl
372 _ =
373 freeCrossedDifferentialWithCoeff
374 (A := B) (coeff.comp φ) (fun x : X => delta (φ (FreeGroup.of x))) w := by
375 exact congrArg (fun d : ScalarCrossedHom (coeff.comp φ) B => d w) hunique
376 _ =
377 freeCrossedDifferentialWithCoeffExpansion
378 (X := X) (coeff.comp φ) (fun x : X => delta (φ (FreeGroup.of x))) w := by
379 exact freeCrossedDifferentialWithCoeff_eq_expansion
380 (X := X) (B := B) (coeff.comp φ)
381 (fun x : X => delta (φ (FreeGroup.of x))) w
383omit [DecidableEq X] in
384/-- The abstract Fox-Jacobian of a homomorphism of free sources, with coefficients in S. -/
385def freeCrossedDifferentialWithCoeffJacobian
386 [DecidableEq Y] (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) :
387 X → Y → S :=
388 fun x => freeCrossedDifferentialWithCoeffCoordinates (X := Y) coeff (φ (FreeGroup.of x))
390omit [DecidableEq X] in
391/-- The abstract Fox-Jacobian of a free-source homomorphism as a matrix. -/
392def freeCrossedDifferentialWithCoeffJacobianMatrix
393 [DecidableEq Y] (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) :
394 Matrix X Y S :=
395 foxJacobianMatrix (freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ)
397omit [DecidableEq X] in
398/-- The abstract Fox-Jacobian matrix entry is the corresponding Fox-Jacobian component. -/
399@[simp]
400theorem freeCrossedDifferentialWithCoeffJacobianMatrix_apply
401 [DecidableEq Y] (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
402 (x : X) (y : Y) :
403 freeCrossedDifferentialWithCoeffJacobianMatrix (X := X) coeff φ x y =
404 freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ x y :=
405 rfl
407omit [DecidableEq X] in
408/--
409The abstract Fox-Jacobian determines a finite linear map between the corresponding free
410coefficient modules.
411-/
412def freeCrossedDifferentialWithCoeffJacobianLinearMap
413 [Fintype X] [DecidableEq Y]
414 (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) :
415 (X → S) →ₗ[S] (Y → S) :=
416 foxJacobianLinearMap (freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ)
418omit [DecidableEq X] in
419/--
420Evaluation of the linear map associated with the abstract Fox-Jacobian is computed by the
421corresponding matrix coefficient formula.
422-/
423@[simp]
424theorem freeCrossedDifferentialWithCoeffJacobianLinearMap_apply
425 [Fintype X] [DecidableEq Y]
426 (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
427 (v : X → S) (y : Y) :
428 freeCrossedDifferentialWithCoeffJacobianLinearMap (X := X) coeff φ v y =
429 ∑ x : X, v x * freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ x y :=
430 rfl
432/-- The abstract Fox-Jacobian linear map sends a source basis vector to the corresponding row. -/
433@[simp]
434theorem freeCrossedDifferentialWithCoeffJacobianLinearMap_single
435 [Fintype X] [DecidableEq Y]
436 (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) (x : X) :
437 freeCrossedDifferentialWithCoeffJacobianLinearMap (X := X) coeff φ
438 (Pi.single x (1 : S)) =
439 freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ x := by
440 exact foxJacobianLinearMap_single
441 (freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ) x
443omit [DecidableEq X] in
444/-- The abstract Fox-Jacobian linear map is row-vector multiplication by its matrix. -/
445theorem freeCrossedDifferentialWithCoeffJacobianLinearMap_eq_vecMul
446 [Fintype X] [DecidableEq Y]
447 (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) (v : X → S) :
448 freeCrossedDifferentialWithCoeffJacobianLinearMap (X := X) coeff φ v =
449 Matrix.vecMul v
450 (freeCrossedDifferentialWithCoeffJacobianMatrix (X := X) coeff φ) := by
451 exact foxJacobianLinearMap_eq_vecMul
452 (freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ) v
454/-- The abstract Fox-Jacobian of the identity homomorphism is the identity family. -/
455@[simp]
456theorem freeCrossedDifferentialWithCoeffJacobian_id (coeff : FreeGroup X →* S) :
457 freeCrossedDifferentialWithCoeffJacobian
458 (X := X) (Y := X) coeff (MonoidHom.id (FreeGroup X)) =
459 foxJacobianId (R := S) (X := X) := by
460 funext x y
461 simp only [freeCrossedDifferentialWithCoeffJacobian, MonoidHom.id_apply,
462 freeCrossedDifferentialWithCoeffCoordinates_of, foxJacobianId]
464/-- The abstract Fox-Jacobian matrix of the identity homomorphism is the identity matrix. -/
465@[simp]
466theorem freeCrossedDifferentialWithCoeffJacobianMatrix_id (coeff : FreeGroup X →* S) :
467 freeCrossedDifferentialWithCoeffJacobianMatrix
468 (X := X) (Y := X) coeff (MonoidHom.id (FreeGroup X)) =
469 (1 : Matrix X X S) := by
470 rw [freeCrossedDifferentialWithCoeffJacobianMatrix,
471 freeCrossedDifferentialWithCoeffJacobian_id]
472 simp only [foxJacobianMatrix_id]
474/-- The abstract Fox-Jacobian linear map of the identity homomorphism is the identity. -/
475@[simp]
476theorem freeCrossedDifferentialWithCoeffJacobianLinearMap_id
477 [Fintype X] (coeff : FreeGroup X →* S) :
478 freeCrossedDifferentialWithCoeffJacobianLinearMap
479 (X := X) (Y := X) coeff (MonoidHom.id (FreeGroup X)) =
480 (LinearMap.id : (X → S) →ₗ[S] (X → S)) := by
481 rw [freeCrossedDifferentialWithCoeffJacobianLinearMap,
482 freeCrossedDifferentialWithCoeffJacobian_id]
483 simp only [foxJacobianLinearMap_id]
485/-- Abstract Fox chain rule for coordinate vectors, written as a Jacobian linear-map identity. -/
486theorem freeCrossedDifferentialWithCoeffCoordinates_comp_linearMap
487 [Fintype X] [DecidableEq Y]
488 (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
489 (w : FreeGroup X) :
490 freeCrossedDifferentialWithCoeffCoordinates (X := Y) coeff (φ w) =
491 freeCrossedDifferentialWithCoeffJacobianLinearMap (X := X) coeff φ
492 (freeCrossedDifferentialWithCoeffCoordinates (X := X) (coeff.comp φ) w) := by
493 have h :=
494 freeCrossedHomWithCoeff_comp_expansion
495 (X := X) (Y := Y) (B := Y → S) coeff φ
496 (freeCrossedHomWithCoeffCoordinates (X := Y) coeff) w
497 calc
498 freeCrossedDifferentialWithCoeffCoordinates (X := Y) coeff (φ w) =
499 freeCrossedDifferentialWithCoeffExpansion
500 (X := X) (coeff.comp φ)
501 (fun x : X =>
502 freeCrossedDifferentialWithCoeffCoordinates (X := Y) coeff
503 (φ (FreeGroup.of x))) w := h
504 _ =
505 freeCrossedDifferentialWithCoeffJacobianLinearMap (X := X) coeff φ
506 (freeCrossedDifferentialWithCoeffCoordinates (X := X) (coeff.comp φ) w) := by
507 funext y
508 simp only [freeCrossedDifferentialWithCoeffExpansion,
509 freeCrossedDifferentialWithCoeffExpansionLinearMap,
510 LinearMap.coe_mk, AddHom.coe_mk, Finset.sum_apply, Pi.smul_apply, smul_eq_mul,
511 freeCrossedDifferentialWithCoeffJacobianLinearMap, foxJacobianLinearMap_apply,
512 freeCrossedDifferentialWithCoeffJacobian]
514/--
515Component form of the abstract Fox chain rule: the pushed-forward coordinate is the sum over
516source coordinates weighted by the Fox-Jacobian.
517-/
518theorem freeCrossedDifferentialWithCoeffCoordinates_comp_apply
519 [Fintype X] [DecidableEq Y]
520 (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
521 (w : FreeGroup X) (y : Y) :
522 freeCrossedDifferentialWithCoeffCoordinates (X := Y) coeff (φ w) y =
523 ∑ x : X,
524 freeCrossedDifferentialWithCoeffCoordinates (X := X) (coeff.comp φ) w x *
525 freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ x y := by
526 exact congrFun
527 (freeCrossedDifferentialWithCoeffCoordinates_comp_linearMap
528 (X := X) (Y := Y) coeff φ w) y
530/-- Abstract Fox chain rule for coordinate vectors, written as matrix multiplication. -/
531theorem freeCrossedDifferentialWithCoeffCoordinates_comp_matrix
532 [Fintype X] [DecidableEq Y]
533 (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
534 (w : FreeGroup X) :
535 freeCrossedDifferentialWithCoeffCoordinates (X := Y) coeff (φ w) =
536 Matrix.vecMul
537 (freeCrossedDifferentialWithCoeffCoordinates (X := X) (coeff.comp φ) w)
538 (freeCrossedDifferentialWithCoeffJacobianMatrix (X := X) coeff φ) := by
539 rw [freeCrossedDifferentialWithCoeffCoordinates_comp_linearMap]
540 exact freeCrossedDifferentialWithCoeffJacobianLinearMap_eq_vecMul
541 (X := X) coeff φ
542 (freeCrossedDifferentialWithCoeffCoordinates (X := X) (coeff.comp φ) w)
544omit [DecidableEq X] in
545/--
546Component form of the abstract Fox-Jacobian chain rule for a composite of free-group
547homomorphisms.
548-/
549theorem freeCrossedDifferentialWithCoeffJacobian_comp_apply
550 {Z : Type*} [Fintype Y] [DecidableEq Y] [DecidableEq Z]
551 (coeff : FreeGroup Z →* S)
552 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y)
553 (x : X) (z : Z) :
554 freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Z) coeff (φ.comp χ) x z =
555 ∑ y : Y,
556 freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Y) (coeff.comp φ) χ x y *
557 freeCrossedDifferentialWithCoeffJacobian (X := Y) (Y := Z) coeff φ y z := by
558 simpa [freeCrossedDifferentialWithCoeffJacobian] using
559 freeCrossedDifferentialWithCoeffCoordinates_comp_apply
560 (X := Y) (Y := Z) coeff φ (χ (FreeGroup.of x)) z
562omit [DecidableEq X] in
563/-- The abstract Fox-Jacobian chain rule is expressed in family form. -/
564theorem freeCrossedDifferentialWithCoeffJacobian_comp
565 {Z : Type*} [Fintype Y] [DecidableEq Y] [DecidableEq Z]
566 (coeff : FreeGroup Z →* S)
567 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
568 freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Z) coeff (φ.comp χ) =
569 fun x z =>
570 ∑ y : Y,
571 freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Y) (coeff.comp φ) χ x y *
572 freeCrossedDifferentialWithCoeffJacobian (X := Y) (Y := Z) coeff φ y z := by
573 funext x z
574 exact freeCrossedDifferentialWithCoeffJacobian_comp_apply
575 (X := X) (Y := Y) coeff φ χ x z
577omit [DecidableEq X] in
578/-- The abstract Fox-Jacobian chain rule is expressed in linear-map form. -/
579theorem freeCrossedDifferentialWithCoeffJacobianLinearMap_comp
580 {Z : Type*} [Fintype X] [Fintype Y] [DecidableEq Y] [DecidableEq Z]
581 (coeff : FreeGroup Z →* S)
582 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
583 (freeCrossedDifferentialWithCoeffJacobianLinearMap (X := Y) (Y := Z) coeff φ).comp
584 (freeCrossedDifferentialWithCoeffJacobianLinearMap
585 (X := X) (Y := Y) (coeff.comp φ) χ) =
586 freeCrossedDifferentialWithCoeffJacobianLinearMap
587 (X := X) (Y := Z) coeff (φ.comp χ) := by
588 change
589 (foxJacobianLinearMap
590 (freeCrossedDifferentialWithCoeffJacobian (X := Y) (Y := Z) coeff φ)).comp
591 (foxJacobianLinearMap
592 (freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Y) (coeff.comp φ) χ)) =
593 foxJacobianLinearMap
594 (freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Z) coeff (φ.comp χ))
595 rw [foxJacobianLinearMap_comp]
596 congr
597 funext x z
598 exact (freeCrossedDifferentialWithCoeffJacobian_comp_apply
599 (X := X) (Y := Y) coeff φ χ x z).symm
601omit [DecidableEq X] in
602/-- The abstract Fox-Jacobian chain rule is expressed in matrix form. -/
603theorem freeCrossedDifferentialWithCoeffJacobianMatrix_comp
604 {Z : Type*} [Fintype Y] [DecidableEq Y] [DecidableEq Z]
605 (coeff : FreeGroup Z →* S)
606 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
607 freeCrossedDifferentialWithCoeffJacobianMatrix
608 (X := X) (Y := Z) coeff (φ.comp χ) =
609 freeCrossedDifferentialWithCoeffJacobianMatrix
610 (X := X) (Y := Y) (coeff.comp φ) χ *
611 freeCrossedDifferentialWithCoeffJacobianMatrix
612 (X := Y) (Y := Z) coeff φ := by
613 apply Matrix.ext
614 intro x z
615 simp only [freeCrossedDifferentialWithCoeffJacobianMatrix, foxJacobianMatrix_apply,
616 freeCrossedDifferentialWithCoeffJacobian_comp_apply, Matrix.mul_apply]
618end Coordinates
620end
622end FoxDifferential