Source: ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Derivative

1import ProCGroups.FoxDifferential.Common.FreeCrossedDifferential

2import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Core

4/-!

5# Fox differential: completed — \(\mathbb{Z}_C\) coefficients — free group — derivative

7The principal declarations in this module are:

9- `ZCFreeFoxCoordinates`

10 Completed Fox-coordinate vectors with coefficients in \(\mathbb{Z}_C\llbracket H\rrbracket\).

11- `zcFreeGroupFoxDerivativeVector`

12 Completed free-group Fox derivative vector, with coefficients pushed forward along

13 \(\psi:\mathrm{FreeGroup}(X)\to H\).

14- `zcFreeGroupFoxDerivativeVector_one`

15 The completed free-group derivative vector sends the identity word to zero.

16- `zcFreeGroupFoxDerivativeVector_of`

17 The completed free-group derivative vector sends a free generator to the corresponding coordinate

18 basis vector.

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]

34omit [DecidableEq X] in

35/-- Completed Fox-coordinate vectors with coefficients in \(\mathbb{Z}_C\llbracket H\rrbracket\). -/

36abbrev ZCFreeFoxCoordinates : Type (max u v) :=

37 X → ZCCompletedGroupAlgebra C H

39/--

40Completed free-group Fox derivative vector, with coefficients pushed forward along

41\(\psi:\mathrm{FreeGroup}(X)\to H\).

42-/

43def zcFreeGroupFoxDerivativeVector (ψ : FreeGroup X →* H) :

44 ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)

45 (ZCFreeFoxCoordinates C (X := X) (H := H)) :=

46 freeCrossedHomWithCoeff

47 (A := ZCFreeFoxCoordinates C (X := X) (H := H))

48 (zcCompletedGroupAlgebraScalar C ψ)

49 (fun x => Pi.single x (1 : ZCCompletedGroupAlgebra C H))

51/-- A coordinate of the completed free-group Fox derivative. -/

52def zcFreeGroupFoxDerivative (ψ : FreeGroup X →* H) (i : X) :

53 ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)

54 (ZCCompletedGroupAlgebra C H) :=

55 (zcFreeGroupFoxDerivativeVector C ψ).mapLinear

56 { toFun := fun v => v i

57 map_add' := by intro v w; rfl

58 map_smul' := by intro r v; rfl }

60/-- The completed free-group derivative vector sends the identity word to zero. -/

61@[simp]

62theorem zcFreeGroupFoxDerivativeVector_one (ψ : FreeGroup X →* H) :

63 zcFreeGroupFoxDerivativeVector C ψ (1 : FreeGroup X) = 0 := by

64 exact (zcFreeGroupFoxDerivativeVector C ψ).map_one

66/--

67The completed free-group derivative vector sends a free generator to the corresponding

68coordinate basis vector.

69-/

70@[simp]

71theorem zcFreeGroupFoxDerivativeVector_of (ψ : FreeGroup X →* H) (x : X) :

72 zcFreeGroupFoxDerivativeVector C ψ (FreeGroup.of x) =

73 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by

74 exact freeCrossedHomWithCoeff_of

75 (A := ZCFreeFoxCoordinates C (X := X) (H := H))

76 (zcCompletedGroupAlgebraScalar C ψ)

77 (fun x => Pi.single x (1 : ZCCompletedGroupAlgebra C H)) x

79section AbstractChainRule

81variable {Y : Type u}

82variable {A : Type*} [AddCommGroup A] [Module (ZCCompletedGroupAlgebra C H) A]

83variable [Fintype X]

85/--

86Completed \(\mathbb{Z}_C\llbracket H\rrbracket\) abstract Fox chain rule for an arbitrary

87crossed differential.

88-/

89theorem zcCrossedDifferential_comp_zcFreeGroupFoxDerivative

90 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)

91 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ) A)

92 (w : FreeGroup X) :

93 delta (φ w) =

94 ∑ x : X,

95 zcFreeGroupFoxDerivative C (ψ.comp φ) x w •

96 delta (φ (FreeGroup.of x)) := by

97 calc

98 delta (φ w) =

99 freeCrossedDifferentialWithCoeffExpansion

100 (X := X) (zcCompletedGroupAlgebraScalar C (ψ.comp φ))

101 (fun x : X => delta (φ (FreeGroup.of x))) w := by

102 exact freeCrossedHomWithCoeff_comp_expansion

103 (X := X) (Y := Y) (B := A)

104 (zcCompletedGroupAlgebraScalar C ψ) φ delta w

105 _ =

106 ∑ x : X,

107 zcFreeGroupFoxDerivative C (ψ.comp φ) x w •

108 delta (φ (FreeGroup.of x)) := by

109 rw [freeCrossedDifferentialWithCoeffExpansion,

110 freeCrossedDifferentialWithCoeffExpansionLinearMap_apply]

111 rfl

112

113end AbstractChainRule

114

115section Jacobian

116

117variable {Y : Type u} [DecidableEq Y]

118

119/--

120Completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian of a homomorphism of free groups.

121-/

122def zcFreeGroupHomFoxJacobian

123 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :

124 X → Y → ZCCompletedGroupAlgebra C H :=

125 freeCrossedDifferentialWithCoeffJacobian

126 (X := X) (Y := Y) (zcCompletedGroupAlgebraScalar C ψ) φ

127

128omit [DecidableEq X] in

129/--

130The completed Fox-Jacobian of a free-group homomorphism is evaluated by taking the completed Fox

131derivative vector of the image of a generator.

132-/

133@[simp]

134theorem zcFreeGroupHomFoxJacobian_apply

135 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)

136 (x : X) (y : Y) :

137 zcFreeGroupHomFoxJacobian C ψ φ x y =

138 zcFreeGroupFoxDerivative C ψ y (φ (FreeGroup.of x)) :=

139 rfl

140

141/-- The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian is packaged as a matrix. -/

142def zcFreeGroupHomFoxJacobianMatrix

143 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :

144 Matrix X Y (ZCCompletedGroupAlgebra C H) :=

145 freeCrossedDifferentialWithCoeffJacobianMatrix

146 (X := X) (Y := Y) (zcCompletedGroupAlgebraScalar C ψ) φ

147

148omit [DecidableEq X] in

149/--

150The matrix evaluation is componentwise the completed \(\mathbb{Z}_C\llbracket H\rrbracket\)

151Fox-Jacobian.

152-/

153@[simp]

154theorem zcFreeGroupHomFoxJacobianMatrix_apply

155 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)

156 (x : X) (y : Y) :

157 zcFreeGroupHomFoxJacobianMatrix C ψ φ x y =

158 zcFreeGroupHomFoxJacobian C ψ φ x y :=

159 rfl

160

161/--

162The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian is bundled into a finite

163linear map on coordinate vectors.

164-/

165def zcFreeGroupHomFoxJacobianLinearMap

166 [Fintype X]

167 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :

168 ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]

169 ZCFreeFoxCoordinates C (X := Y) (H := H) :=

170 freeCrossedDifferentialWithCoeffJacobianLinearMap

171 (X := X) (Y := Y) (zcCompletedGroupAlgebraScalar C ψ) φ

172

173omit [DecidableEq X] in

174/--

175Evaluation formula for the completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian linear

176map.

177-/

178@[simp]

179theorem zcFreeGroupHomFoxJacobianLinearMap_apply

180 [Fintype X]

181 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)

182 (v : ZCFreeFoxCoordinates C (X := X) (H := H)) (y : Y) :

183 zcFreeGroupHomFoxJacobianLinearMap C ψ φ v y =

184 ∑ x : X, v x * zcFreeGroupHomFoxJacobian C ψ φ x y :=

185 rfl

186

187omit [DecidableEq X] in

188/--

189The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian linear map is row-vector

190multiplication by its matrix.

191-/

192theorem zcFreeGroupHomFoxJacobianLinearMap_eq_vecMul

193 [Fintype X]

194 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)

195 (v : ZCFreeFoxCoordinates C (X := X) (H := H)) :

196 zcFreeGroupHomFoxJacobianLinearMap C ψ φ v =

197 Matrix.vecMul v (zcFreeGroupHomFoxJacobianMatrix C ψ φ) := by

198 exact freeCrossedDifferentialWithCoeffJacobianLinearMap_eq_vecMul

199 (X := X) (Y := Y) (zcCompletedGroupAlgebraScalar C ψ) φ v

200

201/--

202The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian of the identity homomorphism

203is the identity family.

204-/

205@[simp]

206theorem zcFreeGroupHomFoxJacobian_id (ψ : FreeGroup X →* H) :

207 zcFreeGroupHomFoxJacobian C ψ (MonoidHom.id (FreeGroup X)) =

208 foxJacobianId (R := ZCCompletedGroupAlgebra C H) (X := X) := by

209 simp only [zcFreeGroupHomFoxJacobian,

210 freeCrossedDifferentialWithCoeffJacobian_id (X := X) (S := ZCCompletedGroupAlgebra C H)

211 (zcCompletedGroupAlgebraScalar C ψ)]

212

213/--

214The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian matrix of the identity

215homomorphism is the identity matrix.

216-/

217@[simp]

218theorem zcFreeGroupHomFoxJacobianMatrix_id (ψ : FreeGroup X →* H) :

219 zcFreeGroupHomFoxJacobianMatrix C ψ (MonoidHom.id (FreeGroup X)) =

220 (1 : Matrix X X (ZCCompletedGroupAlgebra C H)) := by

221 simp only [zcFreeGroupHomFoxJacobianMatrix,

222 freeCrossedDifferentialWithCoeffJacobianMatrix_id (X := X) (S := ZCCompletedGroupAlgebra C H)

223 (zcCompletedGroupAlgebraScalar C ψ)]

224

225/--

226The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian linear map of the identity

227homomorphism is the identity.

228-/

229@[simp]

230theorem zcFreeGroupHomFoxJacobianLinearMap_id

231 [Fintype X] (ψ : FreeGroup X →* H) :

232 zcFreeGroupHomFoxJacobianLinearMap C ψ (MonoidHom.id (FreeGroup X)) =

233 (LinearMap.id :

234 ZCFreeFoxCoordinates C (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra C H]

235 ZCFreeFoxCoordinates C (X := X) (H := H)) := by

236 simp only [zcFreeGroupHomFoxJacobianLinearMap,

237 freeCrossedDifferentialWithCoeffJacobianLinearMap_id (X := X) (S := ZCCompletedGroupAlgebra C H)

238 (zcCompletedGroupAlgebraScalar C ψ)]

239

240/-- Completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox chain rule in vector form. -/

241theorem zcFreeGroupFoxDerivativeVector_comp_linearMap

242 [Fintype X]

243 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)

244 (w : FreeGroup X) :

245 zcFreeGroupFoxDerivativeVector C ψ (φ w) =

246 zcFreeGroupHomFoxJacobianLinearMap C ψ φ

247 (zcFreeGroupFoxDerivativeVector C (ψ.comp φ) w) := by

248 have hcoeff :

249 zcCompletedGroupAlgebraScalar C (ψ.comp φ) =

250 (zcCompletedGroupAlgebraScalar C ψ).comp φ := by

251 ext g

252 rfl

253 simpa [zcFreeGroupFoxDerivativeVector, zcFreeGroupHomFoxJacobianLinearMap,

254 zcFreeGroupHomFoxJacobian, freeCrossedDifferentialWithCoeffCoordinates, hcoeff] using

255 freeCrossedDifferentialWithCoeffCoordinates_comp_linearMap

256 (X := X) (Y := Y) (zcCompletedGroupAlgebraScalar C ψ) φ w

257

258/-- Completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox chain rule in component form. -/

259theorem zcFreeGroupFoxDerivativeVector_comp_apply

260 [Fintype X]

261 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)

262 (w : FreeGroup X) (y : Y) :

263 zcFreeGroupFoxDerivativeVector C ψ (φ w) y =

264 ∑ x : X,

265 zcFreeGroupFoxDerivativeVector C (ψ.comp φ) w x *

266 zcFreeGroupHomFoxJacobian C ψ φ x y := by

267 exact congrFun (zcFreeGroupFoxDerivativeVector_comp_linearMap C ψ φ w) y

268

269/--

270Completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox chain rule, component form for named

271derivative coordinates.

272-/

273theorem zcFreeGroupFoxDerivative_comp

274 [Fintype X]

275 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)

276 (w : FreeGroup X) (y : Y) :

277 zcFreeGroupFoxDerivative C ψ y (φ w) =

278 ∑ x : X,

279 zcFreeGroupFoxDerivative C (ψ.comp φ) x w *

280 zcFreeGroupHomFoxJacobian C ψ φ x y := by

281 exact zcFreeGroupFoxDerivativeVector_comp_apply C ψ φ w y

282

283/-- The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox chain rule in matrix form. -/

284theorem zcFreeGroupFoxDerivativeVector_comp_matrix

285 [Fintype X]

286 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)

287 (w : FreeGroup X) :

288 zcFreeGroupFoxDerivativeVector C ψ (φ w) =

289 Matrix.vecMul

290 (zcFreeGroupFoxDerivativeVector C (ψ.comp φ) w)

291 (zcFreeGroupHomFoxJacobianMatrix C ψ φ) := by

292 rw [zcFreeGroupFoxDerivativeVector_comp_linearMap]

293 exact zcFreeGroupHomFoxJacobianLinearMap_eq_vecMul C ψ φ

294 (zcFreeGroupFoxDerivativeVector C (ψ.comp φ) w)

295

296variable {Z : Type u} [DecidableEq Z]

297

298omit [DecidableEq X] in

299/--

300The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian chain rule is expressed

301componentwise.

302-/

303theorem zcFreeGroupHomFoxJacobian_comp_apply

304 [Fintype Y]

305 (ψ : FreeGroup Z →* H)

306 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y)

307 (x : X) (z : Z) :

308 zcFreeGroupHomFoxJacobian C ψ (φ.comp χ) x z =

309 ∑ y : Y,

310 zcFreeGroupHomFoxJacobian C (ψ.comp φ) χ x y *

311 zcFreeGroupHomFoxJacobian C ψ φ y z := by

312 have hcoeff :

313 zcCompletedGroupAlgebraScalar C (ψ.comp φ) =

314 (zcCompletedGroupAlgebraScalar C ψ).comp φ := by

315 ext g

316 rfl

317 simpa [zcFreeGroupHomFoxJacobian, hcoeff] using

318 freeCrossedDifferentialWithCoeffJacobian_comp_apply

319 (X := X) (Y := Y) (Z := Z) (zcCompletedGroupAlgebraScalar C ψ) φ χ x z

320

321omit [DecidableEq X] in

322/--

323The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian chain rule is expressed in

324linear-map form.

325-/

326theorem zcFreeGroupHomFoxJacobianLinearMap_comp

327 [Fintype X] [Fintype Y]

328 (ψ : FreeGroup Z →* H)

329 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :

330 (zcFreeGroupHomFoxJacobianLinearMap C ψ φ).comp

331 (zcFreeGroupHomFoxJacobianLinearMap C (ψ.comp φ) χ) =

332 zcFreeGroupHomFoxJacobianLinearMap C ψ (φ.comp χ) := by

333 have hcoeff :

334 zcCompletedGroupAlgebraScalar C (ψ.comp φ) =

335 (zcCompletedGroupAlgebraScalar C ψ).comp φ := by

336 ext g

337 rfl

338 simpa [zcFreeGroupHomFoxJacobianLinearMap, hcoeff] using

339 freeCrossedDifferentialWithCoeffJacobianLinearMap_comp

340 (X := X) (Y := Y) (Z := Z) (zcCompletedGroupAlgebraScalar C ψ) φ χ

341

342omit [DecidableEq X] in

343/--

344The completed \(\mathbb{Z}_C\llbracket H\rrbracket\) Fox-Jacobian chain rule is expressed in

345matrix form.

346-/

347theorem zcFreeGroupHomFoxJacobianMatrix_comp

348 [Fintype Y]

349 (ψ : FreeGroup Z →* H)

350 (φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :

351 zcFreeGroupHomFoxJacobianMatrix C ψ (φ.comp χ) =

352 zcFreeGroupHomFoxJacobianMatrix C (ψ.comp φ) χ *

353 zcFreeGroupHomFoxJacobianMatrix C ψ φ := by

354 apply Matrix.ext

355 intro x z

356 exact zcFreeGroupHomFoxJacobian_comp_apply C ψ φ χ x z

357

358end Jacobian

359

360/--

361Uniqueness of the completed free-group derivative vector among crossed differentials with

362standard coordinate values on free generators.

363-/

364theorem zcFreeGroupFoxDerivativeVector_unique

365 (ψ : FreeGroup X →* H)

366 (delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)

367 (ZCFreeFoxCoordinates C (X := X) (H := H)))

368 (hbasis :

369 ∀ x : X, delta (FreeGroup.of x) =

370 Pi.single x (1 : ZCCompletedGroupAlgebra C H)) :

371 delta = zcFreeGroupFoxDerivativeVector C ψ := by

372 exact freeCrossedHomWithCoeff_unique

373 (A := ZCFreeFoxCoordinates C (X := X) (H := H))

374 (zcCompletedGroupAlgebraScalar C ψ)

375 (fun x => Pi.single x (1 : ZCCompletedGroupAlgebra C H))

376 delta hbasis

377

378/-- Existence and uniqueness theorem for the completed free-group derivative vector. -/

379theorem existsUnique_zcFreeGroupFoxDerivativeVector

380 (ψ : FreeGroup X →* H) :

381 ∃! delta : ScalarCrossedHom (zcCompletedGroupAlgebraScalar C ψ)

382 (ZCFreeFoxCoordinates C (X := X) (H := H)),

383 ∀ x : X, delta (FreeGroup.of x) =

384 Pi.single x (1 : ZCCompletedGroupAlgebra C H) := by

385 exact existsUnique_freeCrossedHomWithCoeff

386 (A := ZCFreeFoxCoordinates C (X := X) (H := H))

387 (zcCompletedGroupAlgebraScalar C ψ)

388 (fun x => Pi.single x (1 : ZCCompletedGroupAlgebra C H))

389

390/--

391The linear map from the completed universal module representing the completed derivative vector.

392-/

393def zcFreeGroupFoxDerivativeVectorLinearMap

394 (ψ : FreeGroup X →* H) :

395 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]

396 ZCFreeFoxCoordinates C (X := X) (H := H) :=

397 crossedHomModuleLift

398 (A := ZCFreeFoxCoordinates C (X := X) (H := H))

399 (zcCompletedGroupAlgebraScalar C ψ)

400 (zcFreeGroupFoxDerivativeVector C ψ)

401

402/--

403The representing linear map evaluates on the universal differential as the completed derivative

404vector.

405-/

406@[simp]

407theorem zcFreeGroupFoxDerivativeVectorLinearMap_universal

408 (ψ : FreeGroup X →* H) (w : FreeGroup X) :

409 zcFreeGroupFoxDerivativeVectorLinearMap C ψ

410 (zcUniversalDifferential C ψ w) =

411 zcFreeGroupFoxDerivativeVector C ψ w := by

412 exact crossedHomModuleLift_universal

413 (A := ZCFreeFoxCoordinates C (X := X) (H := H))

414 (zcCompletedGroupAlgebraScalar C ψ)

415 (zcFreeGroupFoxDerivativeVector C ψ) w

416

417/--

418If the universal completed differential of a word vanishes, then its completed free Fox

419derivative vector vanishes.

420-/

421theorem zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero

422 (ψ : FreeGroup X →* H) {w : FreeGroup X}

423 (hw : zcUniversalDifferential C ψ w = 0) :

424 zcFreeGroupFoxDerivativeVector C ψ w = 0 := by

425 have h :=

426 congrArg (zcFreeGroupFoxDerivativeVectorLinearMap C ψ) hw

427 simpa using h

428

429/-- The vanishing criterion for the completed Fox derivative vector holds componentwise. -/

430theorem zcFreeGroupFoxDerivative_eq_zero_of_zcUniversalDifferential_eq_zero

431 (ψ : FreeGroup X →* H) (i : X) {w : FreeGroup X}

432 (hw : zcUniversalDifferential C ψ w = 0) :

433 zcFreeGroupFoxDerivative C ψ i w = 0 := by

434 have hvec :=

435 zcFreeGroupFoxDerivativeVector_eq_zero_of_zcUniversalDifferential_eq_zero

436 (C := C) ψ hw

437 simpa [zcFreeGroupFoxDerivative] using congrFun hvec i

438

439/-- Existence and uniqueness of the linear map representing the completed derivative vector. -/

440theorem existsUnique_zcFreeGroupFoxDerivativeVectorLinearMap

441 (ψ : FreeGroup X →* H) :

442 ∃! f :

443 ZCCompletedDifferentialModule C ψ →ₗ[ZCCompletedGroupAlgebra C H]

444 ZCFreeFoxCoordinates C (X := X) (H := H),

445 ∀ w : FreeGroup X,

446 f (zcUniversalDifferential C ψ w) =

447 zcFreeGroupFoxDerivativeVector C ψ w := by

448 exact existsUnique_crossedHomModuleLift

449 (A := ZCFreeFoxCoordinates C (X := X) (H := H))

450 (zcCompletedGroupAlgebraScalar C ψ)

451 (zcFreeGroupFoxDerivativeVector C ψ)

455end

457end FoxDifferential