Yamaguchi Lean 4 Library
FoxDifferential/Discrete/Jacobian/ChainRule.lean
FoxDifferential/Discrete/Jacobian/ChainRule/Source

FoxDifferential/Discrete/Jacobian/ChainRule.lean

1import FoxDifferential.Discrete.Jacobian.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Discrete/Jacobian/ChainRule.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}
28/-- The composed derivative `w |-> D(φ w)` is a crossed differential. -/
30 [DecidableEq Y]
31 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
33 (A := Y → GroupRing H) (ψ.comp φ)
34 (fun w : FreeGroup X =>
35 relativeFreeGroupFoxDerivative (H := H) Y ψ (φ w)) := by
36 intro u v
37 funext y
38 simp only [map_mul, relativeFreeGroupFoxDerivative_mul, MonoidAlgebra.of_apply, Pi.add_apply, Pi.smul_apply,
39 smul_eq_mul, groupRingScalar, MonoidHom.coe_comp, Function.comp_apply]
41/-- Fox chain rule for homomorphisms between free groups, component form. -/
43 [DecidableEq X] [Fintype X] [DecidableEq Y]
44 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
45 (w : FreeGroup X) (y : Y) :
46 relativeFreeGroupFoxDerivative (H := H) Y ψ (φ w) y =
47 ∑ x : X,
48 relativeFreeGroupFoxDerivative (H := H) X (ψ.comp φ) w x *
49 freeGroupHomFoxJacobian (H := H) ψ φ x y := by
50 have h :=
52 (H := H) (A := Y → GroupRing H) (X := X) (Y := Y)
53 ψ φ (relativeFreeGroupFoxDerivative (H := H) Y ψ)
55 have hy := congrFun h y
56 simpa [freeGroupHomFoxJacobian, Finset.sum_apply, Pi.smul_apply, smul_eq_mul] using hy
58/-- Fox chain rule for homomorphisms between free groups, vector form. -/
60 [DecidableEq X] [Fintype X] [DecidableEq Y]
61 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
62 (w : FreeGroup X) :
63 relativeFreeGroupFoxDerivative (H := H) Y ψ (φ w) =
64 fun y : Y =>
65 ∑ x : X,
66 relativeFreeGroupFoxDerivative (H := H) X (ψ.comp φ) w x *
67 freeGroupHomFoxJacobian (H := H) ψ φ x y := by
68 funext y
71/-- The relative Fox Jacobian of the identity homomorphism is the coordinate identity family. -/
72@[simp]
74 [DecidableEq X]
75 (ψ : FreeGroup X →* H) :
76 freeGroupHomFoxJacobian (H := H) ψ (MonoidHom.id (FreeGroup X)) =
77 fun x : X => Pi.single x (1 : GroupRing H) := by
78 funext x y
81variable {Z : Type z}
83/-- Fox Jacobian chain rule for homomorphisms between free groups, component form. -/
85 [DecidableEq Y] [Fintype Y] [DecidableEq Z]
86 (ψ : FreeGroup Z →* H)
87 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y)
88 (x : X) (z : Z) :
89 freeGroupHomFoxJacobian (H := H) ψ (φ.comp χ) x z =
90 ∑ y : Y,
91 freeGroupHomFoxJacobian (H := H) (ψ.comp φ) χ x y *
92 freeGroupHomFoxJacobian (H := H) ψ φ y z := by
94 relativeFreeGroupFoxDerivative_comp_apply (H := H) ψ φ (χ (FreeGroup.of x)) z
96/-- Fox Jacobian chain rule for homomorphisms between free groups, matrix form. -/
98 [DecidableEq Y] [Fintype Y] [DecidableEq Z]
99 (ψ : FreeGroup Z →* H)
100 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
101 freeGroupHomFoxJacobian (H := H) ψ (φ.comp χ) =
102 fun x z =>
103 ∑ y : Y,
104 freeGroupHomFoxJacobian (H := H) (ψ.comp φ) χ x y *
105 freeGroupHomFoxJacobian (H := H) ψ φ y z := by
106 funext x z
107 exact freeGroupHomFoxJacobian_comp_apply (H := H) ψ φ χ x z
109/-- The relative Fox Jacobian matrix of the identity homomorphism is the identity matrix. -/
110@[simp]
112 [DecidableEq X]
113 (ψ : FreeGroup X →* H) :
114 freeGroupHomFoxJacobianMatrix (H := H) ψ (MonoidHom.id (FreeGroup X)) =
115 (1 : Matrix X X (GroupRing H)) := by
116 apply Matrix.ext
117 intro x y
118 change freeGroupHomFoxJacobian (H := H) ψ (MonoidHom.id (FreeGroup X)) x y =
119 (1 : Matrix X X (GroupRing H)) x y
120 rw [show
121 freeGroupHomFoxJacobian (H := H) ψ (MonoidHom.id (FreeGroup X)) x y =
122 (Pi.single x (1 : GroupRing H) : X → GroupRing H) y from
123 congrFun (congrFun (freeGroupHomFoxJacobian_id (H := H) ψ) x) y]
124 by_cases hxy : x = y
125 · subst y
126 simp only [Pi.single_eq_same, Matrix.one_apply_eq]
127 · simp only [ne_eq, hxy, not_false_eq_true, Pi.single_eq_of_ne', Matrix.one_apply_ne]
129/-- Fox Jacobian chain rule, packaged as matrix multiplication. -/
131 [DecidableEq Y] [Fintype Y] [DecidableEq Z]
132 (ψ : FreeGroup Z →* H)
133 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
134 freeGroupHomFoxJacobianMatrix (H := H) ψ (φ.comp χ) =
135 freeGroupHomFoxJacobianMatrix (H := H) (ψ.comp φ) χ *
136 freeGroupHomFoxJacobianMatrix (H := H) ψ φ := by
137 apply Matrix.ext
138 intro x z
141/-- Absolute Fox Jacobian chain rule, component form. -/
143 [DecidableEq Y] [Fintype Y] [DecidableEq Z]
144 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y)
145 (x : X) (z : Z) :
147 ∑ y : Y,
150 calc
152 ∑ y : Y,
153 freeGroupHomFoxJacobian (H := FreeGroup Z) φ χ x y *
157 (H := FreeGroup Z)
158 (X := X) (Y := Y) (Z := Z)
159 (MonoidHom.id (FreeGroup Z)) φ χ x z
160 _ =
161 ∑ y : Y,
164 apply Finset.sum_congr rfl
165 intro y _
166 rw [freeGroupHomFoxJacobian_eq_map_absolute_apply (H := FreeGroup Z) φ χ x y]
168/-- Absolute Fox Jacobian chain rule, matrix form. -/
170 [DecidableEq Y] [Fintype Y] [DecidableEq Z]
171 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
175 apply Matrix.ext
176 intro x z
178 Matrix.mul_apply, Matrix.map_apply]
181end FoxCalculus
183end
185end FoxDifferential