Emmy, the Algebra System: Differential Geometry Chapter Ten

Functional Differential Geometry: Chapter 10

Author

Affiliation

Markus Agwin Kloimwieder

Scicloj

Published

April 4, 2026

10 Hodge Star and Electrodynamics

The Hodge dual is useful for the elegant formalization of electrodynamics.

(define (gradient metric basis)
  (compose (raise metric basis) d))

(define (curl metric orthonormal-basis)
  (let ((star (Hodge-star metric orthonormal-basis))
        (sharp (raise metric orthonormal-basis))
        (flat (lower metric)))
    (compose sharp star d flat)))

(define (divergence metric orthonormal-basis)
  (let ((star (Hodge-star metric orthonormal-basis))
        (flat (lower metric)))
    (compose star d star flat)))

(define (((divergence-c Cartan) v) point)
  (let ((basis (Cartan->basis Cartan))
        (nabla (covariant-derivative Cartan)))
    (contract
      (lambda (ei wi)
              ((wi ((nabla ei) v)) point))
      basis)))

(define (Laplacian metric orthonormal-basis)
  (compose (divergence metric orthonormal-basis)
           (gradient metric orthonormal-basis)))

(define spherical R3-rect)

(define-coordinates (up r theta phi) spherical)

(define R3-spherical-point
  ((point spherical) (up 'r0 'theta0 'phi0)))

(define (spherical-metric v1 v2)
  (+ (* (dr v1) (dr v2))
     (* (square r)
        (+ (* (dtheta v1) (dtheta v2))
           (* (expt (sin theta) 2)
              (dphi v1) (dphi v2))))))

(define e_0 d:dr)

(define e_1 (* (/ 1 r) d:dtheta))

(define e_2 (* (/ 1 (* r (sin theta))) d:dphi))

(define orthonormal-spherical-vector-basis
  (down e_0 e_1 e_2))

(define orthonormal-spherical-oneform-basis
  (vector-basis->dual orthonormal-spherical-vector-basis
                      spherical))

(define orthonormal-spherical-basis
  (make-basis orthonormal-spherical-vector-basis
              orthonormal-spherical-oneform-basis))

(print-expression
  ((orthonormal-spherical-oneform-basis
     ((gradient spherical-metric orthonormal-spherical-basis)
      (literal-manifold-function 'f spherical)))
   R3-spherical-point))

(up (((partial 0) f) (up r0 theta0 phi0)) (/ (((partial 1) f) (up r0 theta0 phi0)) r0) (/ (((partial 2) f) (up r0 theta0 phi0)) (* r0 (sin theta0))))

(define v
  (+ (* (literal-manifold-function 'v↑0 spherical) e_0)
     (* (literal-manifold-function 'v↑1 spherical) e_1)
     (* (literal-manifold-function 'v↑2 spherical) e_2)))

(print-expression
  ((orthonormal-spherical-oneform-basis
     ((curl spherical-metric orthonormal-spherical-basis) v))
   R3-spherical-point))

(up (/ (+ (* (cos theta0) (v↑2 (up r0 theta0 phi0))) (* (sin theta0) (((partial 1) v↑2) (up r0 theta0 phi0))) (* -1 (((partial 2) v↑1) (up r0 theta0 phi0)))) (* r0 (sin theta0))) (/ (+ (* -1 r0 (sin theta0) (((partial 0) v↑2) (up r0 theta0 phi0))) (* -1 (sin theta0) (v↑2 (up r0 theta0 phi0))) (((partial 2) v↑0) (up r0 theta0 phi0))) (* r0 (sin theta0))) (/ (+ (* r0 (((partial 0) v↑1) (up r0 theta0 phi0))) (v↑1 (up r0 theta0 phi0)) (* -1 (((partial 1) v↑0) (up r0 theta0 phi0)))) r0))

(print-expression
  (((divergence spherical-metric orthonormal-spherical-basis) v)
   R3-spherical-point))

(/ (+ (* r0 (sin theta0) (((partial 0) v↑0) (up r0 theta0 phi0))) (* (cos theta0) (v↑1 (up r0 theta0 phi0))) (* 2 (sin theta0) (v↑0 (up r0 theta0 phi0))) (* (sin theta0) (((partial 1) v↑1) (up r0 theta0 phi0))) (((partial 2) v↑2) (up r0 theta0 phi0))) (* r0 (sin theta0)))

(print-expression
  (((Laplacian spherical-metric orthonormal-spherical-basis)
    (literal-manifold-function 'f spherical))
   R3-spherical-point))

(/ (+ (* (expt r0 2) (expt (sin theta0) 2) (((expt (partial 0) 2) f) (up r0 theta0 phi0))) (* 2 r0 (expt (sin theta0) 2) (((partial 0) f) (up r0 theta0 phi0))) (* (cos theta0) (sin theta0) (((partial 1) f) (up r0 theta0 phi0))) (* (expt (sin theta0) 2) (((expt (partial 1) 2) f) (up r0 theta0 phi0))) (((expt (partial 2) 2) f) (up r0 theta0 phi0))) (* (expt r0 2) (expt (sin theta0) 2)))

The Wave Equation

(define SR R4-rect)

(define-coordinates (up ct x y z) SR)

(define an-event ((point SR) (up 'ct0 'x0 'y0 'z0)))

(define a-vector
  (+ (* (literal-manifold-function 'v↑t SR) d:dct)
     (* (literal-manifold-function 'v↑x SR) d:dx)
     (* (literal-manifold-function 'v↑y SR) d:dy)
     (* (literal-manifold-function 'v↑z SR) d:dz)))

(define (g-Minkowski u v)
  (+ (* -1 (dct u) (dct v))
     (* (dx u) (dx v))
     (* (dy u) (dy v))
     (* (dz u) (dz v))))

(print-expression
  ((g-Minkowski a-vector a-vector) an-event))

(+ (* -1 (expt (v↑t (up ct0 x0 y0 z0)) 2)) (expt (v↑x (up ct0 x0 y0 z0)) 2) (expt (v↑y (up ct0 x0 y0 z0)) 2) (expt (v↑z (up ct0 x0 y0 z0)) 2))

(define SR-vector-basis (coordinate-system->vector-basis SR))

((g-Minkowski SR-vector-basis SR-vector-basis) an-event)

(down (down -1 0 0 0) (down 0 1 0 0) (down 0 0 1 0) (down 0 0 0 1))

(define p (literal-manifold-function 'phi SR))

(define SR-vector-basis (down (* (/ 1 'c) d:dct) d:dx d:dy d:dz))

(define SR-oneform-basis (up (* 'c dct) dx dy dz))

(define SR-basis
  (make-basis SR-vector-basis
              SR-oneform-basis))

(print-expression
  (((Laplacian g-Minkowski SR-basis) p) an-event))

(/ (+ (* -1 (expt c 4) (((expt (partial 1) 2) phi) (up ct0 x0 y0 z0))) (* -1 (expt c 4) (((expt (partial 2) 2) phi) (up ct0 x0 y0 z0))) (* -1 (expt c 4) (((expt (partial 3) 2) phi) (up ct0 x0 y0 z0))) (((expt (partial 0) 2) phi) (up ct0 x0 y0 z0))) (expt c 6))

Electrodynamics

(define (Faraday Ex Ey Ez Bx By Bz)
  (+ (* Ex (wedge dx dct))
     (* Ey (wedge dy dct))
     (* Ez (wedge dz dct))
     (* Bx (wedge dy dz))
     (* By (wedge dz dx))
     (* Bz (wedge dx dy))))

(define (Maxwell Ex Ey Ez Bx By Bz)
  (+ (* -1 Bx (wedge dx dct))
     (* -1 By (wedge dy dct))
     (* -1 Bz (wedge dz dct))
     (* Ex (wedge dy dz))
     (* Ey (wedge dz dx))
     (* Ez (wedge dx dy))))

(define SR-star (Hodge-star g-Minkowski SR-basis))

(print-expression
  (((- (SR-star (Faraday 'Ex 'Ey 'Ez 'Bx 'By 'Bz))
       (Maxwell 'Ex 'Ey 'Ez 'Bx 'By 'Bz))
    (literal-vector-field 'u SR)
    (literal-vector-field 'v SR))
   an-event))

(/ (+ (* -1 Bx (expt c 4) (u↑1 (up ct0 x0 y0 z0)) (v↑0 (up ct0 x0 y0 z0))) (* Bx (expt c 4) (v↑1 (up ct0 x0 y0 z0)) (u↑0 (up ct0 x0 y0 z0))) (* -1 By (expt c 4) (v↑0 (up ct0 x0 y0 z0)) (u↑2 (up ct0 x0 y0 z0))) (* By (expt c 4) (u↑0 (up ct0 x0 y0 z0)) (v↑2 (up ct0 x0 y0 z0))) (* -1 Bz (expt c 4) (v↑0 (up ct0 x0 y0 z0)) (u↑3 (up ct0 x0 y0 z0))) (* Bz (expt c 4) (u↑0 (up ct0 x0 y0 z0)) (v↑3 (up ct0 x0 y0 z0))) (* Bx (expt c 3) (u↑1 (up ct0 x0 y0 z0)) (v↑0 (up ct0 x0 y0 z0))) (* -1 Bx (expt c 3) (v↑1 (up ct0 x0 y0 z0)) (u↑0 (up ct0 x0 y0 z0))) (* By (expt c 3) (v↑0 (up ct0 x0 y0 z0)) (u↑2 (up ct0 x0 y0 z0))) (* -1 By (expt c 3) (u↑0 (up ct0 x0 y0 z0)) (v↑2 (up ct0 x0 y0 z0))) (* Bz (expt c 3) (v↑0 (up ct0 x0 y0 z0)) (u↑3 (up ct0 x0 y0 z0))) (* -1 Bz (expt c 3) (u↑0 (up ct0 x0 y0 z0)) (v↑3 (up ct0 x0 y0 z0))) (* -1 Ex (expt c 3) (u↑2 (up ct0 x0 y0 z0)) (v↑3 (up ct0 x0 y0 z0))) (* Ex (expt c 3) (v↑2 (up ct0 x0 y0 z0)) (u↑3 (up ct0 x0 y0 z0))) (* Ey (expt c 3) (u↑1 (up ct0 x0 y0 z0)) (v↑3 (up ct0 x0 y0 z0))) (* -1 Ey (expt c 3) (v↑1 (up ct0 x0 y0 z0)) (u↑3 (up ct0 x0 y0 z0))) (* -1 Ez (expt c 3) (u↑1 (up ct0 x0 y0 z0)) (v↑2 (up ct0 x0 y0 z0))) (* Ez (expt c 3) (v↑1 (up ct0 x0 y0 z0)) (u↑2 (up ct0 x0 y0 z0))) (* Ex (u↑2 (up ct0 x0 y0 z0)) (v↑3 (up ct0 x0 y0 z0))) (* -1 Ex (v↑2 (up ct0 x0 y0 z0)) (u↑3 (up ct0 x0 y0 z0))) (* -1 Ey (u↑1 (up ct0 x0 y0 z0)) (v↑3 (up ct0 x0 y0 z0))) (* Ey (v↑1 (up ct0 x0 y0 z0)) (u↑3 (up ct0 x0 y0 z0))) (* Ez (u↑1 (up ct0 x0 y0 z0)) (v↑2 (up ct0 x0 y0 z0))) (* -1 Ez (v↑1 (up ct0 x0 y0 z0)) (u↑2 (up ct0 x0 y0 z0)))) (expt c 3))

(define (J charge-density Ix Iy Iz)
  (- (* (/ 1 'c) (+ (* Ix dx) (* Iy dy) (* Iz dz)))
     (* charge-density 'c dct)))

(define F
  (Faraday (literal-manifold-function 'Ex SR)
           (literal-manifold-function 'Ey SR)
           (literal-manifold-function 'Ez SR)
           (literal-manifold-function 'Bx SR)
           (literal-manifold-function 'By SR)
           (literal-manifold-function 'Bz SR)))

(define four-current
  (J (literal-manifold-function 'rho SR)
     (literal-manifold-function 'Ix SR)
     (literal-manifold-function 'Iy SR)
     (literal-manifold-function 'Iz SR)))

Maxwell’s Equations

(print-expression
  (((d F) d:dx d:dy d:dz) an-event))

(+ (((partial 1) Bx) (up ct0 x0 y0 z0)) (((partial 2) By) (up ct0 x0 y0 z0)) (((partial 3) Bz) (up ct0 x0 y0 z0)))

(print-expression
  (((d F) d:dct d:dy d:dz) an-event))

(+ (((partial 0) Bx) (up ct0 x0 y0 z0)) (((partial 2) Ez) (up ct0 x0 y0 z0)) (* -1 (((partial 3) Ey) (up ct0 x0 y0 z0))))

(print-expression
  (((d F) d:dct d:dz d:dx) an-event))

(+ (((partial 0) By) (up ct0 x0 y0 z0)) (((partial 3) Ex) (up ct0 x0 y0 z0)) (* -1 (((partial 1) Ez) (up ct0 x0 y0 z0))))

(print-expression
  (((d F) d:dct d:dx d:dy) an-event))

(+ (((partial 0) Bz) (up ct0 x0 y0 z0)) (((partial 1) Ey) (up ct0 x0 y0 z0)) (* -1 (((partial 2) Ex) (up ct0 x0 y0 z0))))

(print-expression
  (((- (d (SR-star F)) (* 4 'pi (SR-star four-current)))
    d:dx d:dy d:dz)
   an-event))

(/ (+ (* -4 c pi (rho (up ct0 x0 y0 z0))) (((partial 1) Ex) (up ct0 x0 y0 z0)) (((partial 2) Ey) (up ct0 x0 y0 z0)) (((partial 3) Ez) (up ct0 x0 y0 z0))) (expt c 3))

(print-expression
  (((- (d (SR-star F)) (* 4 'pi (SR-star four-current)))
    d:dct d:dy d:dz)
   an-event))

(/ (+ (* -1 (expt c 4) (((partial 2) Bz) (up ct0 x0 y0 z0))) (* (expt c 4) (((partial 3) By) (up ct0 x0 y0 z0))) (* 4N (expt c 3) pi (Ix (up ct0 x0 y0 z0))) (((partial 0) Ex) (up ct0 x0 y0 z0))) (expt c 3))

(print-expression
  (((- (d (SR-star F)) (* 4 'pi (SR-star four-current)))
    d:dct d:dz d:dx)
   an-event))

(/ (+ (* -1 (expt c 4) (((partial 3) Bx) (up ct0 x0 y0 z0))) (* (expt c 4) (((partial 1) Bz) (up ct0 x0 y0 z0))) (* 4N (expt c 3) pi (Iy (up ct0 x0 y0 z0))) (((partial 0) Ey) (up ct0 x0 y0 z0))) (expt c 3))

(print-expression
  (((- (d (SR-star F)) (* 4 'pi (SR-star four-current)))
    d:dct d:dx d:dy)
   an-event))

(/ (+ (* -1 (expt c 4) (((partial 1) By) (up ct0 x0 y0 z0))) (* (expt c 4) (((partial 2) Bx) (up ct0 x0 y0 z0))) (* 4N (expt c 3) pi (Iz (up ct0 x0 y0 z0))) (((partial 0) Ez) (up ct0 x0 y0 z0))) (expt c 3))

Lorentz Force

(define E
  (up (literal-manifold-function 'Ex SR)
      (literal-manifold-function 'Ey SR)
      (literal-manifold-function 'Ez SR)))

(define B
  (up (literal-manifold-function 'Bx SR)
      (literal-manifold-function 'By SR)
      (literal-manifold-function 'Bz SR)))

(define V (up 'V_x 'V_y 'V_z))

(print-expression
  (* 'q (+ (E an-event) (cross-product V (B an-event)))))

(up (+ (* V_y q (Bz (up ct0 x0 y0 z0))) (* -1 V_z q (By (up ct0 x0 y0 z0))) (* q (Ex (up ct0 x0 y0 z0)))) (+ (* -1 V_x q (Bz (up ct0 x0 y0 z0))) (* V_z q (Bx (up ct0 x0 y0 z0))) (* q (Ey (up ct0 x0 y0 z0)))) (+ (* V_x q (By (up ct0 x0 y0 z0))) (* -1 V_y q (Bx (up ct0 x0 y0 z0))) (* q (Ez (up ct0 x0 y0 z0)))))

eta-inverse is not defined, so these will not run.

(comment
  (define (Force charge F four-velocity component)
    (* -1 charge
       (contract (lambda (a b)
                         (contract (lambda (e w)
                                           (* (w four-velocity)
                                              (F e a)
                                              (eta-inverse b component)))
                                   SR-basis))
                 SR-basis)))

  (print-expression
    ((Force 'q F d:dct dx) an-event))

  (define (Ux beta)
    (+ (* (/ 1 (sqrt (- 1 (square beta)))) d:dct)
       (* (/ beta (sqrt (- 1 (square beta)))) d:dx)))

  (print-expression
    ((Force 'q F (Ux 'v:c) dy) an-event))

  :end-comment)

(repl/scittle-sidebar)

source: src/mentat_collective/emmy/fdg_ch10.clj