Source: ProCGroups.FoxDifferential.Discrete.FoxCalculus.Derivative
1import ProCGroups.FoxDifferential.Discrete.FoxCalculus.Semidirect
2import ProCGroups.FoxDifferential.Discrete.DifferentialModule.Universal
3import ProCGroups.FoxDifferential.Common.FreeCrossedDifferential
5/-!
6# Fox differential: discrete — fox calculus — derivative
8The principal declarations in this module are:
10- `relativeFreeGroupFoxLift`
11 The semidirect-product lift whose left component is the Fox derivative pushed forward by \(\psi\),
12 and whose right component is \(\psi\) itself.
13- `relativeFreeGroupFoxDerivative`
14 The Fox derivative of a free-group word, with coefficients pushed forward to \(\mathbb{Z}[H]\) by
15 \(\psi\).
16- `relativeFreeGroupFoxLift_right`
17 The right component of the relative Fox lift is the target homomorphism \(\psi\).
18- `relativeFreeGroupFoxDerivative_one`
19 The relative Fox derivative of the identity word is zero.
20-/
22namespace FoxDifferential
24noncomputable section
26namespace FoxCalculus
28open scoped BigOperators commutatorElement
30universe u v
33variable {H : Type v} [Group H]
34variable (X : Type u)
36variable [DecidableEq X]
37variable (ψ : FreeGroup X →* H)
39/--
40The semidirect-product lift whose left component is the Fox derivative pushed forward by
41\(\psi\), and whose right component is \(\psi\) itself.
42-/
43def relativeFreeGroupFoxLift :
44 FreeGroup X →* CrossedSemidirectProduct (RelativeFoxAction (H := H) X) :=
45 FreeGroup.lift fun x =>
46 { left := Multiplicative.ofAdd (Pi.single x (1 : GroupRing H))
47 right := ψ (FreeGroup.of x) }
49/--
50The Fox derivative of a free-group word, with coefficients pushed forward to \(\mathbb{Z}[H]\)
51by \(\psi\).
52-/
53def relativeFreeGroupFoxDerivative (w : FreeGroup X) :
54 RelativeFreeFoxCoordinates (H := H) X :=
55 Multiplicative.toAdd (relativeFreeGroupFoxLift (H := H) X ψ w).left
57/-- The right component of the relative Fox lift is the target homomorphism \(\psi\). -/
58@[simp]
59theorem relativeFreeGroupFoxLift_right (w : FreeGroup X) :
60 (relativeFreeGroupFoxLift (H := H) X ψ w).right = ψ w := by
61 induction w using FreeGroup.induction_on with
62 | C1 =>
63 simp only [relativeFreeGroupFoxLift, map_one, SemidirectProduct.one_right]
64 | of x =>
65 simp only [relativeFreeGroupFoxLift, FreeGroup.lift_apply_of]
66 | inv_of x hx =>
67 simpa using congrArg Inv.inv hx
68 | mul x y hx hy =>
69 simp only [map_mul, SemidirectProduct.mul_right, hx, hy]
71/-- The relative Fox derivative of the identity word is zero. -/
72@[simp]
73theorem relativeFreeGroupFoxDerivative_one :
74 relativeFreeGroupFoxDerivative (H := H) X ψ (1 : FreeGroup X) = 0 := by
75 simp only [relativeFreeGroupFoxDerivative, relativeFreeGroupFoxLift, map_one,
76 SemidirectProduct.one_left, toAdd_one]
78/-- The relative Fox derivative of a free generator is the corresponding coordinate vector. -/
79@[simp]
80theorem relativeFreeGroupFoxDerivative_of (x : X) :
81 relativeFreeGroupFoxDerivative (H := H) X ψ (FreeGroup.of x) =
82 Pi.single x (1 : GroupRing H) := by
83 simp only [relativeFreeGroupFoxDerivative, relativeFreeGroupFoxLift,
84 FreeGroup.lift_apply_of, toAdd_ofAdd]
86/-- Relative Fox product rule. -/
87theorem relativeFreeGroupFoxDerivative_mul (w₁ w₂ : FreeGroup X) :
88 relativeFreeGroupFoxDerivative (H := H) X ψ (w₁ * w₂) =
89 relativeFreeGroupFoxDerivative (H := H) X ψ w₁ +
90 (MonoidAlgebra.of ℤ H (ψ w₁) : GroupRing H) •
91 relativeFreeGroupFoxDerivative (H := H) X ψ w₂ := by
92 simp only [relativeFreeGroupFoxDerivative, map_mul, SemidirectProduct.mul_left,
93 toAdd_mul, crossedSemidirectMulAction_toAdd, scalarCrossedAction_apply,
94 relativeFreeGroupFoxLift_right, groupRingScalar_apply, MonoidHom.id_apply]
96/-- The relative free-group Fox derivative is a differential map for \(\psi\). -/
97def relativeFreeGroupFoxHom :
98 DifferentialHom ψ (RelativeFreeFoxCoordinates (H := H) X) where
99 toFun := relativeFreeGroupFoxDerivative (H := H) X ψ
100 map_mul' := by
101 intro w₁ w₂
102 simpa only [scalarCrossedAction_apply, groupRingScalar_apply] using
103 relativeFreeGroupFoxDerivative_mul (H := H) X ψ w₁ w₂
105/-- The bundled relative Fox crossed homomorphism evaluates to the relative Fox
106derivative. -/
107@[simp]
108theorem relativeFreeGroupFoxHom_apply (w : FreeGroup X) :
109 relativeFreeGroupFoxHom (H := H) X ψ w =
110 relativeFreeGroupFoxDerivative (H := H) X ψ w :=
111 rfl
113/-- The relative Fox derivative satisfies the inverse rule. -/
114theorem relativeFreeGroupFoxDerivative_inv (w : FreeGroup X) :
115 relativeFreeGroupFoxDerivative (H := H) X ψ w⁻¹ =
116 -((MonoidAlgebra.of ℤ H (ψ w⁻¹) : GroupRing H) •
117 relativeFreeGroupFoxDerivative (H := H) X ψ w) := by
118 simpa only [groupRingScalar_apply, relativeFreeGroupFoxHom_apply] using
119 ScalarCrossedHom.map_inv (relativeFreeGroupFoxHom (H := H) X ψ) w
121/--
122Uniqueness of the relative free-group Fox derivative among differential maps with standard
123coordinate values on free generators.
124-/
125theorem relativeFreeGroupFoxHom_unique
126 (delta : DifferentialHom ψ (RelativeFreeFoxCoordinates (H := H) X))
127 (hbasis :
128 ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : GroupRing H)) :
129 delta = relativeFreeGroupFoxHom (H := H) X ψ := by
130 have hdelta_free :=
131 freeCrossedHomWithCoeff_unique
132 (A := RelativeFreeFoxCoordinates (H := H) X) (groupRingScalar ψ)
133 (fun x : X => Pi.single x (1 : GroupRing H)) delta hbasis
134 have hrelative_free :=
135 freeCrossedHomWithCoeff_unique
136 (A := RelativeFreeFoxCoordinates (H := H) X) (groupRingScalar ψ)
137 (fun x : X => Pi.single x (1 : GroupRing H))
138 (relativeFreeGroupFoxHom (H := H) X ψ)
139 (relativeFreeGroupFoxDerivative_of (H := H) X ψ)
140 exact hdelta_free.trans hrelative_free.symm
142/-- Relative Fox derivative of a positive power. -/
143theorem relativeFreeGroupFoxDerivative_pow (w : FreeGroup X) (n : ℕ) :
144 relativeFreeGroupFoxDerivative (H := H) X ψ (w ^ n) =
145 (Finset.range n).sum (fun k =>
146 (MonoidAlgebra.of ℤ H (ψ (w ^ k)) : GroupRing H) •
147 relativeFreeGroupFoxDerivative (H := H) X ψ w) := by
148 simpa only [relativeFreeGroupFoxHom_apply, groupRingScalar_apply, map_pow] using
149 ScalarCrossedHom.map_pow (relativeFreeGroupFoxHom (H := H) X ψ) w n
151/-- Relative Fox derivative of a conjugate. -/
152theorem relativeFreeGroupFoxDerivative_conj (g h : FreeGroup X) :
153 relativeFreeGroupFoxDerivative (H := H) X ψ (g * h * g⁻¹) =
154 relativeFreeGroupFoxDerivative (H := H) X ψ g +
155 (MonoidAlgebra.of ℤ H (ψ g) : GroupRing H) •
156 relativeFreeGroupFoxDerivative (H := H) X ψ h -
157 (MonoidAlgebra.of ℤ H (ψ (g * h * g⁻¹)) : GroupRing H) •
158 relativeFreeGroupFoxDerivative (H := H) X ψ g := by
159 simpa only [relativeFreeGroupFoxHom_apply, groupRingScalar_apply] using
160 ScalarCrossedHom.map_conj
161 (coeff := groupRingScalar ψ) (relativeFreeGroupFoxHom (H := H) X ψ) g h
163/-- Relative Fox derivative of a commutator. -/
164theorem relativeFreeGroupFoxDerivative_commutator (g h : FreeGroup X) :
165 relativeFreeGroupFoxDerivative (H := H) X ψ ⁅g, h⁆ =
166 relativeFreeGroupFoxDerivative (H := H) X ψ g +
167 (MonoidAlgebra.of ℤ H (ψ g) : GroupRing H) •
168 relativeFreeGroupFoxDerivative (H := H) X ψ h -
169 (MonoidAlgebra.of ℤ H (ψ (g * h * g⁻¹)) : GroupRing H) •
170 relativeFreeGroupFoxDerivative (H := H) X ψ g -
171 (MonoidAlgebra.of ℤ H (ψ ⁅g, h⁆) : GroupRing H) •
172 relativeFreeGroupFoxDerivative (H := H) X ψ h := by
173 simpa only [relativeFreeGroupFoxHom_apply, groupRingScalar_apply] using
174 ScalarCrossedHom.map_commutator (relativeFreeGroupFoxHom (H := H) X ψ) g h
176end FoxCalculus
178end
180end FoxDifferential