FoxDifferential/Completed/ProCIntegerCoefficients/FreeGroup/Derivative.lean
1import FoxDifferential.Common.FreeCrossedDifferential
2import FoxDifferential.Completed.ProCIntegerCoefficients.Core
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/ProCIntegerCoefficients/FreeGroup/Derivative.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Completed group algebra coefficients
15This module gives the free-group formulas for pro-\(C\) integer coefficients, used to compare completed Fox derivatives with ordinary finite-stage derivatives.
16-/
17namespace FoxDifferential
19noncomputable section
21open scoped BigOperators
23universe u v
26variable (C : ProCGroups.FiniteGroupClass.{v})
27variable {X : Type u} [DecidableEq X]
28variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
30omit [DecidableEq X] in
31/-- Completed Fox-coordinate vectors with coefficients in `Z_C[[H]]`. -/
32abbrev ZCFreeFoxCoordinates : Type (max u v) :=
33 X → ZCCompletedGroupAlgebra C H
35/-- Completed free-group Fox derivative vector, with coefficients pushed forward along
36`ψ : FreeGroup X ->* H`. -/
37def zcFreeGroupFoxDerivativeVector (ψ : FreeGroup X →* H) (w : FreeGroup X) :
38 ZCFreeFoxCoordinates C (X := X) (H := H) :=
40 (A := ZCFreeFoxCoordinates C (X := X) (H := H))
42 (fun x => Pi.single x (1 : ZCCompletedGroupAlgebra C H))
43 w
45/-- A coordinate of the completed free-group Fox derivative. -/
46def zcFreeGroupFoxDerivative (ψ : FreeGroup X →* H) (i : X)
47 (w : FreeGroup X) : ZCCompletedGroupAlgebra C H :=
48 zcFreeGroupFoxDerivativeVector C ψ w i
50/-- The completed free-group derivative vector sends the identity word to zero. -/
51@[simp]
52theorem zcFreeGroupFoxDerivativeVector_one (ψ : FreeGroup X →* H) :
53 zcFreeGroupFoxDerivativeVector C ψ (1 : FreeGroup X) = 0 := by
56/-- The completed free-group derivative vector sends a free generator to the corresponding
57coordinate basis vector. -/
58@[simp]
59theorem zcFreeGroupFoxDerivativeVector_of (ψ : FreeGroup X →* H) (x : X) :
60 zcFreeGroupFoxDerivativeVector C ψ (FreeGroup.of x) =
61 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
64/-- Product rule for the completed free-group derivative vector. -/
66 (ψ : FreeGroup X →* H) (u v : FreeGroup X) :
67 zcFreeGroupFoxDerivativeVector C ψ (u * v) =
68 zcFreeGroupFoxDerivativeVector C ψ u +
69 zcCompletedGroupAlgebraScalar C ψ u • zcFreeGroupFoxDerivativeVector C ψ v := by
71 (A := ZCFreeFoxCoordinates C (X := X) (H := H))
73 (fun x => Pi.single x (1 : ZCCompletedGroupAlgebra C H)) u v
75/-- The completed free-group derivative vector is a crossed differential. -/
77 (ψ : FreeGroup X →* H) :
79 (zcCompletedGroupAlgebraScalar C ψ) (zcFreeGroupFoxDerivativeVector C ψ) := by
81 (A := ZCFreeFoxCoordinates C (X := X) (H := H))
83 (fun x => Pi.single x (1 : ZCCompletedGroupAlgebra C H))
85/-- The coefficient-generic coordinate crossed differential specializes to the completed
86free-group Fox derivative vector. -/
88 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
90 (X := X) (zcCompletedGroupAlgebraScalar C ψ) w =
91 zcFreeGroupFoxDerivativeVector C ψ w :=
92 rfl
94section AbstractChainRule
96variable {Y : Type u}
97variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]
98variable [Fintype X]
100/-- Completed `Z_C[[H]]` abstract Fox chain rule for an arbitrary crossed differential. -/
102 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
103 (delta : FreeGroup Y → A)
104 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
105 (w : FreeGroup X) :
106 delta (φ w) =
107 ∑ x : X,
108 zcFreeGroupFoxDerivative C (ψ.comp φ) x w •
109 delta (φ (FreeGroup.of x)) := by
110 calc
111 delta (φ w) =
113 (X := X) (zcCompletedGroupAlgebraScalar C (ψ.comp φ))
114 (fun x : X => delta (φ (FreeGroup.of x))) w := by
116 (X := X) (Y := Y) (B := A)
117 (zcCompletedGroupAlgebraScalar C ψ) φ delta hdelta w
118 _ =
119 ∑ x : X,
120 zcFreeGroupFoxDerivative C (ψ.comp φ) x w •
121 delta (φ (FreeGroup.of x)) := by
125 C (ψ.comp φ) w]
126 rfl
128end AbstractChainRule
130section Jacobian
132variable {Y : Type u} [DecidableEq Y]
134/-- Completed `Z_C[[H]]` Fox-Jacobian of a homomorphism of free groups. -/
136 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
137 X → Y → ZCCompletedGroupAlgebra C H :=
139 (X := X) (Y := Y) (zcCompletedGroupAlgebraScalar C ψ) φ
141omit [DecidableEq X] in
142/-- Evaluation of the completed `Z_C[[H]]` Fox-Jacobian. -/
143@[simp]
145 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
146 (x : X) (y : Y) :
147 zcFreeGroupHomFoxJacobian C ψ φ x y =
148 zcFreeGroupFoxDerivative C ψ y (φ (FreeGroup.of x)) :=
149 rfl
151/-- The completed `Z_C[[H]]` Fox-Jacobian as a matrix. -/
153 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
154 Matrix X Y (ZCCompletedGroupAlgebra C H) :=
156 (X := X) (Y := Y) (zcCompletedGroupAlgebraScalar C ψ) φ
158omit [DecidableEq X] in
159/-- Matrix evaluation is componentwise the completed `Z_C[[H]]` Fox-Jacobian. -/
160@[simp]
162 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
163 (x : X) (y : Y) :
164 zcFreeGroupHomFoxJacobianMatrix C ψ φ x y =
165 zcFreeGroupHomFoxJacobian C ψ φ x y :=
166 rfl
168/-- The completed `Z_C[[H]]` Fox-Jacobian as a finite linear map on coordinate vectors. -/
170 [Fintype X]
171 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
172 ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
173 ZCFreeFoxCoordinates C (X := Y) (H := H) :=
175 (X := X) (Y := Y) (zcCompletedGroupAlgebraScalar C ψ) φ
177omit [DecidableEq X] in
178/-- Evaluation formula for the completed `Z_C[[H]]` Fox-Jacobian linear map. -/
179@[simp]
181 [Fintype X]
182 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
183 (v : ZCFreeFoxCoordinates C (X := X) (H := H)) (y : Y) :
184 zcFreeGroupHomFoxJacobianLinearMap C ψ φ v y =
185 ∑ x : X, v x * zcFreeGroupHomFoxJacobian C ψ φ x y :=
186 rfl
188omit [DecidableEq X] in
189/-- The completed `Z_C[[H]]` Fox-Jacobian linear map is row-vector multiplication by its
190matrix. -/
192 [Fintype X]
193 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
194 (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
195 zcFreeGroupHomFoxJacobianLinearMap C ψ φ v =
196 Matrix.vecMul v (zcFreeGroupHomFoxJacobianMatrix C ψ φ) := by
198 (X := X) (Y := Y) (zcCompletedGroupAlgebraScalar C ψ) φ v
200/-- The completed `Z_C[[H]]` Fox-Jacobian of the identity homomorphism is the identity
201family. -/
202@[simp]
203theorem zcFreeGroupHomFoxJacobian_id (ψ : FreeGroup X →* H) :
204 zcFreeGroupHomFoxJacobian C ψ (MonoidHom.id (FreeGroup X)) =
205 foxJacobianId (R := ZCCompletedGroupAlgebra C H) (X := X) := by
206 simp only [zcFreeGroupHomFoxJacobian,
207 freeCrossedDifferentialWithCoeffJacobian_id (X := X) (S := ZCCompletedGroupAlgebra C H)
208 (zcCompletedGroupAlgebraScalar C ψ)]
210/-- The completed `Z_C[[H]]` Fox-Jacobian matrix of the identity homomorphism is the identity
211matrix. -/
212@[simp]
213theorem zcFreeGroupHomFoxJacobianMatrix_id (ψ : FreeGroup X →* H) :
214 zcFreeGroupHomFoxJacobianMatrix C ψ (MonoidHom.id (FreeGroup X)) =
215 (1 : Matrix X X (ZCCompletedGroupAlgebra C H)) := by
216 simp only [zcFreeGroupHomFoxJacobianMatrix,
217 freeCrossedDifferentialWithCoeffJacobianMatrix_id (X := X) (S := ZCCompletedGroupAlgebra C H)
218 (zcCompletedGroupAlgebraScalar C ψ)]
220/-- The completed `Z_C[[H]]` Fox-Jacobian linear map of the identity homomorphism is the
221identity. -/
222@[simp]
224 [Fintype X] (ψ : FreeGroup X →* H) :
225 zcFreeGroupHomFoxJacobianLinearMap C ψ (MonoidHom.id (FreeGroup X)) =
226 (LinearMap.id :
227 ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
228 ZCFreeFoxCoordinates C (X := X) (H := H)) := by
229 simp only [zcFreeGroupHomFoxJacobianLinearMap,
230 freeCrossedDifferentialWithCoeffJacobianLinearMap_id (X := X) (S := ZCCompletedGroupAlgebra C H)
231 (zcCompletedGroupAlgebraScalar C ψ)]
233/-- Completed `Z_C[[H]]` Fox chain rule, vector form. -/
235 [Fintype X]
236 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
237 (w : FreeGroup X) :
238 zcFreeGroupFoxDerivativeVector C ψ (φ w) =
240 (zcFreeGroupFoxDerivativeVector C (ψ.comp φ) w) := by
242 zcFreeGroupHomFoxJacobian] using
244 (X := X) (Y := Y) (zcCompletedGroupAlgebraScalar C ψ) φ w
246/-- Completed `Z_C[[H]]` Fox chain rule, component form. -/
248 [Fintype X]
249 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
250 (w : FreeGroup X) (y : Y) :
251 zcFreeGroupFoxDerivativeVector C ψ (φ w) y =
252 ∑ x : X,
253 zcFreeGroupFoxDerivativeVector C (ψ.comp φ) w x *
254 zcFreeGroupHomFoxJacobian C ψ φ x y := by
255 exact congrFun (zcFreeGroupFoxDerivativeVector_comp_linearMap C ψ φ w) y
257/-- Completed `Z_C[[H]]` Fox chain rule, component form for named derivative coordinates. -/
258theorem zcFreeGroupFoxDerivative_comp
259 [Fintype X]
260 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
261 (w : FreeGroup X) (y : Y) :
262 zcFreeGroupFoxDerivative C ψ y (φ w) =
263 ∑ x : X,
264 zcFreeGroupFoxDerivative C (ψ.comp φ) x w *
265 zcFreeGroupHomFoxJacobian C ψ φ x y := by
266 exact zcFreeGroupFoxDerivativeVector_comp_apply C ψ φ w y
268/-- Completed `Z_C[[H]]` Fox chain rule, matrix form. -/
270 [Fintype X]
271 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
272 (w : FreeGroup X) :
273 zcFreeGroupFoxDerivativeVector C ψ (φ w) =
274 Matrix.vecMul
275 (zcFreeGroupFoxDerivativeVector C (ψ.comp φ) w)
276 (zcFreeGroupHomFoxJacobianMatrix C ψ φ) := by
278 exact zcFreeGroupHomFoxJacobianLinearMap_eq_vecMul C ψ φ
279 (zcFreeGroupFoxDerivativeVector C (ψ.comp φ) w)
281variable {Z : Type u} [DecidableEq Z]
283omit [DecidableEq X] in
284/-- Completed `Z_C[[H]]` Fox-Jacobian chain rule, component form. -/
286 [Fintype Y]
287 (ψ : FreeGroup Z →* H)
288 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y)
289 (x : X) (z : Z) :
290 zcFreeGroupHomFoxJacobian C ψ (φ.comp χ) x z =
291 ∑ y : Y,
292 zcFreeGroupHomFoxJacobian C (ψ.comp φ) χ x y *
293 zcFreeGroupHomFoxJacobian C ψ φ y z := by
294 simpa [zcFreeGroupHomFoxJacobian] using
296 (X := X) (Y := Y) (Z := Z) (zcCompletedGroupAlgebraScalar C ψ) φ χ x z
298omit [DecidableEq X] in
299/-- Completed `Z_C[[H]]` Fox-Jacobian chain rule, linear-map form. -/
301 [Fintype X] [Fintype Y]
302 (ψ : FreeGroup Z →* H)
303 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
304 (zcFreeGroupHomFoxJacobianLinearMap C ψ φ).comp
305 (zcFreeGroupHomFoxJacobianLinearMap C (ψ.comp φ) χ) =
306 zcFreeGroupHomFoxJacobianLinearMap C ψ (φ.comp χ) := by
307 simpa [zcFreeGroupHomFoxJacobianLinearMap] using
309 (X := X) (Y := Y) (Z := Z) (zcCompletedGroupAlgebraScalar C ψ) φ χ
311omit [DecidableEq X] in
312/-- Completed `Z_C[[H]]` Fox-Jacobian chain rule, matrix form. -/
314 [Fintype Y]
315 (ψ : FreeGroup Z →* H)
316 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
317 zcFreeGroupHomFoxJacobianMatrix C ψ (φ.comp χ) =
318 zcFreeGroupHomFoxJacobianMatrix C (ψ.comp φ) χ *
319 zcFreeGroupHomFoxJacobianMatrix C ψ φ := by
320 apply Matrix.ext
321 intro x z
322 exact zcFreeGroupHomFoxJacobian_comp_apply C ψ φ χ x z
324end Jacobian
326/-- Uniqueness of the completed free-group derivative vector among crossed differentials with
327standard coordinate values on free generators. -/
329 (ψ : FreeGroup X →* H)
330 (delta : FreeGroup X → ZCFreeFoxCoordinates C (X := X) (H := H))
331 (hdelta : IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta)
332 (hbasis :
333 ∀ x : X, delta (FreeGroup.of x) =
334 Pi.single x (1 : ZCCompletedGroupAlgebra C H)) :
335 delta = zcFreeGroupFoxDerivativeVector C ψ := by
337 (A := ZCFreeFoxCoordinates C (X := X) (H := H))
339 (fun x => Pi.single x (1 : ZCCompletedGroupAlgebra C H))
340 delta hdelta hbasis
342/-- Existence and uniqueness theorem for the completed free-group derivative vector. -/
344 (ψ : FreeGroup X →* H) :
345 ∃! delta : FreeGroup X → ZCFreeFoxCoordinates C (X := X) (H := H),
346 IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta ∧
347 ∀ x : X, delta (FreeGroup.of x) =
348 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by
350 (A := ZCFreeFoxCoordinates C (X := X) (H := H))
352 (fun x => Pi.single x (1 : ZCCompletedGroupAlgebra C H))
354/-- Universal representation theorem for completed crossed differentials on a free group. -/
356 (ψ : FreeGroup X →* H) :
357 {delta : FreeGroup X → ZCFreeFoxCoordinates C (X := X) (H := H) //
358 IsCrossedDifferential (zcCompletedGroupAlgebraScalar C ψ) delta} ≃
359 (ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
360 ZCFreeFoxCoordinates C (X := X) (H := H)) :=
362 (A := ZCFreeFoxCoordinates C (X := X) (H := H)) C ψ
364/-- The linear map from the completed universal module representing the completed derivative
365vector. -/
367 (ψ : FreeGroup X →* H) :
368 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
369 ZCFreeFoxCoordinates C (X := X) (H := H) :=
371 (A := ZCFreeFoxCoordinates C (X := X) (H := H)) C ψ
375/-- The representing linear map evaluates on the universal differential as the completed
376derivative vector. -/
377@[simp]
379 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
381 (zcUniversalDifferential C ψ w) =
382 zcFreeGroupFoxDerivativeVector C ψ w := by
384 (A := ZCFreeFoxCoordinates C (X := X) (H := H)) C ψ
388/-- If the universal completed differential of a word vanishes, then its completed free Fox
389derivative vector vanishes. -/
391 (ψ : FreeGroup X →* H) {w : FreeGroup X}
392 (hw : zcUniversalDifferential C ψ w = 0) :
393 zcFreeGroupFoxDerivativeVector C ψ w = 0 := by
394 have h :=
395 congrArg (zcFreeGroupFoxDerivativeVectorLinearMap C ψ) hw
396 simpa using h
398/-- Component form of
401 (ψ : FreeGroup X →* H) (i : X) {w : FreeGroup X}
402 (hw : zcUniversalDifferential C ψ w = 0) :
403 zcFreeGroupFoxDerivative C ψ i w = 0 := by
404 have hvec :=
406 (C := C) ψ hw
407 simpa [zcFreeGroupFoxDerivative] using congrFun hvec i
409/-- Existence and uniqueness of the linear map representing the completed derivative vector. -/
411 (ψ : FreeGroup X →* H) :
412 ∃! f :
413 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
414 ZCFreeFoxCoordinates C (X := X) (H := H),
415 ∀ w : FreeGroup X,
416 f (zcUniversalDifferential C ψ w) =
417 zcFreeGroupFoxDerivativeVector C ψ w := by
419 (A := ZCFreeFoxCoordinates C (X := X) (H := H)) C ψ
425end
427end FoxDifferential