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

FoxDifferential/Common/FreeCrossedDifferential.lean

1import FoxDifferential.Common.CrossedDifferential
2import FoxDifferential.Common.Jacobian
3import Mathlib.GroupTheory.FreeGroup.Basic
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FoxDifferential/Common/FreeCrossedDifferential.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Universal Fox calculus
16Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
17-/
18namespace FoxDifferential
20noncomputable section
22open scoped BigOperators
24universe u v
26variable {R : Type*} [Semiring R]
27variable {A : Type*} [AddCommGroup A] [Module R A]
28variable {X : Type u}
30/-- The semidirect product used to construct a free crossed differential with coefficients
31`coeff : FreeGroup X →* R`. The right component remembers the free-group word, while the left
32component accumulates the crossed differential value. -/
34 (coeff : FreeGroup X →* R) (A : Type*) [AddCommGroup A] [Module R A] where
35 /-- Additive component carrying the crossed differential value. -/
36 left : A
37 /-- Free-group component carrying the source word. -/
38 right : FreeGroup X
42variable (coeff : FreeGroup X →* R)
44/-- Identity element in the semidirect product used for free crossed differentials. -/
46 One (FreeCrossedDifferentialSemidirect (X := X) coeff A) where
47 one := ⟨0, 1⟩
49/-- Multiplication in the semidirect product used for free crossed differentials. -/
51 Mul (FreeCrossedDifferentialSemidirect (X := X) coeff A) where
52 mul x y := ⟨x.left + coeff x.right • y.left, x.right * y.right⟩
54/-- Inversion in the semidirect product used for free crossed differentials. -/
56 Inv (FreeCrossedDifferentialSemidirect (X := X) coeff A) where
57 inv x := ⟨-(coeff x.right⁻¹ • x.left), x.right⁻¹⟩
59/-- Extensionality for the free crossed-differential semidirect product. -/
60@[ext]
61theorem ext {x y : FreeCrossedDifferentialSemidirect (X := X) coeff A}
62 (hleft : x.left = y.left) (hright : x.right = y.right) : x = y := by
63 cases x
64 cases y
65 simp_all
67/-- The additive component of the identity semidirect element is zero. -/
68@[simp]
69theorem one_left :
70 (1 : FreeCrossedDifferentialSemidirect (X := X) coeff A).left = 0 :=
71 rfl
73/-- The free-group component of the identity semidirect element is the identity word. -/
74@[simp]
75theorem one_right :
76 (1 : FreeCrossedDifferentialSemidirect (X := X) coeff A).right = 1 :=
77 rfl
79/-- The additive component of semidirect multiplication. -/
80@[simp]
81theorem mul_left (x y : FreeCrossedDifferentialSemidirect (X := X) coeff A) :
82 (x * y).left = x.left + coeff x.right • y.left :=
83 rfl
85/-- The free-group component of semidirect multiplication. -/
86@[simp]
87theorem mul_right (x y : FreeCrossedDifferentialSemidirect (X := X) coeff A) :
88 (x * y).right = x.right * y.right :=
89 rfl
91/-- The additive component of semidirect inversion. -/
92@[simp]
93theorem inv_left (x : FreeCrossedDifferentialSemidirect (X := X) coeff A) :
94 x⁻¹.left = -(coeff x.right⁻¹ • x.left) :=
95 rfl
97/-- The free-group component of semidirect inversion. -/
98@[simp]
99theorem inv_right (x : FreeCrossedDifferentialSemidirect (X := X) coeff A) :
100 x⁻¹.right = x.right⁻¹ :=
101 rfl
103/-- Group structure on the semidirect product used for free crossed differentials. -/
105 Group (FreeCrossedDifferentialSemidirect (X := X) coeff A) where
106 one := 1
107 mul := (· * ·)
108 inv := Inv.inv
109 mul_assoc x y z := by
110 ext
111 · simp only [mul_left, mul_right, map_mul, add_assoc, smul_add, smul_smul]
112 · simp only [mul_right, mul_assoc]
113 one_mul x := by
114 ext
115 · simp only [mul_left, one_left, one_right, map_one, one_smul, zero_add]
116 · simp only [mul_right, one_right, one_mul]
117 mul_one x := by
118 ext
119 · simp only [mul_left, one_left, smul_zero, add_zero]
120 · simp only [mul_right, one_right, mul_one]
121 inv_mul_cancel x := by
122 ext
123 · simp only [mul_left, inv_left, inv_right, neg_add_cancel, one_left]
124 · simp only [mul_right, inv_right, inv_mul_cancel, one_right]
128variable (coeff : FreeGroup X →* R) (basisValue : X → A)
130/-- The semidirect lift whose left component is the free crossed differential with prescribed
131generator values. -/
133 FreeGroup X →* FreeCrossedDifferentialSemidirect (X := X) coeff A :=
134 FreeGroup.lift fun x => ⟨basisValue x, FreeGroup.of x⟩
136/-- The free crossed differential with coefficient homomorphism `coeff` and prescribed generator
137values `basisValue`. -/
138def freeCrossedDifferentialWithCoeff (w : FreeGroup X) : A :=
139 (freeCrossedDifferentialWithCoeffLift (A := A) coeff basisValue w).left
141/-- The right component of the free crossed-differential lift is the identity on the free group. -/
142@[simp]
144 (freeCrossedDifferentialWithCoeffLift (A := A) coeff basisValue w).right = w := by
145 induction w using FreeGroup.induction_on with
146 | C1 =>
147 simp only [freeCrossedDifferentialWithCoeffLift, map_one, FreeCrossedDifferentialSemidirect.one_right]
148 | of x =>
149 simp only [freeCrossedDifferentialWithCoeffLift, FreeGroup.lift_apply_of]
150 | inv_of x hx =>
151 simpa using congrArg Inv.inv hx
152 | mul x y hx hy =>
153 simp only [map_mul, FreeCrossedDifferentialSemidirect.mul_right, hx, hy]
155/-- The free crossed differential sends the identity word to zero. -/
156@[simp]
158 freeCrossedDifferentialWithCoeff (A := A) coeff basisValue 1 = 0 := by
160 FreeCrossedDifferentialSemidirect.one_left]
162/-- The free crossed differential sends a free generator to its prescribed value. -/
163@[simp]
165 freeCrossedDifferentialWithCoeff (A := A) coeff basisValue (FreeGroup.of x) =
166 basisValue x := by
169/-- Product rule for the free crossed differential with arbitrary coefficients. -/
170theorem freeCrossedDifferentialWithCoeff_mul (u v : FreeGroup X) :
171 freeCrossedDifferentialWithCoeff (A := A) coeff basisValue (u * v) =
172 freeCrossedDifferentialWithCoeff (A := A) coeff basisValue u +
173 coeff u • freeCrossedDifferentialWithCoeff (A := A) coeff basisValue v := by
174 simp only [freeCrossedDifferentialWithCoeff, map_mul, FreeCrossedDifferentialSemidirect.mul_left,
177/-- Inverse rule for the free crossed differential with arbitrary coefficients. -/
178theorem freeCrossedDifferentialWithCoeff_inv (w : FreeGroup X) :
179 freeCrossedDifferentialWithCoeff (A := A) coeff basisValue w⁻¹ =
180 -(coeff w⁻¹ • freeCrossedDifferentialWithCoeff (A := A) coeff basisValue w) := by
181 simp only [freeCrossedDifferentialWithCoeff, map_inv, FreeCrossedDifferentialSemidirect.inv_left,
184/-- The free crossed differential with arbitrary coefficients satisfies the Fox Leibniz rule. -/
187 (freeCrossedDifferentialWithCoeff (A := A) coeff basisValue) := by
188 intro u v
189 simpa using freeCrossedDifferentialWithCoeff_mul (A := A) coeff basisValue u v
191/-- Uniqueness of crossed differentials on a free group from their generator values, for an
192arbitrary coefficient homomorphism. -/
194 (delta : FreeGroup X → A)
195 (hdelta : IsCrossedDifferential coeff delta)
196 (hbasis : ∀ x : X, delta (FreeGroup.of x) = basisValue x) :
197 delta = freeCrossedDifferentialWithCoeff (A := A) coeff basisValue := by
198 funext w
199 induction w using FreeGroup.induction_on with
200 | C1 =>
201 rw [IsCrossedDifferential.one hdelta, freeCrossedDifferentialWithCoeff_one]
202 | of x =>
204 | inv_of x hx =>
205 rw [IsCrossedDifferential.inv hdelta,
207 | mul u v hu hv =>
208 rw [hdelta u v, freeCrossedDifferentialWithCoeff_mul, hu, hv]
210/-- Existence and uniqueness of crossed differentials on a free group from arbitrary generator
211values and an arbitrary coefficient homomorphism. -/
213 ∃! delta : FreeGroup X → A,
214 IsCrossedDifferential coeff delta ∧
215 ∀ x : X, delta (FreeGroup.of x) = basisValue x := by
216 refine ⟨freeCrossedDifferentialWithCoeff (A := A) coeff basisValue, ?_, ?_⟩
217 · exact ⟨freeCrossedDifferentialWithCoeff_isCrossedDifferential (A := A) coeff basisValue,
218 freeCrossedDifferentialWithCoeff_of (A := A) coeff basisValue⟩
219 · intro delta hdelta
220 exact freeCrossedDifferentialWithCoeff_unique (A := A) coeff basisValue
221 delta hdelta.1 hdelta.2
223/-- Crossed differentials on a free group are equivalent to assignments of values on the free
224generators. -/
226 {delta : FreeGroup X → A // IsCrossedDifferential coeff delta} ≃ (X → A) where
227 toFun delta := fun x => delta.1 (FreeGroup.of x)
228 invFun basisValue :=
229 ⟨freeCrossedDifferentialWithCoeff (A := A) coeff basisValue,
231 left_inv delta := by
232 apply Subtype.ext
234 (fun x => delta.1 (FreeGroup.of x)) delta.1 delta.2 (by intro x; rfl)).symm
235 right_inv basisValue := by
236 funext x
239section Coordinates
241variable {S : Type*} [Ring S]
242variable {B : Type*} [AddCommGroup B] [Module S B]
243variable {Y : Type v}
244variable [DecidableEq X]
246/-- The universal Fox-coordinate crossed differential for an arbitrary coefficient homomorphism
247to a ring. -/
249 (coeff : FreeGroup X →* S) (w : FreeGroup X) : X → S :=
251 (A := X → S) coeff (fun x => Pi.single x (1 : S)) w
253/-- The coordinate crossed differential sends the identity word to zero. -/
254@[simp]
256 (coeff : FreeGroup X →* S) :
257 freeCrossedDifferentialWithCoeffCoordinates (X := X) coeff (1 : FreeGroup X) = 0 := by
260/-- The coordinate crossed differential sends a generator to the standard coordinate vector. -/
261@[simp]
263 (coeff : FreeGroup X →* S) (x : X) :
264 freeCrossedDifferentialWithCoeffCoordinates (X := X) coeff (FreeGroup.of x) =
265 Pi.single x (1 : S) := by
268/-- The coordinate crossed differential is a crossed differential. -/
270 (coeff : FreeGroup X →* S) :
274 (A := X → S) coeff (fun x => Pi.single x (1 : S))
276/-- The finite linear map evaluating a coordinate vector on prescribed generator values. -/
278 [Fintype X] (basisValue : X → B) : (X → S) →ₗ[S] B where
279 toFun v := ∑ x : X, v x • basisValue x
280 map_add' v w := by
281 simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
282 map_smul' a v := by
283 simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, Finset.smul_sum, smul_smul]
285omit [DecidableEq X] in
286/-- Evaluation formula for the finite expansion linear map. -/
287@[simp]
289 [Fintype X] (basisValue : X → B) (v : X → S) :
291 ∑ x : X, v x • basisValue x :=
292 rfl
294/-- The expansion linear map sends a standard coordinate vector to the corresponding value. -/
295@[simp]
297 [Fintype X] (basisValue : X → B) (x : X) :
299 (Pi.single x (1 : S)) =
300 basisValue x := by
302 rw [Finset.sum_eq_single x]
303 · simp only [Pi.single_eq_same, one_smul]
304 · intro y _ hy
305 simp only [Pi.single_eq_of_ne hy, zero_smul]
306 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_smul, IsEmpty.forall_iff]
308/-- The Fox-coordinate expansion determined by arbitrary coefficient coordinates. -/
310 [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B)
311 (w : FreeGroup X) : B :=
315/-- The coefficient-coordinate expansion is a crossed differential. -/
317 [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B) :
319 (freeCrossedDifferentialWithCoeffExpansion (X := X) coeff basisValue) := by
320 exact IsCrossedDifferential.map_linear
324/-- The coefficient-coordinate expansion sends each generator to its prescribed value. -/
325@[simp]
327 [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B) (x : X) :
328 freeCrossedDifferentialWithCoeffExpansion (X := X) coeff basisValue (FreeGroup.of x) =
329 basisValue x := by
334/-- A free crossed differential is its coefficient-coordinate expansion. -/
336 [Fintype X] (coeff : FreeGroup X →* S) (basisValue : X → B) (w : FreeGroup X) :
337 freeCrossedDifferentialWithCoeff (A := B) coeff basisValue w =
338 freeCrossedDifferentialWithCoeffExpansion (X := X) coeff basisValue w := by
339 have h :=
341 (A := B) coeff basisValue
344 (X := X) coeff basisValue)
346 exact congrFun h.symm w
348/-- Abstract Fox chain rule: composing a crossed differential with a free-group homomorphism is
349the coordinate expansion using the pulled-back coefficient homomorphism. -/
351 [Fintype X]
352 (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
353 (delta : FreeGroup Y → B) (hdelta : IsCrossedDifferential coeff delta)
354 (w : FreeGroup X) :
355 delta (φ w) =
357 (X := X) (coeff.comp φ) (fun x : X => delta (φ (FreeGroup.of x))) w := by
358 let pulled : FreeGroup X → B := fun w => delta (φ w)
359 have hpulled : IsCrossedDifferential (coeff.comp φ) pulled :=
360 hdelta.comp_monoidHom φ
361 have hunique :
362 pulled =
364 (A := B) (coeff.comp φ) (fun x : X => delta (φ (FreeGroup.of x))) :=
366 (A := B) (coeff.comp φ) (fun x : X => delta (φ (FreeGroup.of x)))
367 pulled hpulled (by intro x; rfl)
368 calc
369 delta (φ w) = pulled w := rfl
370 _ =
372 (A := B) (coeff.comp φ) (fun x : X => delta (φ (FreeGroup.of x))) w := by
373 exact congrFun hunique w
374 _ =
376 (X := X) (coeff.comp φ) (fun x : X => delta (φ (FreeGroup.of x))) w := by
378 (X := X) (B := B) (coeff.comp φ)
379 (fun x : X => delta (φ (FreeGroup.of x))) w
381omit [DecidableEq X] in
382/-- The abstract Fox-Jacobian of a homomorphism of free sources, with coefficients in `S`. -/
384 [DecidableEq Y] (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) :
385 X → Y → S :=
386 fun x => freeCrossedDifferentialWithCoeffCoordinates (X := Y) coeff (φ (FreeGroup.of x))
388omit [DecidableEq X] in
389/-- The abstract Fox-Jacobian of a free-source homomorphism as a matrix. -/
391 [DecidableEq Y] (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) :
392 Matrix X Y S :=
395omit [DecidableEq X] in
396/-- Evaluation of the abstract Fox-Jacobian matrix. -/
397@[simp]
399 [DecidableEq Y] (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
400 (x : X) (y : Y) :
403 rfl
405omit [DecidableEq X] in
406/-- The finite linear map encoded by the abstract Fox-Jacobian. -/
408 [Fintype X] [DecidableEq Y]
409 (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) :
410 (X → S) →ₗ[S] (Y → S) :=
413omit [DecidableEq X] in
414/-- Evaluation formula for the finite linear map encoded by the abstract Fox-Jacobian. -/
415@[simp]
417 [Fintype X] [DecidableEq Y]
418 (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
419 (v : X → S) (y : Y) :
421 ∑ x : X, v x * freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ x y :=
422 rfl
424/-- The abstract Fox-Jacobian linear map sends a source basis vector to the corresponding row. -/
425@[simp]
427 [Fintype X] [DecidableEq Y]
428 (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) (x : X) :
430 (Pi.single x (1 : S)) =
435omit [DecidableEq X] in
436/-- The abstract Fox-Jacobian linear map is row-vector multiplication by its matrix. -/
438 [Fintype X] [DecidableEq Y]
439 (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y) (v : X → S) :
441 Matrix.vecMul v
446/-- The abstract Fox-Jacobian of the identity homomorphism is the identity family. -/
447@[simp]
448theorem freeCrossedDifferentialWithCoeffJacobian_id (coeff : FreeGroup X →* S) :
450 (X := X) (Y := X) coeff (MonoidHom.id (FreeGroup X)) =
451 foxJacobianId (R := S) (X := X) := by
452 funext x y
453 simp only [freeCrossedDifferentialWithCoeffJacobian, MonoidHom.id_apply,
456/-- The abstract Fox-Jacobian matrix of the identity homomorphism is the identity matrix. -/
457@[simp]
458theorem freeCrossedDifferentialWithCoeffJacobianMatrix_id (coeff : FreeGroup X →* S) :
460 (X := X) (Y := X) coeff (MonoidHom.id (FreeGroup X)) =
461 (1 : Matrix X X S) := by
466/-- The abstract Fox-Jacobian linear map of the identity homomorphism is the identity. -/
467@[simp]
469 [Fintype X] (coeff : FreeGroup X →* S) :
471 (X := X) (Y := X) coeff (MonoidHom.id (FreeGroup X)) =
472 (LinearMap.id : (X → S) →ₗ[S] (X → S)) := by
477/-- Abstract Fox chain rule, vector form. -/
479 [Fintype X] [DecidableEq Y]
480 (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
481 (w : FreeGroup X) :
484 (freeCrossedDifferentialWithCoeffCoordinates (X := X) (coeff.comp φ) w) := by
485 have h :=
487 (X := X) (Y := Y) (B := Y → S) coeff φ
490 calc
493 (X := X) (coeff.comp φ)
494 (fun x : X =>
496 (φ (FreeGroup.of x))) w := h
497 _ =
499 (freeCrossedDifferentialWithCoeffCoordinates (X := X) (coeff.comp φ) w) := by
500 funext y
502 LinearMap.coe_mk, AddHom.coe_mk, Finset.sum_apply, Pi.smul_apply, smul_eq_mul,
506/-- Abstract Fox chain rule, component form. -/
508 [Fintype X] [DecidableEq Y]
509 (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
510 (w : FreeGroup X) (y : Y) :
512 ∑ x : X,
513 freeCrossedDifferentialWithCoeffCoordinates (X := X) (coeff.comp φ) w x *
514 freeCrossedDifferentialWithCoeffJacobian (X := X) coeff φ x y := by
515 exact congrFun
517 (X := X) (Y := Y) coeff φ w) y
519/-- Abstract Fox chain rule, matrix form. -/
521 [Fintype X] [DecidableEq Y]
522 (coeff : FreeGroup Y →* S) (φ : FreeGroup X →* FreeGroup Y)
523 (w : FreeGroup X) :
525 Matrix.vecMul
530 (X := X) coeff φ
533omit [DecidableEq X] in
534/-- Abstract Fox-Jacobian chain rule, component form. -/
536 {Z : Type*} [Fintype Y] [DecidableEq Y] [DecidableEq Z]
537 (coeff : FreeGroup Z →* S)
538 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y)
539 (x : X) (z : Z) :
540 freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Z) coeff (φ.comp χ) x z =
541 ∑ y : Y,
542 freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Y) (coeff.comp φ) χ x y *
543 freeCrossedDifferentialWithCoeffJacobian (X := Y) (Y := Z) coeff φ y z := by
546 (X := Y) (Y := Z) coeff φ (χ (FreeGroup.of x)) z
548omit [DecidableEq X] in
549/-- Abstract Fox-Jacobian chain rule, family form. -/
551 {Z : Type*} [Fintype Y] [DecidableEq Y] [DecidableEq Z]
552 (coeff : FreeGroup Z →* S)
553 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
554 freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Z) coeff (φ.comp χ) =
555 fun x z =>
556 ∑ y : Y,
557 freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Y) (coeff.comp φ) χ x y *
558 freeCrossedDifferentialWithCoeffJacobian (X := Y) (Y := Z) coeff φ y z := by
559 funext x z
561 (X := X) (Y := Y) coeff φ χ x z
563omit [DecidableEq X] in
564/-- Abstract Fox-Jacobian chain rule, linear-map form. -/
566 {Z : Type*} [Fintype X] [Fintype Y] [DecidableEq Y] [DecidableEq Z]
567 (coeff : FreeGroup Z →* S)
568 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
569 (freeCrossedDifferentialWithCoeffJacobianLinearMap (X := Y) (Y := Z) coeff φ).comp
571 (X := X) (Y := Y) (coeff.comp φ) χ) =
573 (X := X) (Y := Z) coeff (φ.comp χ) := by
574 change
576 (freeCrossedDifferentialWithCoeffJacobian (X := Y) (Y := Z) coeff φ)).comp
578 (freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Y) (coeff.comp φ) χ)) =
580 (freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Z) coeff (φ.comp χ))
582 congr
583 funext x z
585 (X := X) (Y := Y) coeff φ χ x z).symm
587omit [DecidableEq X] in
588/-- Abstract Fox-Jacobian chain rule, matrix form. -/
590 {Z : Type*} [Fintype Y] [DecidableEq Y] [DecidableEq Z]
591 (coeff : FreeGroup Z →* S)
592 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
594 (X := X) (Y := Z) coeff (φ.comp χ) =
596 (X := X) (Y := Y) (coeff.comp φ) χ *
598 (X := Y) (Y := Z) coeff φ := by
599 apply Matrix.ext
600 intro x z
604end Coordinates
606end
608end FoxDifferential