Source: ProCGroups.FoxDifferential.Discrete.Jacobian.Basic
1import ProCGroups.FoxDifferential.Discrete.Absolute
3/-!
4# Fox differential: discrete — jacobian — basic
6The principal declarations in this module are:
8- `freeGroupHomFoxJacobian`
9 The relative Fox Jacobian of \(\varphi : \mathrm{FreeGroup}(X) \to \mathrm{FreeGroup}(Y)\), with
10 coefficients pushed forward by \(\psi : \mathrm{FreeGroup}(Y) \to H\). The row indexed by \(x :
11 X\) is the relative Fox derivative of the substituted generator \(\varphi(x)\) with respect to the
12 \(Y\)-generators.
13- `freeGroupHomFoxJacobianMatrix`
14 The relative Fox Jacobian, packaged as a matrix.
15- `freeGroupHomFoxJacobianMatrix_apply`
16 Evaluating the bundled relative Fox Jacobian matrix at `(x, y)` returns the corresponding relative
17 Fox derivative.
18- `freeGroupHomFoxJacobian_eq_freeCrossedDifferentialWithCoeffJacobian`
19 The usual relative Fox Jacobian is the coefficient-generic free crossed-differential Jacobian
20 specialized to the group-ring coefficient homomorphism.
21-/
23namespace FoxDifferential
25noncomputable section
27namespace FoxCalculus
29open scoped BigOperators
31universe u v w z t
33variable {H : Type w} [Group H]
34variable {X : Type u} {Y : Type v}
36/--
37The relative Fox Jacobian of \(\varphi : \mathrm{FreeGroup}(X) \to \mathrm{FreeGroup}(Y)\), with
38coefficients pushed forward by \(\psi : \mathrm{FreeGroup}(Y) \to H\). The row indexed by \(x :
39X\) is the relative Fox derivative of the substituted generator \(\varphi(x)\) with respect to
40the \(Y\)-generators.
41-/
42def freeGroupHomFoxJacobian
43 [DecidableEq Y]
44 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
45 X → Y → GroupRing H :=
46 fun x =>
47 relativeFreeGroupFoxDerivative (H := H) Y ψ (φ (FreeGroup.of x))
49/-- The relative Fox Jacobian, packaged as a matrix. -/
50def freeGroupHomFoxJacobianMatrix
51 [DecidableEq Y]
52 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
53 Matrix X Y (GroupRing H) :=
54 freeGroupHomFoxJacobian (H := H) ψ φ
56/--
57Evaluating the bundled relative Fox Jacobian matrix at `(x, y)` returns the corresponding relative
58Fox derivative.
59-/
60@[simp]
61theorem freeGroupHomFoxJacobianMatrix_apply
62 [DecidableEq Y]
63 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
64 (x : X) (y : Y) :
65 freeGroupHomFoxJacobianMatrix (H := H) ψ φ x y =
66 freeGroupHomFoxJacobian (H := H) ψ φ x y :=
67 rfl
69/--
70The usual relative Fox Jacobian is the coefficient-generic free crossed-differential Jacobian
71specialized to the group-ring coefficient homomorphism.
72-/
73theorem freeGroupHomFoxJacobian_eq_freeCrossedDifferentialWithCoeffJacobian
74 [DecidableEq Y]
75 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
76 freeGroupHomFoxJacobian (H := H) ψ φ =
77 freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Y) (groupRingScalar ψ) φ := by
78 funext x y
79 simp only [freeGroupHomFoxJacobian, freeCrossedDifferentialWithCoeffJacobian,
80 freeCrossedDifferentialWithCoeffCoordinates_eq_relativeFreeGroupFoxDerivative]
82/--
83Matrix form of the comparison between the usual relative Fox Jacobian and the
84coefficient-generic free crossed-differential Jacobian.
85-/
86theorem freeGroupHomFoxJacobianMatrix_eq_freeCrossedDifferentialWithCoeffJacobianMatrix
87 [DecidableEq Y]
88 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
89 freeGroupHomFoxJacobianMatrix (H := H) ψ φ =
90 freeCrossedDifferentialWithCoeffJacobianMatrix
91 (X := X) (Y := Y) (groupRingScalar ψ) φ := by
92 apply Matrix.ext
93 intro x y
94 simp only [freeGroupHomFoxJacobianMatrix_apply,
95 freeGroupHomFoxJacobian_eq_freeCrossedDifferentialWithCoeffJacobian,
96 freeCrossedDifferentialWithCoeffJacobianMatrix_apply]
98/-- The absolute Fox Jacobian of a homomorphism between free groups. -/
99def freeGroupHomFoxJacobianAbsolute
100 [DecidableEq Y]
101 (φ : FreeGroup X →* FreeGroup Y) :
102 X → Y → GroupRing (FreeGroup Y) :=
103 freeGroupHomFoxJacobian (H := FreeGroup Y) (MonoidHom.id (FreeGroup Y)) φ
105/-- The absolute Fox Jacobian, packaged as a matrix. -/
106def freeGroupHomFoxJacobianAbsoluteMatrix
107 [DecidableEq Y]
108 (φ : FreeGroup X →* FreeGroup Y) :
109 Matrix X Y (GroupRing (FreeGroup Y)) :=
110 freeGroupHomFoxJacobianAbsolute φ
112/--
113Evaluating the bundled absolute Fox Jacobian matrix at `(x, y)` returns the corresponding absolute
114Fox derivative.
115-/
116@[simp]
117theorem freeGroupHomFoxJacobianAbsoluteMatrix_apply
118 [DecidableEq Y]
119 (φ : FreeGroup X →* FreeGroup Y) (x : X) (y : Y) :
120 freeGroupHomFoxJacobianAbsoluteMatrix φ x y =
121 freeGroupHomFoxJacobianAbsolute φ x y :=
122 rfl
124/-- The absolute Fox Jacobian of the identity homomorphism is the coordinate identity family. -/
125@[simp]
126theorem freeGroupHomFoxJacobianAbsolute_id
127 [DecidableEq X] :
128 freeGroupHomFoxJacobianAbsolute (MonoidHom.id (FreeGroup X)) =
129 fun x : X => Pi.single x (1 : GroupRing (FreeGroup X)) := by
130 funext x y
131 simp only [freeGroupHomFoxJacobianAbsolute, freeGroupHomFoxJacobian, MonoidHom.id_apply,
132 relativeFreeGroupFoxDerivative_of]
134/-- The absolute Fox Jacobian matrix of the identity homomorphism is the identity matrix. -/
135@[simp]
136theorem freeGroupHomFoxJacobianAbsoluteMatrix_id
137 [DecidableEq X] :
138 freeGroupHomFoxJacobianAbsoluteMatrix (MonoidHom.id (FreeGroup X)) =
139 (1 : Matrix X X (GroupRing (FreeGroup X))) := by
140 apply Matrix.ext
141 intro x y
142 change freeGroupHomFoxJacobianAbsolute (MonoidHom.id (FreeGroup X)) x y =
143 (1 : Matrix X X (GroupRing (FreeGroup X))) x y
144 rw [show
145 freeGroupHomFoxJacobianAbsolute (MonoidHom.id (FreeGroup X)) x y =
146 (Pi.single x (1 : GroupRing (FreeGroup X)) : X → GroupRing (FreeGroup X)) y from
147 congrFun (congrFun freeGroupHomFoxJacobianAbsolute_id x) y]
148 by_cases hxy : x = y
149 · subst y
150 simp only [Pi.single_eq_same, Matrix.one_apply_eq]
151 · simp only [ne_eq, hxy, not_false_eq_true, Pi.single_eq_of_ne', Matrix.one_apply_ne]
153variable {K : Type t} [Group K]
155/--
156Postcomposing the coefficient homomorphism maps each relative Fox Jacobian entry through the induced
157group-ring map.
158-/
159theorem freeGroupHomFoxJacobian_mapDomain_apply
160 [DecidableEq Y]
161 (ψ : FreeGroup Y →* H) (η : H →* K)
162 (φ : FreeGroup X →* FreeGroup Y) (x : X) (y : Y) :
163 freeGroupHomFoxJacobian (H := K) (η.comp ψ) φ x y =
164 groupRingMap η (freeGroupHomFoxJacobian (H := H) ψ φ x y) := by
165 simp only [freeGroupHomFoxJacobian, relativeFreeGroupFoxDerivative_mapDomain_apply]
167/-- Fox Jacobians are natural under coefficient push-forward, matrix form. -/
168theorem freeGroupHomFoxJacobianMatrix_mapDomain
169 [DecidableEq Y]
170 (ψ : FreeGroup Y →* H) (η : H →* K)
171 (φ : FreeGroup X →* FreeGroup Y) :
172 freeGroupHomFoxJacobianMatrix (H := K) (η.comp ψ) φ =
173 (freeGroupHomFoxJacobianMatrix (H := H) ψ φ).map (groupRingMap η) := by
174 apply Matrix.ext
175 intro x y
176 simp only [freeGroupHomFoxJacobianMatrix, freeGroupHomFoxJacobian_mapDomain_apply,
177 Matrix.map_apply]
179/--
180A relative Fox Jacobian entry is the image of the corresponding absolute entry under the coefficient
181group-ring map.
182-/
183theorem freeGroupHomFoxJacobian_eq_map_absolute_apply
184 [DecidableEq Y]
185 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
186 (x : X) (y : Y) :
187 freeGroupHomFoxJacobian (H := H) ψ φ x y =
188 groupRingMap ψ (freeGroupHomFoxJacobianAbsolute φ x y) := by
189 simpa [freeGroupHomFoxJacobianAbsolute] using
190 freeGroupHomFoxJacobian_mapDomain_apply
191 (H := FreeGroup Y) (K := H)
192 (MonoidHom.id (FreeGroup Y)) ψ φ x y
194/-- Matrix form of the absolute-to-relative comparison for Fox Jacobians. -/
195theorem freeGroupHomFoxJacobianMatrix_eq_map_absolute
196 [DecidableEq Y]
197 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
198 freeGroupHomFoxJacobianMatrix (H := H) ψ φ =
199 (freeGroupHomFoxJacobianAbsoluteMatrix φ).map (groupRingMap ψ) := by
200 apply Matrix.ext
201 intro x y
202 simp only [freeGroupHomFoxJacobianMatrix, freeGroupHomFoxJacobian_eq_map_absolute_apply,
203 freeGroupHomFoxJacobianAbsoluteMatrix, Matrix.map_apply]
206end FoxCalculus
208end
210end FoxDifferential