Source: ProCGroups.FoxDifferential.Discrete.Absolute
1import ProCGroups.FoxDifferential.Discrete.Naturality
2import ProCGroups.FoxDifferential.Discrete.FoxCalculus.Boundary
4/-!
5# Fox differential: discrete — absolute
7The principal declarations in this module are:
9- `freeGroupFoxDerivative`
10 The absolute Fox derivative of a free-group word, with coefficients in
11 \(\mathbb{Z}[\mathrm{FreeGroup}(X)]\).
12- `freeGroupFoxDerivative_one`
13 The absolute Fox derivative of the identity word is zero.
14- `freeGroupFoxDerivative_of`
15 The absolute Fox derivative of a free generator is the corresponding coordinate vector.
16- `freeGroupFoxDerivative_mul`
17 Product rule for the absolute Fox derivative.
18-/
20namespace FoxDifferential
22noncomputable section
24namespace FoxCalculus
26open scoped BigOperators commutatorElement
28universe u v
30variable {X : Type u} [DecidableEq X]
32/--
33The absolute Fox derivative of a free-group word, with coefficients in
34\(\mathbb{Z}[\mathrm{FreeGroup}(X)]\).
35-/
36def freeGroupFoxDerivative (w : FreeGroup X) :
37 RelativeFreeFoxCoordinates (H := FreeGroup X) X :=
38 relativeFreeGroupFoxDerivative (H := FreeGroup X) X
39 (MonoidHom.id (FreeGroup X)) w
41/-- The absolute Fox derivative of the identity word is zero. -/
42@[simp]
43theorem freeGroupFoxDerivative_one :
44 freeGroupFoxDerivative (X := X) (1 : FreeGroup X) = 0 := by
45 simp only [freeGroupFoxDerivative, relativeFreeGroupFoxDerivative_one]
47/-- The absolute Fox derivative of a free generator is the corresponding coordinate vector. -/
48@[simp]
49theorem freeGroupFoxDerivative_of (x : X) :
50 freeGroupFoxDerivative (X := X) (FreeGroup.of x) =
51 Pi.single x (1 : GroupRing (FreeGroup X)) := by
52 simp only [freeGroupFoxDerivative, relativeFreeGroupFoxDerivative_of]
54/-- Product rule for the absolute Fox derivative. -/
55theorem freeGroupFoxDerivative_mul (u v : FreeGroup X) :
56 freeGroupFoxDerivative (X := X) (u * v) =
57 freeGroupFoxDerivative (X := X) u +
58 (MonoidAlgebra.of ℤ (FreeGroup X) u : GroupRing (FreeGroup X)) •
59 freeGroupFoxDerivative (X := X) v := by
60 simpa [freeGroupFoxDerivative] using
61 relativeFreeGroupFoxDerivative_mul (H := FreeGroup X) X
62 (MonoidHom.id (FreeGroup X)) u v
64/-- Inverse rule for the absolute Fox derivative. -/
65theorem freeGroupFoxDerivative_inv (w : FreeGroup X) :
66 freeGroupFoxDerivative (X := X) w⁻¹ =
67 -((MonoidAlgebra.of ℤ (FreeGroup X) w⁻¹ : GroupRing (FreeGroup X)) •
68 freeGroupFoxDerivative (X := X) w) := by
69 simpa [freeGroupFoxDerivative] using
70 relativeFreeGroupFoxDerivative_inv (H := FreeGroup X) X
71 (MonoidHom.id (FreeGroup X)) w
73/-- Positive-power rule for the absolute Fox derivative. -/
74theorem freeGroupFoxDerivative_pow (w : FreeGroup X) (n : ℕ) :
75 freeGroupFoxDerivative (X := X) (w ^ n) =
76 (Finset.range n).sum (fun k =>
77 (MonoidAlgebra.of ℤ (FreeGroup X) (w ^ k) : GroupRing (FreeGroup X)) •
78 freeGroupFoxDerivative (X := X) w) := by
79 simpa [freeGroupFoxDerivative] using
80 relativeFreeGroupFoxDerivative_pow (H := FreeGroup X) X
81 (MonoidHom.id (FreeGroup X)) w n
83/-- Conjugation rule for the absolute Fox derivative. -/
84theorem freeGroupFoxDerivative_conj (g h : FreeGroup X) :
85 freeGroupFoxDerivative (X := X) (g * h * g⁻¹) =
86 freeGroupFoxDerivative (X := X) g +
87 (MonoidAlgebra.of ℤ (FreeGroup X) g : GroupRing (FreeGroup X)) •
88 freeGroupFoxDerivative (X := X) h -
89 (MonoidAlgebra.of ℤ (FreeGroup X) (g * h * g⁻¹) :
90 GroupRing (FreeGroup X)) •
91 freeGroupFoxDerivative (X := X) g := by
92 simpa [freeGroupFoxDerivative] using
93 relativeFreeGroupFoxDerivative_conj (H := FreeGroup X) X
94 (MonoidHom.id (FreeGroup X)) g h
96/-- Commutator rule for the absolute Fox derivative. -/
97theorem freeGroupFoxDerivative_commutator (g h : FreeGroup X) :
98 freeGroupFoxDerivative (X := X) ⁅g, h⁆ =
99 freeGroupFoxDerivative (X := X) g +
100 (MonoidAlgebra.of ℤ (FreeGroup X) g : GroupRing (FreeGroup X)) •
101 freeGroupFoxDerivative (X := X) h -
102 (MonoidAlgebra.of ℤ (FreeGroup X) (g * h * g⁻¹) :
103 GroupRing (FreeGroup X)) •
104 freeGroupFoxDerivative (X := X) g -
105 (MonoidAlgebra.of ℤ (FreeGroup X) ⁅g, h⁆ : GroupRing (FreeGroup X)) •
106 freeGroupFoxDerivative (X := X) h := by
107 simpa [freeGroupFoxDerivative] using
108 relativeFreeGroupFoxDerivative_commutator (H := FreeGroup X) X
109 (MonoidHom.id (FreeGroup X)) g h
111variable [Fintype X]
113/--
114The Euler formula for the free-group Fox derivative expresses a word as the augmentation term
115plus the sum of generator derivatives.
116-/
117theorem freeGroupFoxDerivative_euler_formula (w : FreeGroup X) :
118 (MonoidAlgebra.of ℤ (FreeGroup X) w : GroupRing (FreeGroup X)) - 1 =
119 ∑ x : X,
120 freeGroupFoxDerivative (X := X) w x *
121 augmentationGenerator (FreeGroup X) (FreeGroup.of x) := by
122 simpa [freeGroupFoxDerivative] using
123 relativeFreeGroupFoxDerivative_euler_formula (H := FreeGroup X) X
124 (MonoidHom.id (FreeGroup X)) w
126variable {H : Type v} [Group H]
128omit [Fintype X] in
129/--
130Relative Fox derivatives are obtained from the absolute derivative by pushing coefficients
131forward along \(\psi\).
132-/
133theorem relativeFreeGroupFoxDerivative_eq_map_freeGroupFoxDerivative
134 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
135 relativeFreeGroupFoxDerivative (H := H) X ψ w =
136 relativeFreeFoxCoordinatesMap (X := X) ψ
137 (freeGroupFoxDerivative (X := X) w) := by
138 simpa [freeGroupFoxDerivative] using
139 relativeFreeGroupFoxDerivative_mapDomain
140 (H := FreeGroup X) (K := H) (X := X)
141 (MonoidHom.id (FreeGroup X)) ψ w
143omit [Fintype X] in
144/--
145Component form of the absolute-to-relative comparison: each relative Fox derivative coordinate
146is the group-ring image of the absolute coordinate.
147-/
148theorem relativeFreeGroupFoxDerivative_eq_map_freeGroupFoxDerivative_apply
149 (ψ : FreeGroup X →* H) (w : FreeGroup X) (x : X) :
150 relativeFreeGroupFoxDerivative (H := H) X ψ w x =
151 groupRingMap ψ (freeGroupFoxDerivative (X := X) w x) := by
152 have h := congrFun
153 (relativeFreeGroupFoxDerivative_eq_map_freeGroupFoxDerivative
154 (H := H) (X := X) ψ w) x
155 simpa [relativeFreeFoxCoordinatesMap] using h
157end FoxCalculus
159end
161end FoxDifferential