Source: ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Coordinates
1import ProCGroups.FoxDifferential.Common.FoxBoundary
2import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Derivative
4/-!
5# Fox differential: completed — \(\mathbb{Z}_C\) coefficients — free group — coordinates
7The principal declarations in this module are:
9- `zcFreeGroupFoxBoundary`
10 The completed Fox boundary/Euler map \(v \mapsto \sum_i v_i * ([\psi(x_i)]-1)\).
11- `zcDifferentialToFreeFoxCoordinates`
12 The linear map from the completed universal module to completed Fox-coordinate vectors.
13- `zcFreeGroupFoxBoundary_apply`
14 The boundary map is evaluated on the canonical generators and then extended linearly to the
15 completed coordinate module.
16- `zcFreeGroupFoxBoundary_eq_foxBoundaryMap`
17 The completed Fox boundary is the generic finite Fox boundary map specialized to \(x \mapsto
18 [\psi(x)] - 1\).
19-/
21namespace FoxDifferential
23noncomputable section
25open scoped BigOperators
27universe u v
30variable (C : ProCGroups.FiniteGroupClass.{v})
31variable {X : Type u} [DecidableEq X]
32variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
34section FiniteBasis
36variable [Fintype X]
38/-- The completed Fox boundary/Euler map \(v \mapsto \sum_i v_i * ([\psi(x_i)]-1)\). -/
39def zcFreeGroupFoxBoundary (ψ : FreeGroup X →* H) :
40 ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
41 ZCCompletedGroupAlgebra C H where
42 toFun v := ∑ i : X, v i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1)
43 map_add' := by
44 intro v w
45 simp only [Pi.add_apply, add_mul, Finset.sum_add_distrib]
46 map_smul' := by
47 intro r v
48 simp only [Pi.smul_apply, smul_eq_mul, mul_assoc, RingHom.id_apply, Finset.mul_sum]
50omit [DecidableEq X] in
51/--
52The boundary map is evaluated on the canonical generators and then extended linearly to the
53completed coordinate module.
54-/
55theorem zcFreeGroupFoxBoundary_apply
56 (ψ : FreeGroup X →* H) (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :
57 zcFreeGroupFoxBoundary C ψ v =
58 ∑ i : X, v i * (zcGroupLike C H (ψ (FreeGroup.of i)) - 1) :=
59 rfl
61omit [DecidableEq X] in
62/--
63The completed Fox boundary is the generic finite Fox boundary map specialized to \(x \mapsto
64[\psi(x)] - 1\).
65-/
66theorem zcFreeGroupFoxBoundary_eq_foxBoundaryMap
67 (ψ : FreeGroup X →* H) :
68 zcFreeGroupFoxBoundary C ψ =
69 foxBoundaryMap
70 (fun i : X =>
71 coefficientFoxBoundary (zcCompletedGroupAlgebraScalar C ψ) (FreeGroup.of i)) := by
72 ext v
73 rfl
75/--
76The completed Fox boundary sends a coordinate basis vector to the corresponding completed
77augmentation generator.
78-/
79@[simp]
80theorem zcFreeGroupFoxBoundary_single (ψ : FreeGroup X →* H) (i : X) :
81 zcFreeGroupFoxBoundary C ψ
82 (Pi.single i (1 : ZCCompletedGroupAlgebra C H)) =
83 zcCompletedGroupAlgebraBoundary C ψ (FreeGroup.of i) := by
84 rw [zcFreeGroupFoxBoundary_apply]
85 rw [Finset.sum_eq_single i]
86 · simp only [Pi.single_eq_same, one_mul]
87 rfl
88 · intro j _ hji
89 simp only [Pi.single_eq_of_ne hji, zero_mul]
90 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_mul, IsEmpty.forall_iff]
92/-- The linear map from the completed universal module to completed Fox-coordinate vectors. -/
93def zcDifferentialToFreeFoxCoordinates (ψ : FreeGroup X →* H) :
94 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]
95 ZCFreeFoxCoordinates C (X := X) (H := H) :=
96 zcFreeGroupFoxDerivativeVectorLinearMap C ψ
98omit [Fintype X] in
99/--
100The completed coordinate map sends a universal differential to the completed Fox derivative
101vector.
102-/
103@[simp]
104theorem zcDifferentialToFreeFoxCoordinates_universal
105 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
106 zcDifferentialToFreeFoxCoordinates C ψ
107 (zcUniversalDifferential C ψ w) =
108 zcFreeGroupFoxDerivativeVector C ψ w := by
109 exact zcFreeGroupFoxDerivativeVectorLinearMap_universal C ψ w
111/--
112The linear map from completed Fox-coordinate vectors to the completed universal module, sending
113the coordinate basis at \(x\) to \(d_{\psi}(x)\).
114-/
115def zcFreeFoxCoordinatesLinearMap (ψ : FreeGroup X →* H) :
116 ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]
117 ZCCompletedDifferentialModule C ψ where
118 toFun v := ∑ x : X, v x • zcUniversalDifferential C ψ (FreeGroup.of x)
119 map_add' := by
120 intro v w
121 simp only [Pi.add_apply, add_smul, Finset.sum_add_distrib]
122 map_smul' := by
123 intro r v
124 simp only [Pi.smul_apply, RingHom.id_apply, smul_eq_mul, Finset.smul_sum, smul_smul]
126/--
127The coordinate-to-differential map sends a coordinate basis vector to the corresponding
128universal completed differential.
129-/
130@[simp]
131theorem zcFreeFoxCoordinatesLinearMap_single (ψ : FreeGroup X →* H) (x : X) :
132 zcFreeFoxCoordinatesLinearMap C ψ
133 (Pi.single x (1 : ZCCompletedGroupAlgebra C H)) =
134 zcUniversalDifferential C ψ (FreeGroup.of x) := by
135 change (∑ y : X,
136 ((Pi.single x (1 : ZCCompletedGroupAlgebra C H) :
137 ZCFreeFoxCoordinates C (X := X) (H := H)) y) •
138 zcUniversalDifferential C ψ (FreeGroup.of y)) =
139 zcUniversalDifferential C ψ (FreeGroup.of x)
140 rw [Finset.sum_eq_single x]
141 · simp only [Pi.single_eq_same, one_smul]
142 · intro y _ hy
143 simp only [Pi.single_eq_of_ne hy, zero_smul]
144 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_smul, IsEmpty.forall_iff]
146/--
147The coordinate-to-differential map recovers the universal completed differential from the
148completed derivative vector.
149-/
150theorem zcFreeFoxCoordinatesLinearMap_derivativeVector
151 (ψ : FreeGroup X →* H) (w : FreeGroup X) :
152 zcFreeFoxCoordinatesLinearMap C ψ
153 (zcFreeGroupFoxDerivativeVector C ψ w) =
154 zcUniversalDifferential C ψ w := by
155 let beta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
156 (ZCCompletedDifferentialModule C ψ) :=
157 (zcFreeGroupFoxDerivativeVector C ψ).mapLinear
158 (zcFreeFoxCoordinatesLinearMap C ψ)
159 have hbasis :
160 ∀ x : X, beta (FreeGroup.of x) =
161 zcUniversalDifferential C ψ (FreeGroup.of x) := by
162 intro x
163 change zcFreeFoxCoordinatesLinearMap C ψ
164 (zcFreeGroupFoxDerivativeVector C ψ (FreeGroup.of x)) =
165 zcUniversalDifferential C ψ (FreeGroup.of x)
166 rw [zcFreeGroupFoxDerivativeVector_of, zcFreeFoxCoordinatesLinearMap_single]
167 have hbeta_eq :
168 beta =
169 freeCrossedHomWithCoeff
170 (A := ZCCompletedDifferentialModule C ψ)
171 (zcCompletedGroupAlgebraScalar C ψ)
172 (fun x => zcUniversalDifferential C ψ (FreeGroup.of x)) := by
173 exact freeCrossedHomWithCoeff_unique
174 (A := ZCCompletedDifferentialModule C ψ)
175 (zcCompletedGroupAlgebraScalar C ψ)
176 (fun x => zcUniversalDifferential C ψ (FreeGroup.of x))
177 beta hbasis
178 have huniv_eq :
179 zcUniversalDifferential C ψ =
180 freeCrossedHomWithCoeff
181 (A := ZCCompletedDifferentialModule C ψ)
182 (zcCompletedGroupAlgebraScalar C ψ)
183 (fun x => zcUniversalDifferential C ψ (FreeGroup.of x)) := by
184 exact freeCrossedHomWithCoeff_unique
185 (A := ZCCompletedDifferentialModule C ψ)
186 (zcCompletedGroupAlgebraScalar C ψ)
187 (fun x => zcUniversalDifferential C ψ (FreeGroup.of x))
188 (zcUniversalDifferential C ψ) (by intro x; rfl)
189 exact congrArg
190 (fun d : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)
191 (ZCCompletedDifferentialModule C ψ) => d w)
192 (hbeta_eq.trans huniv_eq.symm)
194/-- The coordinate map is a left inverse to the coordinate-to-differential map. -/
195theorem zcDifferentialToFreeFoxCoordinates_comp_zcFreeFoxCoordinatesLinearMap
196 (ψ : FreeGroup X →* H) :
197 (zcDifferentialToFreeFoxCoordinates C ψ).comp
198 (zcFreeFoxCoordinatesLinearMap C ψ) =
199 LinearMap.id := by
200 apply LinearMap.ext
201 intro v
202 rw [LinearMap.comp_apply]
203 change zcDifferentialToFreeFoxCoordinates C ψ
204 (∑ y : X, v y • zcUniversalDifferential C ψ (FreeGroup.of y)) = v
205 rw [map_sum]
206 simp only [map_smul, zcDifferentialToFreeFoxCoordinates_universal]
207 funext x
208 change ((∑ y : X,
209 v y • zcFreeGroupFoxDerivativeVector C ψ (FreeGroup.of y)) :
210 ZCFreeFoxCoordinates C (X := X) (H := H)) x = v x
211 rw [Finset.sum_apply]
212 rw [Finset.sum_eq_single x]
213 · simp only [zcFreeGroupFoxDerivativeVector_of, Pi.smul_apply, Pi.single_eq_same, smul_eq_mul,
214 mul_one]
215 · intro y _ hy
216 have hxy : x ≠ y := fun h => hy h.symm
217 simp only [zcFreeGroupFoxDerivativeVector_of, Pi.smul_apply, Pi.single_eq_of_ne hxy,
218 smul_eq_mul, mul_zero]
219 · simp only [Finset.mem_univ, not_true_eq_false, zcFreeGroupFoxDerivativeVector_of, Pi.smul_apply,
220 Pi.single_eq_same, smul_eq_mul, mul_one, IsEmpty.forall_iff]
222/-- The coordinate-to-differential map is a left inverse to the completed coordinate map. -/
223theorem zcFreeFoxCoordinatesLinearMap_comp_zcDifferentialToFreeFoxCoordinates
224 (ψ : FreeGroup X →* H) :
225 (zcFreeFoxCoordinatesLinearMap C ψ).comp
226 (zcDifferentialToFreeFoxCoordinates C ψ) =
227 LinearMap.id := by
228 apply crossedDifferentialModuleHom_ext
229 (A := ZCCompletedDifferentialModule C ψ)
230 (zcCompletedGroupAlgebraScalar C ψ)
231 intro w
232 change zcFreeFoxCoordinatesLinearMap C ψ
233 (zcDifferentialToFreeFoxCoordinates C ψ
234 (zcUniversalDifferential C ψ w)) =
235 zcUniversalDifferential C ψ w
236 rw [zcDifferentialToFreeFoxCoordinates_universal,
237 zcFreeFoxCoordinatesLinearMap_derivativeVector]
239/--
240The linear equivalence between completed Fox coordinates and the completed universal
241differential module of a finite-rank free group.
242-/
243def zcFreeFoxCoordinatesLinearEquivDifferential
244 (ψ : FreeGroup X →* H) :
245 ZCFreeFoxCoordinates C (X := X) (H := H) ≃ₗ[ZCCompletedGroupAlgebra C H]
246 ZCCompletedDifferentialModule C ψ := by
247 refine LinearEquiv.ofLinear
248 (zcFreeFoxCoordinatesLinearMap C ψ)
249 (zcDifferentialToFreeFoxCoordinates C ψ)
250 ?_ ?_
251 · exact zcFreeFoxCoordinatesLinearMap_comp_zcDifferentialToFreeFoxCoordinates C ψ
252 · exact zcDifferentialToFreeFoxCoordinates_comp_zcFreeFoxCoordinatesLinearMap C ψ
255end FiniteBasis
258end
260end FoxDifferential