euler-form-of-S2.egi

declare symbol r, θ, φ: MathValue

-- Euler form of S2

def x : Vector MathValue := [| θ, φ |]

def X : Vector MathValue := [| r * sin θ * cos φ, r * sin θ * sin φ, r * cos θ |]

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

-- Metric tensor
def g_i_j : Matrix MathValue := generateTensor (\[x, y] -> V.* e_x_# e_y_#) [2, 2]
def g~i~j : Matrix MathValue := M.inverse g_#_#

assertEqual "Metric tensor"
  g_#_#
  [| [| r^2, 0 |], [| 0, r^2 * (sin θ)^2 |] |]_#_#

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

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

-- Vielbein (orthonormal frame)
def A : Matrix MathValue := [| [| 1 / r, 0 |], [| 0, 1 / (r * sin θ) |] |]

-- Exterior derivative (paper canonical: !(flip ∂/∂) x t with disjoint index completion)
def d (t : Tensor MathValue) : Tensor MathValue := !(flip ∂/∂) x t

-- Connection 1-form in coordinate basis (paper canonical: ω~i_j := Γ~i_j_#)
def ω0~i_j : Matrix MathValue := Γ~i_j_#

-- Connection 1-form in orthonormal basis (Cartan transformation):
--   ω = A⁻¹ ω₀ A + A⁻¹ dA
def ω~i_j : Tensor MathValue := withSymbols [a, b]
  (M.inverse A)~i_a . ω0~a_b . A~b_j + (M.inverse A)~i_a . d A~a_j

-- Curvature 2-form (Cartan structure equation)
def Ω~i_j : Tensor MathValue := withSymbols [k]
  antisymmetrize (d ω~i_j + ω~i_k ∧ ω~k_j)

-- Euler form: e(S²) = (1/(2π)) (Ω₁² - Ω²₁)
-- The withSymbols on the form indices is needed so the binary minus
-- aligns the two rank-2 form components correctly.
def eulerForm : Tensor MathValue :=
  (1 / (2 * π)) * withSymbols [t1, t2] (Ω~1_2_t1_t2 - Ω~2_1_t1_t2)

-- The Euler form integrates to the Euler characteristic χ = 2 for S²
assertEqual "Euler form of S2"
  eulerForm
  [| [| 0, sin θ / (2 * π) |], [| - sin θ / (2 * π), 0 |] |]