FoxDifferential/Discrete/Jacobian/Basic.lean
1import FoxDifferential.Discrete.Absolute
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Discrete/Jacobian/Basic.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Discrete group-ring Fox calculus
14Ordinary Fox derivatives over group rings are developed through augmentation, relative differential modules, coordinates, Jacobians, and chain rules.
15-/
16namespace FoxDifferential
18noncomputable section
20namespace FoxCalculus
22open scoped BigOperators
24universe u v w z t
26variable {H : Type w} [Group H]
27variable {X : Type u} {Y : Type v}
29/-- The relative Fox Jacobian of `φ : FreeGroup X ->* FreeGroup Y`, with coefficients pushed
30forward by `ψ : FreeGroup Y ->* H`.
33with respect to the `Y`-generators. -/
35 [DecidableEq Y]
36 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
38 fun x =>
39 relativeFreeGroupFoxDerivative (H := H) Y ψ (φ (FreeGroup.of x))
41/-- The relative Fox Jacobian, packaged as a matrix. -/
43 [DecidableEq Y]
44 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
46 freeGroupHomFoxJacobian (H := H) ψ φ
48/-- Matrix evaluation is componentwise the relative Fox Jacobian. -/
49@[simp]
51 [DecidableEq Y]
52 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
53 (x : X) (y : Y) :
54 freeGroupHomFoxJacobianMatrix (H := H) ψ φ x y =
55 freeGroupHomFoxJacobian (H := H) ψ φ x y :=
56 rfl
58/-- The usual relative Fox Jacobian is the coefficient-generic free crossed-differential
59Jacobian specialized to the group-ring coefficient homomorphism. -/
61 [DecidableEq Y]
62 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
63 freeGroupHomFoxJacobian (H := H) ψ φ =
64 freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Y) (groupRingScalar ψ) φ := by
65 funext x y
69/-- Matrix form of the comparison between the usual relative Fox Jacobian and the
70coefficient-generic free crossed-differential Jacobian. -/
72 [DecidableEq Y]
73 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
74 freeGroupHomFoxJacobianMatrix (H := H) ψ φ =
76 (X := X) (Y := Y) (groupRingScalar ψ) φ := by
77 apply Matrix.ext
78 intro x y
79 simp only [freeGroupHomFoxJacobianMatrix_apply,
83/-- The absolute Fox Jacobian of a homomorphism between free groups. -/
85 [DecidableEq Y]
86 (φ : FreeGroup X →* FreeGroup Y) :
88 freeGroupHomFoxJacobian (H := FreeGroup Y) (MonoidHom.id (FreeGroup Y)) φ
90/-- The absolute Fox Jacobian, packaged as a matrix. -/
92 [DecidableEq Y]
93 (φ : FreeGroup X →* FreeGroup Y) :
97/-- Matrix evaluation is componentwise the absolute Fox Jacobian. -/
98@[simp]
100 [DecidableEq Y]
101 (φ : FreeGroup X →* FreeGroup Y) (x : X) (y : Y) :
103 freeGroupHomFoxJacobianAbsolute φ x y :=
104 rfl
106/-- The absolute Fox Jacobian of the identity homomorphism is the coordinate identity family. -/
107@[simp]
109 [DecidableEq X] :
110 freeGroupHomFoxJacobianAbsolute (MonoidHom.id (FreeGroup X)) =
112 funext x y
113 simp only [freeGroupHomFoxJacobianAbsolute, freeGroupHomFoxJacobian, MonoidHom.id_apply,
116/-- The absolute Fox Jacobian matrix of the identity homomorphism is the identity matrix. -/
117@[simp]
119 [DecidableEq X] :
120 freeGroupHomFoxJacobianAbsoluteMatrix (MonoidHom.id (FreeGroup X)) =
122 apply Matrix.ext
123 intro x y
124 change freeGroupHomFoxJacobianAbsolute (MonoidHom.id (FreeGroup X)) x y =
126 rw [show
127 freeGroupHomFoxJacobianAbsolute (MonoidHom.id (FreeGroup X)) x y =
129 congrFun (congrFun freeGroupHomFoxJacobianAbsolute_id x) y]
130 by_cases hxy : x = y
131 · subst y
132 simp only [Pi.single_eq_same, Matrix.one_apply_eq]
133 · simp only [ne_eq, hxy, not_false_eq_true, Pi.single_eq_of_ne', Matrix.one_apply_ne]
135variable {K : Type t} [Group K]
137/-- Fox Jacobians are natural under coefficient push-forward, component form. -/
139 [DecidableEq Y]
140 (ψ : FreeGroup Y →* H) (η : H →* K)
141 (φ : FreeGroup X →* FreeGroup Y) (x : X) (y : Y) :
142 freeGroupHomFoxJacobian (H := K) (η.comp ψ) φ x y =
143 groupRingMap η (freeGroupHomFoxJacobian (H := H) ψ φ x y) := by
146/-- Fox Jacobians are natural under coefficient push-forward, matrix form. -/
148 [DecidableEq Y]
149 (ψ : FreeGroup Y →* H) (η : H →* K)
150 (φ : FreeGroup X →* FreeGroup Y) :
151 freeGroupHomFoxJacobianMatrix (H := K) (η.comp ψ) φ =
152 (freeGroupHomFoxJacobianMatrix (H := H) ψ φ).map (groupRingMap η) := by
153 apply Matrix.ext
154 intro x y
155 simp only [freeGroupHomFoxJacobianMatrix, freeGroupHomFoxJacobian_mapDomain_apply, Matrix.map_apply]
157/-- A relative Fox Jacobian is obtained from the absolute Jacobian by pushing coefficients
158forward. -/
160 [DecidableEq Y]
161 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
162 (x : X) (y : Y) :
163 freeGroupHomFoxJacobian (H := H) ψ φ x y =
164 groupRingMap ψ (freeGroupHomFoxJacobianAbsolute φ x y) := by
165 simpa [freeGroupHomFoxJacobianAbsolute] using
167 (H := FreeGroup Y) (K := H)
168 (MonoidHom.id (FreeGroup Y)) ψ φ x y
170/-- Matrix form of the absolute-to-relative comparison for Fox Jacobians. -/
172 [DecidableEq Y]
173 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
174 freeGroupHomFoxJacobianMatrix (H := H) ψ φ =
175 (freeGroupHomFoxJacobianAbsoluteMatrix φ).map (groupRingMap ψ) := by
176 apply Matrix.ext
177 intro x y
179 freeGroupHomFoxJacobianAbsoluteMatrix, Matrix.map_apply]
182end FoxCalculus
184end
186end FoxDifferential