Source: ProCGroups.FoxDifferential.Discrete.FoxCalculus.Universal
1import ProCGroups.FoxDifferential.Discrete.FoxCalculus.Derivative
3/-!
4# Fox differential: discrete — fox calculus — universal
6The principal declarations in this module are:
8- `relativeDifferentialToFreeFoxCoordinates`
9 The universal map \(A_{\psi}\) \(\to\) \(\mathbb{Z}[H]^X\) induced by the relative Fox derivative.
10- `relativeFreeFoxCoordinatesLinearMap`
11 The linear map from pushed-forward Fox-coordinate vectors to \(A_{\psi}\), sending the coordinate
12 basis vector at \(x\) to \(\mathrm{universalDifferential}(\psi)(x)\).
13- `relativeDifferentialToFreeFoxCoordinates_d`
14 The coordinate map out of the universal differential module sends
15 \(\mathrm{universalDifferential}(w)\) to the Fox derivative of \(w\).
16- `relativeFreeFoxCoordinatesLinearMap_single`
17 The coordinate-to-differential map sends a coordinate basis vector to the corresponding universal
18 generator differential.
19-/
21namespace FoxDifferential
23noncomputable section
25namespace FoxCalculus
27open scoped BigOperators
29universe u v
32variable {H : Type v} [Group H]
33variable (X : Type u)
35variable [DecidableEq X]
36variable (ψ : FreeGroup X →* H)
38/--
39The universal map \(A_{\psi}\) \(\to\) \(\mathbb{Z}[H]^X\) induced by the relative Fox
40derivative.
41-/
42def relativeDifferentialToFreeFoxCoordinates :
43 DifferentialModule ψ →ₗ[GroupRing H] RelativeFreeFoxCoordinates (H := H) X :=
44 differentialModuleLift
45 (A := RelativeFreeFoxCoordinates (H := H) X)
46 ψ
47 (relativeFreeGroupFoxHom (H := H) X ψ)
49/--
50The coordinate map out of the universal differential module sends
51\(\mathrm{universalDifferential}(w)\) to the Fox derivative of \(w\).
52-/
53@[simp]
54theorem relativeDifferentialToFreeFoxCoordinates_d (w : FreeGroup X) :
55 relativeDifferentialToFreeFoxCoordinates (H := H) X ψ (universalDifferential ψ w) =
56 relativeFreeGroupFoxDerivative (H := H) X ψ w := by
57 change
58 differentialModuleLift ψ
59 (relativeFreeGroupFoxHom (H := H) X ψ)
60 (universalDifferential ψ w) =
61 relativeFreeGroupFoxDerivative (H := H) X ψ w
62 exact
63 differentialModuleLift_d
64 (A := RelativeFreeFoxCoordinates (H := H) X)
65 ψ
66 (relativeFreeGroupFoxHom (H := H) X ψ)
67 w
69variable [Fintype X]
71/--
72The linear map from pushed-forward Fox-coordinate vectors to \(A_{\psi}\), sending the
73coordinate basis vector at \(x\) to \(\mathrm{universalDifferential}(\psi)(x)\).
74-/
75def relativeFreeFoxCoordinatesLinearMap :
76 RelativeFreeFoxCoordinates (H := H) X →ₗ[GroupRing H] DifferentialModule ψ :=
77 { toFun := fun a =>
78 ∑ x : X, a x • universalDifferential ψ (FreeGroup.of x)
79 map_add' := by
80 intro a b
81 simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
82 map_smul' := by
83 intro r a
84 simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply, Finset.smul_sum,
85 smul_smul]}
87/--
88The coordinate-to-differential map sends a coordinate basis vector to the corresponding
89universal generator differential.
90-/
91@[simp]
92theorem relativeFreeFoxCoordinatesLinearMap_single (x : X) :
93 relativeFreeFoxCoordinatesLinearMap (H := H) X ψ
94 (Pi.single x (1 : GroupRing H)) =
95 universalDifferential ψ (FreeGroup.of x) := by
96 change (∑ y : X,
97 ((Pi.single x (1 : GroupRing H) : RelativeFreeFoxCoordinates (H := H) X) y) •
98 universalDifferential ψ (FreeGroup.of y)) =
99 universalDifferential ψ (FreeGroup.of x)
100 rw [Finset.sum_eq_single x]
101 · simp only [Pi.single_eq_same, one_smul]
102 · intro y _ hy
103 simp only [Pi.single_eq_of_ne hy, zero_smul]
104 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_smul,
105 IsEmpty.forall_iff]
107omit [DecidableEq X] [Fintype X] in
108/-- The universal relative differential on a free group satisfies the inverse rule. -/
109theorem relativeFreeGroupDifferential_inv (w : FreeGroup X) :
110 universalDifferential ψ w⁻¹ =
111 -((MonoidAlgebra.of ℤ H (ψ w⁻¹) : GroupRing H) • universalDifferential ψ w) := by
112 have h := universalDifferential_mul_inv_right ψ w⁻¹
113 rw [eq_neg_iff_add_eq_zero]
114 simpa using h
116/-- The relative Fox-coordinate formula recovers the universal differential in \(A_{\psi}\). -/
117theorem relativeFreeFoxCoordinatesLinearMap_derivative (w : FreeGroup X) :
118 relativeFreeFoxCoordinatesLinearMap (H := H) X ψ
119 (relativeFreeGroupFoxDerivative (H := H) X ψ w) =
120 universalDifferential ψ w := by
121 induction w using FreeGroup.induction_on with
122 | C1 =>
123 simp only [relativeFreeGroupFoxDerivative_one, map_zero, universalDifferential_one]
124 | of x =>
125 simp only [relativeFreeGroupFoxDerivative_of,
126 relativeFreeFoxCoordinatesLinearMap_single]
127 | inv_of x hx =>
128 rw [relativeFreeGroupFoxDerivative_inv, map_neg, map_smul, hx]
129 exact (relativeFreeGroupDifferential_inv (H := H) X ψ (FreeGroup.of x)).symm
130 | mul x y hx hy =>
131 rw [relativeFreeGroupFoxDerivative_mul, map_add, map_smul, hx, hy]
132 simpa using (universalDifferential_mul ψ x y).symm
134end FoxCalculus
136end
138end FoxDifferential