riemann-curvature-tensor-of-S7.egi

-- Riemann curvature tensor of S7

declare symbol α, β, γ, δ, ξ, ζ, η, r : MathValue

def x := [| α, β, γ, δ, ξ, ζ, η |]

def X := [| r * cos α
          , r * sin α * cos β
          , r * sin α * sin β * cos γ
          , r * sin α * sin β * sin γ * cos δ
          , r * sin α * sin β * sin γ * sin δ * cos ξ
          , r * sin α * sin β * sin γ * sin δ * sin ξ * cos ζ
          , r * sin α * sin β * sin γ * sin δ * sin ξ * sin ζ * cos η
          , r * sin α * sin β * sin γ * sin δ * sin ξ * sin ζ * sin η
          |]

-- Local basis
def e_i_j : Matrix MathValue := ∂/∂ X_j x~i

-- Metric tensor
def g_i_j := generateTensor (\[a, b] -> V.* e_a e_b) [7, 7]
def g~i~j := M.inverse g_#_#

assertEqual "Metric tensor g_1_#"
  g_1_#
  [| r^2, 0, 0, 0, 0, 0, 0 |]_#
assertEqual "Metric tensor g_2_#"
  g_2_#
  [| 0, r^2 * (sin α)^2, 0, 0, 0, 0, 0 |]_#

-- 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

assertEqual "Christoffel symbols of the second kind Γ~1_#_#"
  Γ~1_#_#
  [| [| 0, 0, 0, 0, 0, 0, 0 |]
   , [| 0, -1 * sin α * cos α, 0, 0, 0, 0, 0 |]
   , [| 0, 0, -1 * sin α * cos α * (sin β)^2, 0, 0, 0, 0 |]
   , [| 0, 0, 0, -1 * sin α * cos α * (sin β)^2 * (sin γ)^2, 0, 0, 0 |]
   , [| 0, 0, 0, 0, -1 * sin α * cos α * (sin β)^2 * (sin γ)^2 * (sin δ)^2, 0, 0 |]
   , [| 0, 0, 0, 0, 0, -1 * sin α * cos α * (sin β)^2 * (sin γ)^2 * (sin δ)^2 * (sin ξ)^2, 0 |]
   , [| 0, 0, 0, 0, 0, 0, -1 * sin α * cos α * (sin β)^2 * (sin γ)^2 * (sin δ)^2 * (sin ξ)^2 * (sin ζ)^2 |]
   |]_#_#
assertEqual "Christoffel symbols of the second kind Γ~2_#_#"
  Γ~2_#_#
  [| [| 0, (cos α) / (sin α), 0, 0, 0, 0, 0 |]
   , [| (cos α) / (sin α), 0, 0, 0, 0, 0, 0 |]
   , [| 0, 0, -1 * sin β * cos β, 0, 0, 0, 0 |]
   , [| 0, 0, 0, -1 * sin β * cos β * (sin γ)^2, 0, 0, 0 |]
   , [| 0, 0, 0, 0, -1 * sin β * cos β * (sin γ)^2 * (sin δ)^2, 0, 0 |]
   , [| 0, 0, 0, 0, 0, -1 * sin β * cos β * (sin γ)^2 * (sin δ)^2 * (sin ξ)^2, 0 |]
   , [| 0, 0, 0, 0, 0, 0, -1 * sin β * cos β * (sin γ)^2 * (sin δ)^2 * (sin ξ)^2 * (sin ζ)^2 |]
   |]_#_#

-- 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)

assertEqual "Ricci curvature Ric_1_#"
  Ric_1_#
  [| 6, 0, 0, 0, 0, 0, 0 |]_#
assertEqual "Ricci curvature Ric_2_#"
  Ric_2_#
  [| 0, 6 * (sin α)^2, 0, 0, 0, 0, 0 |]_#

-- Scalar curvature
def scalarCurvature := withSymbols [i, j]
  g~i~j . Ric_i_j

-- For S^7, scalar curvature is n(n-1)/r^2 = 7*6/r^2 = 42/r^2
assertEqual "scalar curvature"
  scalarCurvature
  (42 / r^2)