Emmy, the Algebra System: Differential Geometry Chapter Nine

Functional Differential Geometry: Chapter 9

Author

Affiliation

Published

April 3, 2026

9 Metrics

We often want to impose further structure on a manifold to allow us to define lengths and angles. This is done by generalizing the idea of the Euclidean dot product, which allows us to compute lengths of vectors and angles between vectors in traditional vector algebra.

lower is already defined in environment

(comment
  (define ((lower metric) u)
    (define (omega v) (metric v u))
    (ff/procedure->oneform-field omega))
  :end-comment)

(define (contract proc basis)
  (let ((vector-basis (basis->vector-basis basis))
        (oneform-basis (basis->oneform-basis basis)))
    (s/sumr proc vector-basis oneform-basis)))

(define (raise metric basis)
  (let ((gi (invert metric basis)))
    (lambda (omega)
            (contract (lambda (e_i w↑i)
                              (* (gi omega w↑i) e_i))
                      basis))))

Metric Compatibility

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

ERR

WARNING: S2-spherical already refers to: #'emmy.env/S2-spherical in namespace: mentat-collective.emmy.fdg-ch09, being replaced by: #'mentat-collective.emmy.fdg-ch09/S2-spherical
WARNING: phi already refers to: #'emmy.env/phi in namespace: mentat-collective.emmy.fdg-ch09, being replaced by: #'mentat-collective.emmy.fdg-ch09/phi

(define ((g-sphere R) u v)
  (* (square R)
     (+ (* (dtheta u) (dtheta v))
        (* (compose (square sin) theta)
           (dphi u)
           (dphi v)))))

(define S2-basis
  (coordinate-system->basis S2-spherical))

(print-expression
  ((Christoffel->symbols
     (metric->Christoffel-1 (g-sphere 'R) S2-basis))
   ((point S2-spherical) (up 'theta0 'phi0))))

(down (down (down 0 0) (down 0 (* (expt R 2) (cos theta0) (sin theta0)))) (down (down 0 (* (expt R 2) (cos theta0) (sin theta0))) (down (* -1N (expt R 2) (cos theta0) (sin theta0)) 0)))

(print-expression
  ((Christoffel->symbols
     (metric->Christoffel-2 (g-sphere 'R) S2-basis))
   ((point S2-spherical) (up 'theta0 'phi0))))

(down (down (up 0 0) (up 0 (/ (cos theta0) (sin theta0)))) (down (up 0 (/ (cos theta0) (sin theta0))) (up (* -1N (cos theta0) (sin theta0)) 0)))

Metrics and Lagrange Equations

(define (metric->Lagrangian metric coordsys)
  (define (L state)
    (let ((q (ref state 1)) (qd (ref state 2)))
      (define v
        (components->vector-field (lambda (m) qd) coordsys))
      ((* 1/2 (metric v v)) ((point coordsys) q))))
  L)

(define (Lagrange-explicit L)
  (let ((P ((partial 2) L))
        (F ((partial 1) L)))
    (/ (- F (+ ((partial 0) P)
               (* ((partial 1) P) velocity)))
       ((partial 2) P))))

(print-expression
  (let-scheme ((metric (literal-metric 'g R3-rect))
               (q (typical-coords R3-rect))
               (L2 (metric->Lagrangian metric R3-rect)))
    (+ (* 1/2
          (((expt (partial 2) 2) (Lagrange-explicit L2))
           (up 't q (corresponding-velocities q))))
       ((Christoffel->symbols
          (metric->Christoffel-2 metric
                                 (coordinate-system->basis R3-rect)))
        ((point R3-rect) q)))))

(down (down (up 0 0 0) (up 0 0 0) (up 0 0 0)) (down (up 0 0 0) (up 0 0 0) (up 0 0 0)) (down (up 0 0 0) (up 0 0 0) (up 0 0 0)))

For Two Dimensions

(define L2
  (metric->Lagrangian (literal-metric 'm R2-rect)
                      R2-rect))

(define (L1 state)
  (sqrt (* 2 (L2 state))))

(print-expression
  (determinant
    (((partial 2) ((partial 2) L2))
     (up 't (up 'x 'y) (up 'vx 'vy)))))

(+ (* (m_00 (up x y)) (m_11 (up x y))) (* -1N (expt (m_01 (up x y)) 2)))

(print-expression
  (determinant
    (((partial 2) ((partial 2) L1))
     (up 't (up 'x 'y) (up 'vx 'vy)))))

(define (L1 state)
  (sqrt (square (velocity state))))

(print-expression
  (((Lagrange-equations L1)
    (up (literal-function 'x) (literal-function 'y)))
   't))

(down (/ (+ (* (((expt D 2) x) t) (expt ((D y) t) 2)) (* -1 (((expt D 2) y) t) ((D x) t) ((D y) t))) (+ (* (expt ((D x) t) 2) (sqrt (+ (expt ((D x) t) 2) (expt ((D y) t) 2)))) (* (expt ((D y) t) 2) (sqrt (+ (expt ((D x) t) 2) (expt ((D y) t) 2)))))) (/ (+ (* -1 (((expt D 2) x) t) ((D x) t) ((D y) t)) (* (((expt D 2) y) t) (expt ((D x) t) 2))) (+ (* (expt ((D x) t) 2) (sqrt (+ (expt ((D x) t) 2) (expt ((D y) t) 2)))) (* (expt ((D y) t) 2) (sqrt (+ (expt ((D x) t) 2) (expt ((D y) t) 2)))))))

Reparametrization

(print-expression
  (let-scheme ((x (literal-function 'x))
               (y (literal-function 'y))
               (f (literal-function 'f))
               (E1 (Euler-Lagrange-operator L1)))
    ((- (compose E1
                 (Gamma (up (compose x f)
                            (compose y f))
                        4))
        (* (compose E1
                    (Gamma (up x y) 4)
                    f)
           (D f)))
     't)))

OUT

2026-04-03T12:14:21.685Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? (+ (expt ((D x) (f t)) 2) (expt ((D y) (f t)) 2))) in c1
2026-04-03T12:14:21.686Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? (+ (* (expt ((D x) (f t)) 2) (expt ((D f) t) 2)) (* (expt ((D f) t) 2) (expt ((D y) (f t)) 2)))) in c1
2026-04-03T12:14:21.686Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? (+ (expt ((D x) (f t)) 2) (expt ((D y) (f t)) 2))) in c1
2026-04-03T12:14:21.686Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? (+ (* (expt ((D x) (f t)) 2) (expt ((D f) t) 2)) (* (expt ((D f) t) 2) (expt ((D y) (f t)) 2)))) in c1
2026-04-03T12:14:21.693Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? ((D f) t)) in root-out-squares
2026-04-03T12:14:21.694Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? ((D f) t)) in root-out-squares
2026-04-03T12:14:21.696Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? (+ (* (expt ((D x) (f t)) 2) ((D f) t)) (* ((D f) t) (expt ((D y) (f t)) 2)))) in root-out-squares
2026-04-03T12:14:21.698Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? (+ (* (expt ((D x) (f t)) 2) ((D f) t)) (* ((D f) t) (expt ((D y) (f t)) 2)))) in root-out-squares
2026-04-03T12:14:21.721Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? ((D f) t)) in root-out-squares
2026-04-03T12:14:21.722Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? ((D f) t)) in root-out-squares
2026-04-03T12:14:21.723Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? (+ (* (expt ((D x) (f t)) 2) ((D f) t)) (* ((D f) t) (expt ((D y) (f t)) 2)))) in root-out-squares
2026-04-03T12:14:21.725Z runnervm727z3 WARN [emmy.util.logic:22] - Assuming (non-negative? (+ (* (expt ((D x) (f t)) 2) ((D f) t)) (* ((D f) t) (expt ((D y) (f t)) 2)))) in root-out-squares

(down 0 0)

(print-expression
  (let-scheme ((q (up (literal-function 'x) (literal-function 'y)))
               (f (literal-function 'f)))
    ((- (compose (Euler-Lagrange-operator L2)
                 (Gamma (compose q f) 4))
        (* (compose (Euler-Lagrange-operator L2)
                    (Gamma q 4)
                    f)
           (expt (D f) 2)))
     't)))

(down (+ (* ((D x) (f t)) (((expt D 2) f) t) (m_00 (up (x (f t)) (y (f t))))) (* ((D y) (f t)) (((expt D 2) f) t) (m_01 (up (x (f t)) (y (f t)))))) (+ (* ((D x) (f t)) (((expt D 2) f) t) (m_01 (up (x (f t)) (y (f t))))) (* ((D y) (f t)) (((expt D 2) f) t) (m_11 (up (x (f t)) (y (f t)))))))

Exercise 9.3: Curvature of a Spherical Surface

(define M (make-manifold S2-type 2 3))

(define spherical
  (coordinate-system-at M :spherical :north-pole))

(define-coordinates (up theta phi) spherical)

(define spherical-basis (coordinate-system->basis spherical))

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

[KLM:] the below trace2down is too simple for further use you need to revert to e/trace2down for actual use

(define ((trace2down-simple metric-tensor basis) tensor)
  (let ((inverse-metric-tensor
          (invert metric-tensor basis)))
    (contract
      (lambda (v1 w1)
              (contract
                (lambda (v w)
                        (* (inverse-metric-tensor w1 w)
                           (tensor v v1)))
                basis))
      basis)))

General Relativity

Exercise 9.5: Newton’s Equations

(define-coordinates [t x y z] spacetime-rect)

ERR

WARNING: spacetime-rect already refers to: #'emmy.env/spacetime-rect in namespace: mentat-collective.emmy.fdg-ch09, being replaced by: #'mentat-collective.emmy.fdg-ch09/spacetime-rect

(define spacetime-rect-basis
  (coordinate-system->basis spacetime-rect))

(define (Newton-metric M G c V)
  (let ((a
          (+ 1 (* (/ 2 (square c))
                  (compose V (up x y z))))))
    (define (g v1 v2)
      (+ (* -1 (square c) a (dt v1) (dt v2))
         (* (dx v1) (dx v2))
         (* (dy v1) (dy v2))
         (* (dz v1) (dz v2))))
    g))

(define (Newton-connection M G c V)
  (Christoffel->Cartan
    (metric->Christoffel-2 (Newton-metric M G c V)
                           spacetime-rect-basis)))

(define V (literal-function 'V '(-> (UP Real Real Real) Real)))

(define nabla
  (covariant-derivative
    (Newton-connection 'M 'G 'c (literal-function 'V '(-> (UP Real Real Real) Real)))))

(print-expression
  (((Ricci nabla (coordinate-system->basis spacetime-rect))
    d:dt d:dt)
   ((point spacetime-rect) (up 't 'x 'y 'z))))

(/ (+ (* (expt c 2) (((expt (partial 0) 2) V) (up x y z))) (* (expt c 2) (((expt (partial 1) 2) V) (up x y z))) (* (expt c 2) (((expt (partial 2) 2) V) (up x y z))) (* -1N (expt (((partial 0) V) (up x y z)) 2)) (* 2 (V (up x y z)) (((expt (partial 0) 2) V) (up x y z))) (* 2 (V (up x y z)) (((expt (partial 1) 2) V) (up x y z))) (* 2 (V (up x y z)) (((expt (partial 2) 2) V) (up x y z))) (* -1N (expt (((partial 1) V) (up x y z)) 2)) (* -1N (expt (((partial 2) V) (up x y z)) 2))) (+ (expt c 2) (* 2N (V (up x y z)))))

(print-expression
  (+ (((partial 0) ((partial 0) V)) (up 'x 'y 'z))
     (((partial 1) ((partial 1) V)) (up 'x 'y 'z))
     (((partial 2) ((partial 2) V)) (up 'x 'y 'z))))

(+ (((expt (partial 0) 2) V) (up x y z)) (((expt (partial 1) 2) V) (up x y z)) (((expt (partial 2) 2) V) (up x y z)))

(define (Tdust rho)
  (define (T w1 w2)
    (* rho (w1 d:dt) (w2 d:dt)))
  T)

(print-expression
  (let-scheme ((g (Newton-metric 'M 'G 'c V)))
    (let ((T_ij ((drop2 g spacetime-rect-basis) (Tdust 'rho))))
      (let ((T ((e/trace2down g spacetime-rect-basis) T_ij)))
        ((- (T_ij d:dt d:dt) (* (/ 1 2) T (g d:dt d:dt)))
         ((point spacetime-rect) (up 't 'x 'y 'z)))))))

(+ (* 1/2 (expt c 4) rho) (* 2N (expt c 2) rho (V (up x y z))) (* 2N rho (expt (V (up x y z)) 2)))

Exercise 9.6: Curvature of Schwarzschild Spacetime

(define-coordinates (up t r theta phi) spacetime-sphere)

ERR

WARNING: spacetime-sphere already refers to: #'emmy.env/spacetime-sphere in namespace: mentat-collective.emmy.fdg-ch09, being replaced by: #'mentat-collective.emmy.fdg-ch09/spacetime-sphere

(define (Schwarzschild-metric M G c)
  (let ((a (- 1 (/ (* 2 G M) (* (square c) r)))))
    (lambda (v1 v2)
            (+ (* -1 (square c) a (dt v1) (dt v2))
               (* (/ 1 a) (dr v1) (dr v2))
               (* (square r)
                  (+ (* (dtheta v1) (dtheta v2))
                     (* (square (sin theta))
                        (dphi v1) (dphi v2))))))))

Exercise 9.7: Circular Orbits in Schwarzschild Spacetime

(define (prime-meridian r omega)
  (compose (point spacetime-sphere)
           (lambda (t) (up t r (* omega t) 0))
           (chart R1-rect)))

Exercise 9.9: Friedmann-Lemaître-Robertson-Walker

(define (Einstein coordinate-system metric-tensor)
  (let ((basis (coordinate-system->basis coordinate-system))
         (connection
           (Christoffel->Cartan
             (metric->Christoffel-2 metric-tensor basis)))
         (nabla (covariant-derivative connection))
         (Ricci-tensor (Ricci nabla basis))
         (Ricci-scalar
           ((trace2down metric-tensor basis) Ricci-tensor)))
    (define (Einstein-tensor v1 v2)
      (- (Ricci-tensor v1 v2)
         (* 1/2 Ricci-scalar (metric-tensor v1 v2))))
    Einstein-tensor))

(define (Einstein-field-equation
          coordinate-system metric-tensor Lambda stress-energy-tensor)
  (let ((Einstein-tensor
          (Einstein coordinate-system metric-tensor)))
    (define EFE-residuals
      (- (+ Einstein-tensor (* Lambda metric-tensor))
         (* (/ (* 8 'pi 'G) (expt 'c 4))
            stress-energy-tensor)))
    EFE-residuals))

(define (FLRW-metric c k R)
  (let ((a (/ (square (compose R t)) (- 1 (* k (square r)))))
        (b (square (* (compose R t) r))))
    (define (g v1 v2)
      (+ (* -1 (square c) (dt v1) (dt v2))
         (* a (dr v1) (dr v2))
         (* b (+ (* (dtheta v1) (dtheta v2))
                 (* (square (sin theta))
                    (dphi v1) (dphi v2))))))
    g))

(define (Tperfect-fluid rho p c metric)
  (let ((basis (coordinate-system->basis spacetime-sphere))
         (inverse-metric (metric:invert metric basis)))
    (define (T w1 w2)
      (+ (* (+ (compose rho t)
               (/ (compose p t) (square c)))
            (w1 d:dt) (w2 d:dt))
         (* (compose p t) (inverse-metric w1 w2))))
    T))

(repl/scittle-sidebar)

source: src/mentat_collective/emmy/fdg_ch09.clj