Idx

formal source

  30
  31def spacetime_dim : ℕ := 4
  32
  33abbrev Idx := Fin 4
  34
  35/-! ## Metric Tensor in Coordinates -/
  36
  37/-- A metric tensor in local coordinates: a symmetric 4x4 matrix
  38    at each spacetime point (here abstracted as just the components). -/
  39structure MetricTensor where
  40  g : Idx → Idx → ℝ
  41  symmetric : ∀ mu nu, g mu nu = g nu mu
  42
  43/-- The inverse metric g^{mu nu} (satisfying g^{mu rho} g_{rho nu} = delta^mu_nu). -/
  44structure InverseMetric where
  45  ginv : Idx → Idx → ℝ
  46  symmetric : ∀ mu nu, ginv mu nu = ginv nu mu
  47
  48/-- The flat Minkowski metric eta = diag(-1, +1, +1, +1). -/
  49def minkowski : MetricTensor where
  50  g := fun mu nu => if mu = nu then (if mu = 0 then -1 else 1) else 0
  51  symmetric := by intro mu nu; split_ifs <;> simp_all [eq_comm]
  52
  53/-- The Minkowski inverse equals the Minkowski metric itself. -/
  54def minkowski_inverse : InverseMetric where
  55  ginv := fun mu nu => if mu = nu then (if mu = 0 then -1 else 1) else 0
  56  symmetric := by intro mu nu; split_ifs <;> simp_all [eq_comm]
  57
  58/-! ## Christoffel Symbols -/
  59
  60/-- The Christoffel symbols of the second kind in local coordinates.
  61    Gamma^rho_{mu nu} = (1/2) g^{rho sigma} (d_mu g_{nu sigma} + d_nu g_{mu sigma} - d_sigma g_{mu nu})
  62
  63    We represent these as a function of three indices.