FoxDifferential/Discrete/Absolute.lean
1import FoxDifferential.Discrete.Naturality
2import FoxDifferential.Discrete.FoxCalculus.Boundary
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Discrete/Absolute.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Discrete group-ring Fox calculus
15Ordinary Fox derivatives over group rings are developed through augmentation, relative differential modules, coordinates, Jacobians, and chain rules.
16-/
17namespace FoxDifferential
19noncomputable section
21namespace FoxCalculus
23open scoped BigOperators
25universe u v
27variable {X : Type u} [DecidableEq X]
29/-- The absolute Fox derivative of a free-group word, with coefficients in `ℤ[FreeGroup X]`. -/
30def freeGroupFoxDerivative (w : FreeGroup X) :
31 RelativeFreeFoxCoordinates (H := FreeGroup X) X :=
32 relativeFreeGroupFoxDerivative (H := FreeGroup X) X
33 (MonoidHom.id (FreeGroup X)) w
35/-- The absolute Fox derivative of the identity word is zero. -/
36@[simp]
37theorem freeGroupFoxDerivative_one :
38 freeGroupFoxDerivative (X := X) (1 : FreeGroup X) = 0 := by
39 simp only [freeGroupFoxDerivative, relativeFreeGroupFoxDerivative_one]
41/-- The absolute Fox derivative of a free generator is the corresponding coordinate vector. -/
42@[simp]
43theorem freeGroupFoxDerivative_of (x : X) :
44 freeGroupFoxDerivative (X := X) (FreeGroup.of x) =
46 simp only [freeGroupFoxDerivative, relativeFreeGroupFoxDerivative_of]
48/-- Product rule for the absolute Fox derivative. -/
49theorem freeGroupFoxDerivative_mul (u v : FreeGroup X) :
50 freeGroupFoxDerivative (X := X) (u * v) =
51 freeGroupFoxDerivative (X := X) u +
53 freeGroupFoxDerivative (X := X) v := by
54 simpa [freeGroupFoxDerivative] using
55 relativeFreeGroupFoxDerivative_mul (H := FreeGroup X) X
56 (MonoidHom.id (FreeGroup X)) u v
58/-- Inverse rule for the absolute Fox derivative. -/
59theorem freeGroupFoxDerivative_inv (w : FreeGroup X) :
60 freeGroupFoxDerivative (X := X) w⁻¹ =
62 freeGroupFoxDerivative (X := X) w) := by
63 simpa [freeGroupFoxDerivative] using
64 relativeFreeGroupFoxDerivative_inv (H := FreeGroup X) X
65 (MonoidHom.id (FreeGroup X)) w
67/-- Positive-power rule for the absolute Fox derivative. -/
68theorem freeGroupFoxDerivative_pow (w : FreeGroup X) (n : ℕ) :
69 freeGroupFoxDerivative (X := X) (w ^ n) =
70 (Finset.range n).sum (fun k =>
72 freeGroupFoxDerivative (X := X) w) := by
73 simpa [freeGroupFoxDerivative] using
74 relativeFreeGroupFoxDerivative_pow (H := FreeGroup X) X
75 (MonoidHom.id (FreeGroup X)) w n
77/-- Conjugation rule for the absolute Fox derivative. -/
78theorem freeGroupFoxDerivative_conj (g h : FreeGroup X) :
79 freeGroupFoxDerivative (X := X) (g * h * g⁻¹) =
80 freeGroupFoxDerivative (X := X) g +
82 freeGroupFoxDerivative (X := X) h -
83 (MonoidAlgebra.of ℤ (FreeGroup X) (g * h * g⁻¹) :
85 freeGroupFoxDerivative (X := X) g := by
86 simpa [freeGroupFoxDerivative] using
87 relativeFreeGroupFoxDerivative_conj (H := FreeGroup X) X
88 (MonoidHom.id (FreeGroup X)) g h
90/-- Commutator rule for the absolute Fox derivative. -/
91theorem freeGroupFoxDerivative_commutator (g h : FreeGroup X) :
92 freeGroupFoxDerivative (X := X) ⁅g, h⁆ =
93 freeGroupFoxDerivative (X := X) g +
95 freeGroupFoxDerivative (X := X) h -
96 (MonoidAlgebra.of ℤ (FreeGroup X) (g * h * g⁻¹) :
98 freeGroupFoxDerivative (X := X) g -
100 freeGroupFoxDerivative (X := X) h := by
101 simpa [freeGroupFoxDerivative] using
102 relativeFreeGroupFoxDerivative_commutator (H := FreeGroup X) X
103 (MonoidHom.id (FreeGroup X)) g h
105variable [Fintype X]
107/-- Absolute Fox--Euler formula. -/
108theorem freeGroupFoxDerivative_euler_formula (w : FreeGroup X) :
110 ∑ x : X,
111 freeGroupFoxDerivative (X := X) w x *
112 augmentationGenerator (FreeGroup X) (FreeGroup.of x) := by
113 simpa [freeGroupFoxDerivative] using
114 relativeFreeGroupFoxDerivative_euler_formula (H := FreeGroup X) X
115 (MonoidHom.id (FreeGroup X)) w
117variable {H : Type v} [Group H]
119omit [Fintype X] in
120/-- Relative Fox derivatives are obtained from the absolute derivative by pushing coefficients
121forward along `ψ`. -/
123 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
124 relativeFreeGroupFoxDerivative (H := H) X ψ w =
125 relativeFreeFoxCoordinatesMap (X := X) ψ
126 (freeGroupFoxDerivative (X := X) w) := by
127 simpa [freeGroupFoxDerivative] using
129 (H := FreeGroup X) (K := H) (X := X)
130 (MonoidHom.id (FreeGroup X)) ψ w
132omit [Fintype X] in
133/-- Component form of the absolute-to-relative comparison. -/
135 (ψ : FreeGroup X →* H) (w : FreeGroup X) (x : X) :
136 relativeFreeGroupFoxDerivative (H := H) X ψ w x =
137 groupRingMap ψ (freeGroupFoxDerivative (X := X) w x) := by
138 have h := congrFun
140 (H := H) (X := X) ψ w) x
141 simpa [relativeFreeFoxCoordinatesMap] using h
143end FoxCalculus
145end
147end FoxDifferential