Source: ProCGroups.FoxDifferential.Discrete.Jacobian.ChainRule
1import ProCGroups.FoxDifferential.Discrete.Jacobian.Basic
3/-!
4# Fox differential: discrete — jacobian — chain rule
6The principal declarations in this module are:
8- `relativeFreeGroupFoxHom_comp`
9 The composed derivative \(w \mapsto D(\varphi(w))\) is a crossed differential.
10- `relativeFreeGroupFoxDerivative_comp_apply`
11 The relative Fox derivative of a composite free-group homomorphism satisfies the coordinatewise
12 chain-rule sum.
13- `relativeFreeGroupFoxDerivative_comp`
14 Fox chain rule for homomorphisms between free groups in vector form.
15- `freeGroupHomFoxJacobian_id`
16 The relative Fox Jacobian of the identity homomorphism is the coordinate identity family.
17-/
19namespace FoxDifferential
21noncomputable section
23namespace FoxCalculus
25open scoped BigOperators
27universe u v w z t
29variable {H : Type w} [Group H]
30variable {X : Type u} {Y : Type v}
32/-- The composed derivative \(w \mapsto D(\varphi(w))\) is a crossed differential. -/
33def relativeFreeGroupFoxHom_comp
34 [DecidableEq Y]
35 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
36 DifferentialHom (ψ.comp φ) (Y → GroupRing H) where
37 toFun w := relativeFreeGroupFoxHom (H := H) Y ψ (φ w)
38 map_mul' := by
39 intro u v
40 funext y
41 simp only [scalarCrossedAction_apply, map_mul, ScalarCrossedHom.map_mul,
42 MonoidAlgebra.of_apply, Pi.add_apply, Pi.smul_apply, smul_eq_mul,
43 groupRingScalar, MonoidHom.coe_comp, Function.comp_apply]
44 rfl
46/--
47The relative Fox derivative of a composite free-group homomorphism satisfies the coordinatewise
48chain-rule sum.
49-/
50theorem relativeFreeGroupFoxDerivative_comp_apply
51 [DecidableEq X] [Fintype X] [DecidableEq Y]
52 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
53 (w : FreeGroup X) (y : Y) :
54 relativeFreeGroupFoxDerivative (H := H) Y ψ (φ w) y =
55 ∑ x : X,
56 relativeFreeGroupFoxDerivative (H := H) X (ψ.comp φ) w x *
57 freeGroupHomFoxJacobian (H := H) ψ φ x y := by
58 have h :=
59 crossedHom_comp_relativeFreeGroupFoxDerivative
60 (H := H) (A := Y → GroupRing H) (X := X) (Y := Y)
61 ψ φ (relativeFreeGroupFoxHom (H := H) Y ψ) w
62 have hy := congrFun h y
63 simpa [freeGroupHomFoxJacobian, Finset.sum_apply, Pi.smul_apply, smul_eq_mul] using hy
65/-- Fox chain rule for homomorphisms between free groups in vector form. -/
66theorem relativeFreeGroupFoxDerivative_comp
67 [DecidableEq X] [Fintype X] [DecidableEq Y]
68 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
69 (w : FreeGroup X) :
70 relativeFreeGroupFoxDerivative (H := H) Y ψ (φ w) =
71 fun y : Y =>
72 ∑ x : X,
73 relativeFreeGroupFoxDerivative (H := H) X (ψ.comp φ) w x *
74 freeGroupHomFoxJacobian (H := H) ψ φ x y := by
75 funext y
76 exact relativeFreeGroupFoxDerivative_comp_apply (H := H) ψ φ w y
78/-- The relative Fox Jacobian of the identity homomorphism is the coordinate identity family. -/
79@[simp]
80theorem freeGroupHomFoxJacobian_id
81 [DecidableEq X]
82 (ψ : FreeGroup X →* H) :
83 freeGroupHomFoxJacobian (H := H) ψ (MonoidHom.id (FreeGroup X)) =
84 fun x : X => Pi.single x (1 : GroupRing H) := by
85 funext x y
86 simp only [freeGroupHomFoxJacobian, MonoidHom.id_apply, relativeFreeGroupFoxDerivative_of]
88variable {Z : Type z}
90/--
91An entry of the relative Fox Jacobian of a composite is the group-ring-weighted sum of the
92corresponding Jacobian entries.
93-/
94theorem freeGroupHomFoxJacobian_comp_apply
95 [DecidableEq Y] [Fintype Y] [DecidableEq Z]
96 (ψ : FreeGroup Z →* H)
97 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y)
98 (x : X) (z : Z) :
99 freeGroupHomFoxJacobian (H := H) ψ (φ.comp χ) x z =
100 ∑ y : Y,
101 freeGroupHomFoxJacobian (H := H) (ψ.comp φ) χ x y *
102 freeGroupHomFoxJacobian (H := H) ψ φ y z := by
103 simpa [freeGroupHomFoxJacobian] using
104 relativeFreeGroupFoxDerivative_comp_apply (H := H) ψ φ (χ (FreeGroup.of x)) z
106/--
107The Fox Jacobian chain rule for homomorphisms between free groups is expressed in matrix form.
108-/
109theorem freeGroupHomFoxJacobian_comp
110 [DecidableEq Y] [Fintype Y] [DecidableEq Z]
111 (ψ : FreeGroup Z →* H)
112 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
113 freeGroupHomFoxJacobian (H := H) ψ (φ.comp χ) =
114 fun x z =>
115 ∑ y : Y,
116 freeGroupHomFoxJacobian (H := H) (ψ.comp φ) χ x y *
117 freeGroupHomFoxJacobian (H := H) ψ φ y z := by
118 funext x z
119 exact freeGroupHomFoxJacobian_comp_apply (H := H) ψ φ χ x z
121/-- The relative Fox Jacobian matrix of the identity homomorphism is the identity matrix. -/
122@[simp]
123theorem freeGroupHomFoxJacobianMatrix_id
124 [DecidableEq X]
125 (ψ : FreeGroup X →* H) :
126 freeGroupHomFoxJacobianMatrix (H := H) ψ (MonoidHom.id (FreeGroup X)) =
127 (1 : Matrix X X (GroupRing H)) := by
128 apply Matrix.ext
129 intro x y
130 change freeGroupHomFoxJacobian (H := H) ψ (MonoidHom.id (FreeGroup X)) x y =
131 (1 : Matrix X X (GroupRing H)) x y
132 rw [show
133 freeGroupHomFoxJacobian (H := H) ψ (MonoidHom.id (FreeGroup X)) x y =
134 (Pi.single x (1 : GroupRing H) : X → GroupRing H) y from
135 congrFun (congrFun (freeGroupHomFoxJacobian_id (H := H) ψ) x) y]
136 by_cases hxy : x = y
137 · subst y
138 simp only [Pi.single_eq_same, Matrix.one_apply_eq]
139 · simp only [ne_eq, hxy, not_false_eq_true, Pi.single_eq_of_ne', Matrix.one_apply_ne]
141/-- Fox Jacobian chain rule, packaged as matrix multiplication. -/
142theorem freeGroupHomFoxJacobianMatrix_comp
143 [DecidableEq Y] [Fintype Y] [DecidableEq Z]
144 (ψ : FreeGroup Z →* H)
145 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
146 freeGroupHomFoxJacobianMatrix (H := H) ψ (φ.comp χ) =
147 freeGroupHomFoxJacobianMatrix (H := H) (ψ.comp φ) χ *
148 freeGroupHomFoxJacobianMatrix (H := H) ψ φ := by
149 apply Matrix.ext
150 intro x z
151 simp only [freeGroupHomFoxJacobianMatrix, freeGroupHomFoxJacobian_comp_apply, Matrix.mul_apply]
153/--
154An entry of the absolute Fox Jacobian of a composite is the group-ring-weighted chain-rule sum.
155-/
156theorem freeGroupHomFoxJacobianAbsolute_comp_apply
157 [DecidableEq Y] [Fintype Y] [DecidableEq Z]
158 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y)
159 (x : X) (z : Z) :
160 freeGroupHomFoxJacobianAbsolute (φ.comp χ) x z =
161 ∑ y : Y,
162 groupRingMap φ (freeGroupHomFoxJacobianAbsolute χ x y) *
163 freeGroupHomFoxJacobianAbsolute φ y z := by
164 calc
165 freeGroupHomFoxJacobianAbsolute (φ.comp χ) x z =
166 ∑ y : Y,
167 freeGroupHomFoxJacobian (H := FreeGroup Z) φ χ x y *
168 freeGroupHomFoxJacobianAbsolute φ y z := by
169 simpa [freeGroupHomFoxJacobianAbsolute] using
170 freeGroupHomFoxJacobian_comp_apply
171 (H := FreeGroup Z)
172 (X := X) (Y := Y) (Z := Z)
173 (MonoidHom.id (FreeGroup Z)) φ χ x z
174 _ =
175 ∑ y : Y,
176 groupRingMap φ (freeGroupHomFoxJacobianAbsolute χ x y) *
177 freeGroupHomFoxJacobianAbsolute φ y z := by
178 apply Finset.sum_congr rfl
179 intro y _
180 rw [freeGroupHomFoxJacobian_eq_map_absolute_apply (H := FreeGroup Z) φ χ x y]
182/-- The absolute Fox Jacobian chain rule is expressed in matrix form. -/
183theorem freeGroupHomFoxJacobianAbsoluteMatrix_comp
184 [DecidableEq Y] [Fintype Y] [DecidableEq Z]
185 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
186 freeGroupHomFoxJacobianAbsoluteMatrix (φ.comp χ) =
187 (freeGroupHomFoxJacobianAbsoluteMatrix χ).map (groupRingMap φ) *
188 freeGroupHomFoxJacobianAbsoluteMatrix φ := by
189 apply Matrix.ext
190 intro x z
191 simp only [freeGroupHomFoxJacobianAbsoluteMatrix, freeGroupHomFoxJacobianAbsolute_comp_apply,
192 Matrix.mul_apply, Matrix.map_apply]
195end FoxCalculus
197end
199end FoxDifferential