Yamaguchi Lean 4 Library
FoxDifferential/Common/Jacobian.lean
FoxDifferential/Common/Jacobian/Source

FoxDifferential/Common/Jacobian.lean

1import Mathlib.Algebra.Module.LinearMap.Basic
2import Mathlib.Data.Matrix.Mul
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Common/Jacobian.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Universal Fox calculus
15Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
16-/
17namespace FoxDifferential
19noncomputable section
21open scoped BigOperators
23universe u v w z
25section JacobianLinearMap
27variable {R : Type u} [Ring R]
28variable {X : Type v}
29variable {Y : Type w}
31/-- A Fox-Jacobian family packaged as a matrix. -/
32def foxJacobianMatrix (jac : X → Y → R) : Matrix X Y R :=
33 jac
35omit [Ring R] in
36/-- Matrix evaluation is componentwise the Fox-Jacobian family. -/
37@[simp]
38theorem foxJacobianMatrix_apply (jac : X → Y → R) (x : X) (y : Y) :
39 foxJacobianMatrix jac x y = jac x y :=
40 rfl
42section Identity
44variable [DecidableEq X]
46/-- The identity Fox-Jacobian family. -/
47def foxJacobianId : X → X → R := fun x => Pi.single x (1 : R)
49/-- Evaluation formula for the identity Fox-Jacobian family. -/
50@[simp]
51theorem foxJacobianId_apply (x y : X) :
52 foxJacobianId (R := R) (X := X) x y = (Pi.single x (1 : R) : X → R) y :=
53 rfl
55/-- The identity Fox-Jacobian family is the identity matrix. -/
56@[simp]
58 foxJacobianMatrix (R := R) (X := X) (Y := X) (foxJacobianId (R := R) (X := X)) =
59 (1 : Matrix X X R) := by
60 ext x y
61 by_cases hxy : x = y
62 · subst y
63 simp only [foxJacobianMatrix, foxJacobianId, Pi.single_eq_same, Matrix.one_apply_eq]
64 · simp only [foxJacobianMatrix, foxJacobianId, ne_eq, hxy, not_false_eq_true, Pi.single_eq_of_ne',
65 Matrix.one_apply_ne]
67end Identity
69/-- The finite linear map encoded by a Fox-Jacobian family. -/
70def foxJacobianLinearMap [Fintype X] (jac : X → Y → R) :
71 (X → R) →ₗ[R] (Y → R) where
72 toFun v := fun y => ∑ x : X, v x * jac x y
73 map_add' v w := by
74 funext y
75 simp only [Pi.add_apply, add_mul, Finset.sum_add_distrib]
76 map_smul' a v := by
77 funext y
78 simp only [Pi.smul_apply]
79 change (∑ x : X, (a * v x) * jac x y) = a * ∑ x : X, v x * jac x y
80 simp only [mul_assoc, Finset.mul_sum]
82/-- Evaluation formula for the finite linear map encoded by a Fox-Jacobian family. -/
83@[simp]
85 [Fintype X]
86 (jac : X → Y → R) (v : X → R) (y : Y) :
87 foxJacobianLinearMap jac v y = ∑ x : X, v x * jac x y :=
88 rfl
90/-- The Fox-Jacobian linear map is row-vector multiplication by the corresponding matrix. -/
92 [Fintype X]
93 (jac : X → Y → R) (v : X → R) :
94 foxJacobianLinearMap jac v = Matrix.vecMul v (foxJacobianMatrix jac) := by
95 funext y
96 simp only [foxJacobianLinearMap_apply, Matrix.vecMul, dotProduct, foxJacobianMatrix]
98/-- The linear map encoded by the identity Fox-Jacobian family is the identity. -/
99@[simp]
100theorem foxJacobianLinearMap_id [Fintype X] [DecidableEq X] :
101 foxJacobianLinearMap (R := R) (X := X) (Y := X) (foxJacobianId (R := R) (X := X)) =
102 (LinearMap.id : (X → R) →ₗ[R] (X → R)) := by
103 apply LinearMap.ext
104 intro v
105 funext y
106 change (∑ x : X, v x * (Pi.single x (1 : R) : X → R) y) = v y
107 rw [Finset.sum_eq_single y]
108 · simp only [Pi.single_eq_same, mul_one]
109 · intro x _ hxy
110 rw [Pi.single_eq_of_ne (Ne.symm hxy)]
111 simp only [mul_zero]
112 · intro hy
113 simp only [Finset.mem_univ, not_true_eq_false] at hy
115variable {Z : Type z}
117/-- Composition of finite Fox-Jacobian linear maps is multiplication of Jacobian kernels. -/
119 [Fintype X] [Fintype Y]
120 (jacXY : X → Y → R) (jacYZ : Y → Z → R) :
122 foxJacobianLinearMap (fun x z => ∑ y : Y, jacXY x y * jacYZ y z) := by
123 ext v z
124 change
125 (∑ y : Y, (∑ x : X, v x * jacXY x y) * jacYZ y z) =
126 ∑ x : X, v x * ∑ y : Y, jacXY x y * jacYZ y z
127 calc
128 (∑ y : Y, (∑ x : X, v x * jacXY x y) * jacYZ y z) =
129 ∑ y : Y, ∑ x : X, (v x * jacXY x y) * jacYZ y z := by
130 simp only [Finset.sum_mul]
131 _ = ∑ x : X, ∑ y : Y, (v x * jacXY x y) * jacYZ y z := by
132 rw [Finset.sum_comm]
133 _ = ∑ x : X, v x * ∑ y : Y, jacXY x y * jacYZ y z := by
134 refine Finset.sum_congr rfl ?_
135 intro x _
136 rw [Finset.mul_sum]
137 refine Finset.sum_congr rfl ?_
138 intro y _
139 rw [mul_assoc]
141/-- Composition of Fox-Jacobian matrices is multiplication of Jacobian kernels. -/
143 [Fintype Y]
144 (jacXY : X → Y → R) (jacYZ : Y → Z → R) :
145 foxJacobianMatrix (R := R) (X := X) (Y := Z)
146 (fun x z => ∑ y : Y, jacXY x y * jacYZ y z) =
147 foxJacobianMatrix (R := R) (X := X) (Y := Y) jacXY *
148 foxJacobianMatrix (R := R) (X := Y) (Y := Z) jacYZ := by
149 apply Matrix.ext
150 intro x z
151 simp only [foxJacobianMatrix, Matrix.mul_apply]
153/-- A Fox-Jacobian linear map sends a standard source coordinate to the corresponding Jacobian
154row. -/
155@[simp]
156theorem foxJacobianLinearMap_single [Fintype X] [DecidableEq X] (jac : X → Y → R) (x : X) :
157 foxJacobianLinearMap jac (Pi.single x (1 : R)) = jac x := by
158 funext y
159 change (∑ z : X, ((Pi.single x (1 : R) : X → R) z) * jac z y) = jac x y
160 rw [Finset.sum_eq_single x]
161 · simp only [Pi.single_eq_same, one_mul]
162 · intro z _ hz
163 simp only [Pi.single_eq_of_ne hz, zero_mul]
164 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_mul, IsEmpty.forall_iff]
166variable {M : Type*} [AddCommMonoid M] [Module R M]
168/-- Linear maps out of finite coordinate vectors are determined by the standard coordinate
169vectors. -/
171 [Finite X] [DecidableEq X]
172 {L₁ L₂ : (X → R) →ₗ[R] M}
173 (h : ∀ x : X, L₁ (Pi.single x (1 : R)) = L₂ (Pi.single x (1 : R))) :
174 L₁ = L₂ := by
175 classical
176 letI := Fintype.ofFinite X
177 apply LinearMap.ext
178 intro v
179 have hv : v = ∑ x : X, v x • (Pi.single x (1 : R) : X → R) := by
180 funext y
181 rw [Finset.sum_apply]
182 rw [Finset.sum_eq_single y]
183 · simp only [Pi.smul_apply, Pi.single_eq_same, smul_eq_mul, mul_one]
184 · intro x _ hxy
185 change v x * ((Pi.single x (1 : R) : X → R) y) = 0
186 rw [Pi.single_eq_of_ne (Ne.symm hxy)]
187 simp only [mul_zero]
188 · intro hy
189 simp only [Finset.mem_univ, not_true_eq_false] at hy
190 calc
191 L₁ v = L₁ (∑ x : X, v x • (Pi.single x (1 : R) : X → R)) := by
192 exact congrArg L₁ hv
193 _ = ∑ x : X, v x • L₁ (Pi.single x (1 : R)) := by simp only [map_sum, map_smul]
194 _ = ∑ x : X, v x • L₂ (Pi.single x (1 : R)) := by simp only [h]
195 _ = L₂ (∑ x : X, v x • (Pi.single x (1 : R) : X → R)) := by simp only [map_sum, map_smul]
196 _ = L₂ v := by
197 exact (congrArg L₂ hv).symm
199end JacobianLinearMap
201end
203end FoxDifferential