egison-5.1.0: sample/math/geometry/riemann-curvature-tensor-of-S2xS3.egi

-- Riemann curvature tensor of S2 x S3 (product manifold)

declare symbol φ, θ, ψ, y, α, a

def x := [| φ, θ, ψ, y, α |]

def g_i_j :=
  [| [| (3 * `(1 + (- y))^2 * (sin θ)^2 * `(a + (- (y^2))) +
         2 * `(a + (-3) * y^2 + 2 * y^3) * (cos θ)^2 * `(1 + (- y)) +
         `(a + (-2) * y + y^2)^2 * (cos θ)^2) /
        (18 * `(a + (- (y^2))) * `(1 + (- y)))
      , 0
      , ((-2) * `(a + (-3) * y^2 + 2 * y^3) * cos θ * `(1 + (- y)) +
         (- (`(a + (-2) * y + y^2)^2)) * cos θ) /
        (18 * `(a + (- (y^2))) * `(1 + (- y)))
      , 0
      , (- `(a + (-2) * y + y^2)) * cos θ / (3 * `(1 + (- y)))
      |]
   , [| 0, `(1 + (- y)) / 6, 0, 0, 0 |]
   , [| ((-2) * `(a + (-3) * y^2 + 2 * y^3) * cos θ * `(1 + (- y)) +
         (- (`(a + (-2) * y + y^2)^2)) * cos θ) /
        (18 * `(a + (- (y^2))) * `(1 + (- y)))
      , 0
      , (2 * `(a + (-3) * y^2 + 2 * y^3) * `(1 + (- y)) +
         `(a + (-2) * y + y^2)^2) / (18 * `(a + (- (y^2))) * `(1 + (- y)))
      , 0
      , 1 * `(a + (-2) * y + y^2) / (3 * `(1 + (- y)))
      |]
   , [| 0, 0, 0, `(1 + (- y)) / (2 * `(a + (-3) * y^2 + 2 * y^3)), 0 |]
   , [| (- `(a + (-2) * y + y^2)) * cos θ / (3 * `(1 + (- y)))
      , 0
      , 1 * `(a + (-2) * y + y^2) / (3 * `(1 + (- y)))
      , 0
      , 2 * `(a + (- (y^2))) / `(1 + (- y))
      |]
   |]_#_#

def g~i~j := M.inverse g_#_#

-- Christoffel symbols
def Γ_i_j_k := (1 / 2) * (∂/∂ g_i_k x~j + ∂/∂ g_i_j x~k - ∂/∂ g_j_k x~i)

def Γ~i_j_k := withSymbols [m]
  g~i~m . Γ_m_j_k

-- Riemann curvature
def R~i_j_k_l := withSymbols [m]
  ∂/∂ Γ~i_j_l x~k - ∂/∂ Γ~i_j_k x~l + Γ~m_j_l . Γ~i_m_k - Γ~m_j_k . Γ~i_m_l

-- Ricci curvature
def Ric_i_j := withSymbols [m]
  sum (contract R~m_i_m_j)

-- The Einstein condition: Ric_ij = 4 * g_ij
-- Check Einstein condition by computing Ric - 4*g
assertEqual "Einstein condition (Ric - 4*g = 0)"
  (expandAll' (withSymbols [i, j] Ric_i_j -' 4 *' g_i_j))
  [| [| 0, 0, 0, 0, 0 |]
   , [| 0, 0, 0, 0, 0 |]
   , [| 0, 0, 0, 0, 0 |]
   , [| 0, 0, 0, 0, 0 |]
   , [| 0, 0, 0, 0, 0 |]
   |]_#_#