Yamaguchi Lean 4 Library
FoxDifferential/Discrete/FoxCalculus/Derivative.lean
FoxDifferential/Discrete/FoxCalculus/Derivative/Source

FoxDifferential/Discrete/FoxCalculus/Derivative.lean

1import FoxDifferential.Discrete.FoxCalculus.Semidirect
2import FoxDifferential.Discrete.DifferentialModule.Universal
3import FoxDifferential.Common.FreeCrossedDifferential
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FoxDifferential/Discrete/FoxCalculus/Derivative.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Discrete group-ring Fox calculus
16Ordinary Fox derivatives over group rings are developed through augmentation, relative differential modules, coordinates, Jacobians, and chain rules.
17-/
18namespace FoxDifferential
20noncomputable section
22namespace FoxCalculus
24open scoped BigOperators
26universe u v
29variable {H : Type v} [Group H]
30variable (X : Type u)
32variable [DecidableEq X]
33variable (ψ : FreeGroup X →* H)
35/-- The semidirect-product lift whose left component is the Fox derivative pushed forward by
36`ψ`, and whose right component is `ψ` itself. -/
37def relativeFreeGroupFoxLift : FreeGroup X →* RelativeFoxSemidirect (H := H) X :=
38 FreeGroup.lift fun x =>
39 { left := Pi.single x (1 : GroupRing H)
40 right := ψ (FreeGroup.of x) }
42/-- The Fox derivative of a free-group word, with coefficients pushed forward to `ℤ[H]` by
43`ψ`. -/
44def relativeFreeGroupFoxDerivative (w : FreeGroup X) :
46 (relativeFreeGroupFoxLift (H := H) X ψ w).left
48/-- The right component of the relative Fox lift is the target homomorphism `ψ`. -/
49@[simp]
50theorem relativeFreeGroupFoxLift_right (w : FreeGroup X) :
51 (relativeFreeGroupFoxLift (H := H) X ψ w).right = ψ w := by
52 induction w using FreeGroup.induction_on with
53 | C1 =>
54 simp only [relativeFreeGroupFoxLift, map_one, RelativeFoxSemidirect.one_right]
55 | of x =>
56 simp only [relativeFreeGroupFoxLift, FreeGroup.lift_apply_of]
57 | inv_of x hx =>
58 simpa using congrArg Inv.inv hx
59 | mul x y hx hy =>
60 simp only [map_mul, RelativeFoxSemidirect.mul_right, hx, hy]
62/-- The relative Fox derivative of the identity word is zero. -/
63@[simp]
65 relativeFreeGroupFoxDerivative (H := H) X ψ (1 : FreeGroup X) = 0 := by
66 simp only [relativeFreeGroupFoxDerivative, relativeFreeGroupFoxLift, map_one, RelativeFoxSemidirect.one_left]
68/-- The relative Fox derivative of a free generator is the corresponding coordinate vector. -/
69@[simp]
71 relativeFreeGroupFoxDerivative (H := H) X ψ (FreeGroup.of x) =
72 Pi.single x (1 : GroupRing H) := by
73 simp only [relativeFreeGroupFoxDerivative, relativeFreeGroupFoxLift, FreeGroup.lift_apply_of]
75/-- Relative Fox product rule. -/
76theorem relativeFreeGroupFoxDerivative_mul (w₁ w₂ : FreeGroup X) :
77 relativeFreeGroupFoxDerivative (H := H) X ψ (w₁ * w₂) =
78 relativeFreeGroupFoxDerivative (H := H) X ψ w₁ +
79 (MonoidAlgebra.of ℤ H (ψ w₁) : GroupRing H) •
80 relativeFreeGroupFoxDerivative (H := H) X ψ w₂ := by
81 simp only [relativeFreeGroupFoxDerivative, map_mul, RelativeFoxSemidirect.mul_left,
82 relativeFreeGroupFoxLift_right, MonoidAlgebra.of_apply]
84/-- Relative Fox inverse rule. -/
85theorem relativeFreeGroupFoxDerivative_inv (w : FreeGroup X) :
86 relativeFreeGroupFoxDerivative (H := H) X ψ w⁻¹ =
87 -((MonoidAlgebra.of ℤ H (ψ w⁻¹) : GroupRing H) •
88 relativeFreeGroupFoxDerivative (H := H) X ψ w) := by
89 simp only [relativeFreeGroupFoxDerivative, map_inv, RelativeFoxSemidirect.inv_left,
90 relativeFreeGroupFoxLift_right, MonoidAlgebra.of_apply]
92/-- The relative free-group Fox derivative is a differential map for `ψ`. -/
95 (A := RelativeFreeFoxCoordinates (H := H) X)
96 ψ
97 (relativeFreeGroupFoxDerivative (H := H) X ψ) := by
98 intro w₁ w₂
99 simpa using relativeFreeGroupFoxDerivative_mul (H := H) X ψ w₁ w₂
101/-- Uniqueness of the relative free-group Fox derivative among differential maps with standard
102coordinate values on free generators. -/
104 (delta : FreeGroup X → RelativeFreeFoxCoordinates (H := H) X)
105 (hdelta : IsDifferentialMap (A := RelativeFreeFoxCoordinates (H := H) X) ψ delta)
106 (hbasis :
107 ∀ x : X, delta (FreeGroup.of x) =
108 Pi.single x (1 : GroupRing H)) :
109 delta = relativeFreeGroupFoxDerivative (H := H) X ψ := by
110 have hdelta_free :
111 delta =
114 (fun x : X => Pi.single x (1 : GroupRing H)) :=
117 (fun x : X => Pi.single x (1 : GroupRing H))
118 delta hdelta hbasis
119 have hrelative_free :
123 (fun x : X => Pi.single x (1 : GroupRing H)) :=
126 (fun x : X => Pi.single x (1 : GroupRing H))
130 exact hdelta_free.trans hrelative_free.symm
132/-- Relative Fox derivative of a positive power. -/
133theorem relativeFreeGroupFoxDerivative_pow (w : FreeGroup X) (n : ℕ) :
134 relativeFreeGroupFoxDerivative (H := H) X ψ (w ^ n) =
135 (Finset.range n).sum (fun k =>
136 (MonoidAlgebra.of ℤ H (ψ (w ^ k)) : GroupRing H) •
137 relativeFreeGroupFoxDerivative (H := H) X ψ w) := by
138 simpa [groupRingScalar] using
139 IsCrossedDifferential.pow
142/-- Relative Fox derivative of a conjugate. -/
143theorem relativeFreeGroupFoxDerivative_conj (g h : FreeGroup X) :
144 relativeFreeGroupFoxDerivative (H := H) X ψ (g * h * g⁻¹) =
146 (MonoidAlgebra.of ℤ H (ψ g) : GroupRing H) •
148 (MonoidAlgebra.of ℤ H (ψ (g * h * g⁻¹)) : GroupRing H) •
149 relativeFreeGroupFoxDerivative (H := H) X ψ g := by
150 simpa [groupRingScalar] using
151 IsCrossedDifferential.conj
154/-- Relative Fox derivative of a commutator. -/
155theorem relativeFreeGroupFoxDerivative_commutator (g h : FreeGroup X) :
156 relativeFreeGroupFoxDerivative (H := H) X ψ ⁅g, h⁆ =
158 (MonoidAlgebra.of ℤ H (ψ g) : GroupRing H) •
160 (MonoidAlgebra.of ℤ H (ψ (g * h * g⁻¹)) : GroupRing H) •
162 (MonoidAlgebra.of ℤ H (ψ ⁅g, h⁆) : GroupRing H) •
163 relativeFreeGroupFoxDerivative (H := H) X ψ h := by
164 simpa [groupRingScalar] using
165 IsCrossedDifferential.commutator
168end FoxCalculus
170end
172end FoxDifferential