maps.scm 17 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695
  1. #| -*-Scheme-*-
  2. Copyright (C) 1986, 1987, 1988, 1989, 1990, 1991, 1992, 1993, 1994,
  3. 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002, 2003, 2004, 2005,
  4. 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013 Massachusetts
  5. Institute of Technology
  6. This file is part of MIT/GNU Scheme.
  7. MIT/GNU Scheme is free software; you can redistribute it and/or modify
  8. it under the terms of the GNU General Public License as published by
  9. the Free Software Foundation; either version 2 of the License, or (at
  10. your option) any later version.
  11. MIT/GNU Scheme is distributed in the hope that it will be useful, but
  12. WITHOUT ANY WARRANTY; without even the implied warranty of
  13. MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
  14. General Public License for more details.
  15. You should have received a copy of the GNU General Public License
  16. along with MIT/GNU Scheme; if not, write to the Free Software
  17. Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301,
  18. USA.
  19. |#
  20. ;;;; Maps between manifolds.
  21. ;;; If we have a function on a manifold M and a map from manifold N to
  22. ;;; manifold M we can define a function on N:
  23. (define* ((pullback-function mu:N->M) f-on-M)
  24. (compose f-on-M mu:N->M))
  25. ;;; If we have an inverse map mu^-1:M->N, we can push a function
  26. ;;; on N forward through the map:
  27. (define* ((pushforward-function mu^-1:M->N) f-on-N)
  28. (compose f-on-N mu^-1:M->N))
  29. ;;; The map between manifolds induces various ways to transport
  30. ;;; vectors from one manifold to another. The simplest of these is
  31. ;;; the differential.
  32. ;;; The differential of a function mu:N->M from N to M takes a vector
  33. ;;; field on the source manifold N to a vector field-like operator on
  34. ;;; the target manifold M. This results in a vector field over the
  35. ;;; map mu:N->M. The result takes directional derivatives of
  36. ;;; functions defined on M, at points of M that are targets of points
  37. ;;; of N.
  38. (define* ((differential-of-map mu:N->M) v-on-N)
  39. (define (v-on-M g-on-M)
  40. (v-on-N (compose g-on-M mu:N->M)))
  41. (assert (vector-field? v-on-N))
  42. (procedure->vector-field v-on-M
  43. `((d ,(diffop-name mu:N->M))
  44. ,(diffop-name v-on-N))))
  45. (define differential differential-of-map)
  46. ;;; For a long time we were confused between the concepts of
  47. ;;; differential and pushforward. The resolution seems to be that the
  48. ;;; differential takes the manifold position in the source manifold
  49. ;;; and the pushforward takes the manifold position in the target
  50. ;;; manifold of the map. So the pushforward needs an inverse map to
  51. ;;; define it and so the pushforward is not a very useful idea.
  52. (define* ((pushforward-vector mu:N->M mu^-1:M->N) v-on-N)
  53. ;; Assume (compose mu^-1:M->N mu:N->M) = identity
  54. (procedure->vector-field
  55. (lambda (f)
  56. (compose (((differential mu:N->M) v-on-N) f) mu^-1:M->N))
  57. `((pushforward ,(diffop-name mu:N->M))
  58. ,(diffop-name v-on-N))))
  59. (define (literal-manifold-map name source target)
  60. (let ((n (source 'dimension))
  61. (m (target 'dimension)))
  62. (let ((sig (if (fix:= n 1) (-> Real Real) (-> (UP* Real n) Real))))
  63. (compose (target '->point)
  64. (s:generate m 'up
  65. (lambda (i)
  66. (literal-function
  67. (string->symbol
  68. (string-append (symbol->string name)
  69. "^"
  70. (number->string i)))
  71. sig)))
  72. (source '->coords)))))
  73. #|
  74. ;;; Explanation of the connection between the basis forms and the
  75. ;;; differentials of coordinate functions.
  76. (install-coordinates R3-rect (up 'x 'y 'z))
  77. (define R3-rect-point ((R3-rect '->point) (up 'x0 'y0 'z0)))
  78. (install-coordinates R3-cyl (up 'r 'theta 'zeta))
  79. (define R3-cyl-point ((R3-cyl '->point) (up 'r0 'theta0 'zeta0)))
  80. (define counter-clockwise (- (* x d/dy) (* y d/dx)))
  81. (define outward (+ (* x d/dx) (* y d/dy)))
  82. (pec ((dx counter-clockwise) R3-rect-point))
  83. #| Result:
  84. (* -1 y0)
  85. |#
  86. (pec ((((differential x) counter-clockwise) identity) R3-rect-point))
  87. #| Result:
  88. (* -1 y0)
  89. |#
  90. (pec ((dx outward) R3-rect-point))
  91. #| Result:
  92. x0
  93. |#
  94. (pec ((((differential x) outward) identity) R3-rect-point))
  95. #| Result:
  96. x0
  97. |#
  98. (pec ((dy counter-clockwise) R3-rect-point))
  99. #| Result:
  100. x0
  101. |#
  102. (pec ((((differential y) counter-clockwise) identity) R3-rect-point))
  103. #| Result:
  104. x0
  105. |#
  106. (pec ((dy outward) R3-rect-point))
  107. #| Result:
  108. y0
  109. |#
  110. (pec ((((differential y) outward) identity) R3-rect-point))
  111. #| Result:
  112. y0
  113. |#
  114. (pec ((dr counter-clockwise) R3-cyl-point))
  115. #| Result:
  116. 0
  117. |#
  118. (pec ((((differential r) counter-clockwise) identity) R3-cyl-point))
  119. #| Result:
  120. 0
  121. |#
  122. (pec ((dr outward) R3-cyl-point))
  123. #| Result:
  124. r0
  125. |#
  126. (pec ((((differential r) outward) identity) R3-cyl-point))
  127. #| Result:
  128. r0
  129. |#
  130. (pec ((dtheta counter-clockwise) R3-cyl-point))
  131. #| Result:
  132. 1
  133. |#
  134. (pec ((((differential theta) counter-clockwise) identity) R3-cyl-point))
  135. #| Result:
  136. 1
  137. |#
  138. (pec ((dtheta outward) R3-cyl-point))
  139. #| Result:
  140. 0
  141. |#
  142. (pec ((((differential theta) outward) identity) R3-cyl-point))
  143. #| Result:
  144. 0
  145. |#
  146. |#
  147. #|
  148. (install-coordinates R2-rect (up 'x 'y))
  149. (define R2-rect-point ((R2-rect '->point) (up 'x0 'y0)))
  150. (install-coordinates R1-rect 't)
  151. (define mu (literal-manifold-map 'mu R1-rect R2-rect))
  152. (define f (literal-scalar-field 'f R2-rect))
  153. (pec ((((differential mu) d/dt) f)
  154. ((R1-rect '->point) 'tau)))
  155. #| Result:
  156. (+ (* (((partial 1) f) (up (mu0 tau) (mu1 tau))) ((D mu1) tau))
  157. (* (((partial 0) f) (up (mu0 tau) (mu1 tau))) ((D mu0) tau)))
  158. |#
  159. (pec ((dx ((differential mu) d/dt))
  160. ((R1-rect '->point) 'tau)))
  161. #| Result:
  162. ((D mu0) tau)
  163. |#
  164. (pec ((dy ((differential mu) d/dt))
  165. ((R1-rect '->point) 'tau)))
  166. #| Result:
  167. ((D mu1) tau)
  168. |#
  169. ;;; but this is a fraud... Note that if we have a non-coordinate basis
  170. ;;; the dual does not work on the transported vector.
  171. (define e0 (literal-vector-field 'e0 R2-rect))
  172. (define e1 (literal-vector-field 'e1 R2-rect))
  173. (define edual (vector-basis->dual (down e0 e1) R2-rect))
  174. (pec (((ref edual 0) ((differential mu) d/dt))
  175. ((R1-rect '->point) 'tau)))
  176. ;Bad point: rectangular #(tau)
  177. ;;; However, if we kludge the correct argument it gives the expected
  178. ;;; answer.
  179. (pec (((ref edual 0)
  180. (procedure->vector-field
  181. (lambda (f)
  182. (lambda (m)
  183. ((((differential mu) d/dt) f)
  184. ((R1-rect '->point) 't))))))
  185. R2-rect-point))
  186. #| Result:
  187. (/ (+ (* -1 (e1^1 (up x0 y0)) ((D mu0) t))
  188. (* (e1^0 (up x0 y0)) ((D mu1) t)))
  189. (+ (* -1 (e0^0 (up x0 y0)) (e1^1 (up x0 y0)))
  190. (* (e0^1 (up x0 y0)) (e1^0 (up x0 y0)))))
  191. |#
  192. ;;; General path on the sphere
  193. (define mu
  194. (compose (S2-spherical '->point)
  195. (up (literal-function 'theta)
  196. (literal-function 'phi))
  197. (R1-rect '->coords)))
  198. (define f
  199. (compose (literal-function 'f (-> (UP Real Real) Real))
  200. (S2-spherical '->coords)))
  201. (pec ((((differential mu) d/dt) f)
  202. ((R1-rect '->point) 't)))
  203. #| Result:
  204. (+ (* ((D theta) t) (((partial 0) f) (up (theta t) (phi t))))
  205. (* (((partial 1) f) (up (theta t) (phi t))) ((D phi) t)))
  206. |#
  207. |#
  208. ;;; Another way to obtain a vector field over a map is to start with a
  209. ;;; vector field on the target manifold. Given a vector field v-on-M
  210. ;;; and a map mu:N->M, we obtain a vector field over the map. This is
  211. ;;; a thing like a vector field on M restricted to the targets of
  212. ;;; mu:N->M and evaluated on points of N.
  213. (define* ((vector-field->vector-field-over-map mu:N->M) v-on-M)
  214. (procedure->vector-field
  215. (lambda (f-on-M)
  216. (compose (v-on-M f-on-M)
  217. mu:N->M))
  218. `((vector-field->vector-field-over-map ,(diffop-name mu:N->M))
  219. ,(diffop-name v-on-M))))
  220. ;;; A form field can also be transported across a map. Given a form
  221. ;;; field on M and a map mu:N->M, we obtain a thing like a form field
  222. ;;; on M that measures vectors over the map mu:N->M and is evaluated
  223. ;;; on points of N.
  224. #|
  225. (define ((1form-field-over-map mu:N->M) w-on-M)
  226. (procedure->1form-field
  227. (lambda (V-over-mu)
  228. (lambda (n)
  229. ((w-on-M
  230. (vector-field-over-map->vector-field V-over-mu n))
  231. (mu:N->M n))))
  232. `((1form-field-over-map ,(diffop-name mu:N->M))
  233. ,(diffop-name w-on-M))))
  234. |#
  235. (define* ((form-field->form-field-over-map mu:N->M) w-on-M)
  236. (define (vector-field-over-map->vector-field V-over-mu n)
  237. ;; This helper has no clear meaning.
  238. (procedure->vector-field
  239. (lambda (f)
  240. (lambda (m)
  241. ;;(assert (= m (mu:N->M n)))
  242. ((V-over-mu f) n)))
  243. `(vector-field-over-map->vector-field
  244. ,(diffop-name V-over-mu))))
  245. (procedure->nform-field
  246. (lambda vectors-over-map
  247. (assert (= (length vectors-over-map) (get-rank w-on-M)))
  248. (lambda (n)
  249. ((apply w-on-M
  250. (map (lambda (V-over-mu)
  251. (vector-field-over-map->vector-field V-over-mu n))
  252. vectors-over-map))
  253. (mu:N->M n))))
  254. (get-rank w-on-M)
  255. `((form-field->form-field-over-map ,(diffop-name mu:N->M))
  256. ,(diffop-name w-on-M))))
  257. (define (basis->basis-over-map mu:N->M basis-on-M)
  258. (let ((vector-basis-on-M (basis->vector-basis basis-on-M))
  259. (dual-basis-on-M (basis->1form-basis basis-on-M)))
  260. (make-basis
  261. (s:map/r (vector-field->vector-field-over-map mu:N->M)
  262. vector-basis-on-M)
  263. (s:map/r (form-field->form-field-over-map mu:N->M)
  264. dual-basis-on-M))))
  265. #|
  266. (install-coordinates S2-spherical (up 'theta 'phi))
  267. (define f (literal-scalar-field 'f S2-spherical))
  268. ;;; General path on the sphere
  269. (define mu
  270. (compose (S2-spherical '->point)
  271. (up (literal-function 'theta)
  272. (literal-function 'phi))
  273. (R1-rect '->coords)))
  274. (pec ((((vector-field->vector-field-over-map mu) d/dtheta) f)
  275. ((R1-rect '->point) 't)))
  276. #| Result:
  277. (((partial 0) f) (up (theta t) (phi t)))
  278. |#
  279. (pec ((((form-field->form-field-over-map mu) dtheta)
  280. ((differential mu) d/dt))
  281. ((R1-rect '->point) 't)))
  282. #| Result:
  283. ((D theta) t)
  284. |#
  285. (define foo
  286. (basis->basis-over-map mu
  287. (coordinate-system->basis S2-spherical)))
  288. (pec
  289. (((basis->1form-basis foo)
  290. (basis->vector-basis foo))
  291. ((R1-rect '->point) 't)))
  292. #| Result:
  293. (up (down 1 0) (down 0 1))
  294. |#
  295. (pec
  296. (((basis->1form-basis foo)
  297. ((differential mu) d/dt))
  298. ((R1-rect '->point) 't)))
  299. #| Result:
  300. (up ((D theta) t) ((D phi) t))
  301. |#
  302. |#
  303. ;;; The following helper is used to define pullbacks of forms.
  304. #|
  305. (define ((effective-pushforward mu:N->M n) v-on-N)
  306. (procedure->vector-field
  307. (lambda (g-on-M)
  308. (lambda (m)
  309. ;;(assert (= m (mu:N->M n)))
  310. ((((differential mu:N->M) v-on-N)
  311. g-on-M)
  312. n)))
  313. `((differential ,(diffop-name mu:N->M))
  314. ,(diffop-name v-on-N))))
  315. ;;; We extend the pullback to 1-forms:
  316. (define* ((pullback-1form mu:N->M) omega-on-M)
  317. (procedure->1form-field
  318. (lambda (v-on-N)
  319. (lambda (n)
  320. ((omega-on-M
  321. ((effective-pushforward mu:N->M n) v-on-N))
  322. (mu:N->M n))))
  323. `((pullback ,(diffop-name mu:N->M))
  324. ,(diffop-name omega-on-M))))
  325. (define* ((pullback-1form mu:N->M) omega-on-M)
  326. (procedure->1form-field
  327. (lambda (X-on-N)
  328. (((form-field->form-field-over-map mu:N->M) omega-on-M)
  329. ((differential mu:N->M) X-on-N)))
  330. `((pullback ,(diffop-name mu:N->M))
  331. ,(diffop-name omega-on-M))))
  332. (define* ((pullback mu:N->M) omega-on-M)
  333. (let ((k (get-rank omega-on-M)))
  334. (if (= k 0)
  335. ((pullback-function mu:N->M) omega-on-M)
  336. (let ((the-pullback
  337. (lambda args
  338. (assert (fix:= (length args) k))
  339. (lambda (n)
  340. ((apply omega-on-M
  341. (map (effective-pushforward mu:N->M n)
  342. args))
  343. (mu:N->M n))))))
  344. (procedure->nform-field the-pullback
  345. k
  346. `((pullback ,(diffop-name mu:N->M))
  347. ,(diffop-name omega-on-M)))))))
  348. |#
  349. ;;; The general case
  350. ;;; ((mu^* w) v) = w (mu_* v) = (w^mu ((d mu) v))
  351. (define* ((pullback-form mu:N->M) omega-on-M)
  352. (let ((k (get-rank omega-on-M)))
  353. (if (= k 0)
  354. ((pullback-function mu:N->M) omega-on-M)
  355. (procedure->nform-field
  356. (lambda vectors-on-N
  357. (apply ((form-field->form-field-over-map mu:N->M) omega-on-M)
  358. (map (differential mu:N->M)
  359. vectors-on-N)))
  360. k
  361. `((pullback ,(diffop-name mu:N->M))
  362. ,(diffop-name omega-on-M))))))
  363. (define (pullback-vector-field mu:N->M mu^-1:M->N)
  364. (pushforward-vector mu^-1:M->N mu:N->M))
  365. (define* (pullback mu:N->M #:optional mu^-1:M->N)
  366. (lambda (thing)
  367. (if (vector-field? thing)
  368. (if (default-object? mu^-1:M->N)
  369. (error "Pullback vector needs inverse map")
  370. ((pullback-vector-field mu:N->M mu^-1:M->N) thing))
  371. ((pullback-form mu:N->M) thing))))
  372. #|
  373. (pec (((pullback mu) f)
  374. ((R1-rect '->point) 't)))
  375. #| Result:
  376. (f (up (theta t) (phi t)))
  377. |#
  378. (pec
  379. ((((pullback mu) dtheta) d/dt)
  380. ((R1-rect '->point) 't)))
  381. #| Result:
  382. ((D theta) t)
  383. |#
  384. (pec
  385. ((((pullback mu)
  386. (wedge dtheta dphi))
  387. d/dt d/dt)
  388. ((R1-rect '->point) 't)))
  389. #| Result:
  390. 0
  391. |#
  392. |#
  393. #|
  394. (install-coordinates R3-rect (up 'x 'y 'z))
  395. (install-coordinates R3-cyl (up 'r 'theta 'zeta))
  396. (define mu
  397. (compose
  398. (R3-cyl '->point)
  399. (up (literal-function 'mu^r
  400. (-> (UP Real Real Real) Real))
  401. (literal-function 'mu^theta
  402. (-> (UP Real Real Real) Real))
  403. (literal-function 'mu^zeta
  404. (-> (UP Real Real Real) Real)))
  405. (R3-rect '->coords)))
  406. (pec
  407. ((((pullback mu) dtheta) d/dx)
  408. ((R3-rect '->point) (up 'x 'y 'z))))
  409. #| Result:
  410. (((partial 0) mu^theta) (up x y z))
  411. |#
  412. (pec
  413. ((((pullback mu) dtheta) d/dy)
  414. ((R3-rect '->point) (up 'x 'y 'z))))
  415. #| Result:
  416. (((partial 1) mu^theta) (up x y z))
  417. |#
  418. (pec
  419. ((((pullback mu) dr) d/dx)
  420. ((R3-rect '->point) (up 'x 'y 'z))))
  421. #| Result:
  422. (((partial 0) mu^r) (up x y z))
  423. |#
  424. (pec
  425. ((((pullback mu) dr) d/dy)
  426. ((R3-rect '->point) (up 'x 'y 'z))))
  427. #| Result:
  428. (((partial 1) mu^r) (up x y z))
  429. |#
  430. (pec
  431. ((((pullback mu)
  432. (wedge dr dtheta))
  433. d/dx d/dy)
  434. ((R3-rect '->point)
  435. (up 'x 'y 'z))))
  436. #| Result:
  437. (+ (* (((partial 1) mu^theta) (up x y z))
  438. (((partial 0) mu^r) (up x y z)))
  439. (* -1
  440. (((partial 1) mu^r) (up x y z))
  441. (((partial 0) mu^theta) (up x y z))))
  442. |#
  443. |#
  444. #|
  445. (define m ((R2-rect '->point) (up 3 4)))
  446. (install-coordinates R2-rect (up 'x 'y))
  447. (define phi
  448. (compose (R2-rect '->point)
  449. (up square cube)
  450. (R1-rect '->coords)))
  451. (pec ((((pullback phi) (* x dy)) d/dt)
  452. ((R1-rect '->point) 't0)))
  453. #| Result:
  454. (* 3 (expt t0 4))
  455. |#
  456. (define psi
  457. (compose (R1-rect '->point)
  458. (lambda (v)
  459. (let ((x (ref v 0))
  460. (y (ref v 1)))
  461. (- x y)))
  462. (R2-rect '->coords)))
  463. (pec ((((pullback psi) dt)
  464. (literal-vector-field 'u R2-rect))
  465. ((R2-rect '->point) (up 'x0 'y0))))
  466. #| Result:
  467. (+ (u^0 (up x0 y0)) (* -1 (u^1 (up x0 y0))))
  468. |#
  469. |#
  470. #|
  471. ;;; pullback commutes with exterior derivative
  472. (install-coordinates R3-rect (up 'x 'y 'z))
  473. (define R3-rect-chi (R3-rect '->coords))
  474. (define R3-rect-chi-inverse (R3-rect '->point))
  475. (define R3-rect->R (-> (UP Real Real Real) Real))
  476. (define m3 ((R3-rect '->point) (up 'x0 'y0 'z0)))
  477. (define alpha (literal-function 'alpha R3-rect->R))
  478. (define beta (literal-function 'beta R3-rect->R))
  479. (define gamma (literal-function 'gamma R3-rect->R))
  480. (define theta
  481. (+ (* (compose alpha R3-rect-chi) dx)
  482. (* (compose beta R3-rect-chi) dy)
  483. (* (compose gamma R3-rect-chi) dz)))
  484. (define R2-chi (R2-rect '->coords))
  485. (define R2-chi-inverse (R2-rect '->point))
  486. (define R2-rect->R (-> (UP Real Real) Real))
  487. (define X2 (literal-vector-field 'X R2-rect))
  488. (define Y2 (literal-vector-field 'Y R2-rect))
  489. (define m2 ((R2-rect '->point) (up 'u0 'v0)))
  490. (define mu
  491. (compose R3-rect-chi-inverse
  492. (up (literal-function 'mu^x R2-rect->R)
  493. (literal-function 'mu^y R2-rect->R)
  494. (literal-function 'mu^z R2-rect->R))
  495. R2-chi))
  496. ;;; first pullback a function
  497. (define f
  498. (compose (literal-function 'f R3-rect->R)
  499. R3-rect-chi))
  500. (pec
  501. (((- ((pullback mu) (d f))
  502. (d ((pullback mu) f)))
  503. X2)
  504. m2))
  505. #| Result:
  506. 0
  507. |#
  508. ;;; now pullback a form
  509. (pec (R3-rect-chi (mu m2)))
  510. #| Result:
  511. (up (mu^x (up u0 v0)) (mu^y (up u0 v0)) (mu^z (up u0 v0)))
  512. |#
  513. (pec ((((pullback mu) theta) X2) m2))
  514. #| Result:
  515. (+
  516. (* (((partial 0) mu^x) (up u0 v0))
  517. (alpha (up (mu^x (up u0 v0)) (mu^y (up u0 v0)) (mu^z (up u0 v0))))
  518. (X^0 (up u0 v0)))
  519. (* (((partial 1) mu^x) (up u0 v0))
  520. (alpha (up (mu^x (up u0 v0)) (mu^y (up u0 v0)) (mu^z (up u0 v0))))
  521. (X^1 (up u0 v0)))
  522. (* (((partial 0) mu^y) (up u0 v0))
  523. (beta (up (mu^x (up u0 v0)) (mu^y (up u0 v0)) (mu^z (up u0 v0))))
  524. (X^0 (up u0 v0)))
  525. (* (((partial 1) mu^y) (up u0 v0))
  526. (beta (up (mu^x (up u0 v0)) (mu^y (up u0 v0)) (mu^z (up u0 v0))))
  527. (X^1 (up u0 v0)))
  528. (* (((partial 0) mu^z) (up u0 v0))
  529. (X^0 (up u0 v0))
  530. (gamma (up (mu^x (up u0 v0)) (mu^y (up u0 v0)) (mu^z (up u0 v0)))))
  531. (* (((partial 1) mu^z) (up u0 v0))
  532. (gamma (up (mu^x (up u0 v0)) (mu^y (up u0 v0)) (mu^z (up u0 v0))))
  533. (X^1 (up u0 v0))))
  534. |#
  535. (pec
  536. (((- ((pullback mu) (d theta))
  537. (d ((pullback mu) theta)))
  538. X2 Y2)
  539. m2))
  540. #| Result:
  541. 0
  542. |#
  543. ;;; works.
  544. |#
  545. #|
  546. ;;; Pullback commutes with wedge
  547. (pec
  548. (let ((theta (literal-1form-field 'theta R3-rect))
  549. (phi (literal-1form-field 'phi R3-rect)))
  550. (((- (wedge ((pullback mu) theta) ((pullback mu) phi))
  551. ((pullback mu) (wedge theta phi)))
  552. X2
  553. Y2)
  554. m2)))
  555. #| Result:
  556. 0
  557. |#
  558. (pec
  559. (let ((theta (literal-manifold-function 'f R3-rect))
  560. (phi (literal-1form-field 'phi R3-rect)))
  561. (((- (wedge ((pullback mu) theta) ((pullback mu) phi))
  562. ((pullback mu) (wedge theta phi)))
  563. X2)
  564. m2)))
  565. #| Result:
  566. 0
  567. |#
  568. |#