ConnectionCoeffs

formal source

  37/-! ## §1 Connection as a Function Type -/
  38
  39/-- A connection Γ on 4D spacetime: Γ^ρ_μν at each point x. -/
  40abbrev ConnectionCoeffs := (Fin 4 → ℝ) → Fin 4 → Fin 4 → Fin 4 → ℝ
  41
  42/-- A connection is torsion-free iff Γ^ρ_μν = Γ^ρ_νμ. -/
  43def IsTorsionFree (Γ : ConnectionCoeffs) : Prop :=
  44  ∀ x ρ μ ν, Γ x ρ μ ν = Γ x ρ ν μ
  45
  46/-- The covariant derivative of the metric with respect to a connection:
  47    ∇_ρ g_{μν} = ∂_ρ g_{μν} - Γ^σ_ρμ g_{σν} - Γ^σ_ρν g_{μσ}. -/
  48def cov_deriv_metric (Γ : ConnectionCoeffs) (g : MetricTensor)
  49    (x : Fin 4 → ℝ) (ρ μ ν : Fin 4) : ℝ :=
  50  let g_comp := fun y a b => g.g y (fun _ => 0) (fun i => if i.val = 0 then a else b)
  51  partialDeriv_v2 (fun y => g_comp y μ ν) ρ x -
  52  Finset.univ.sum (fun σ => Γ x σ ρ μ * g_comp x σ ν) -
  53  Finset.univ.sum (fun σ => Γ x σ ρ ν * g_comp x μ σ)
  54
  55/-- A connection is metric-compatible iff ∇_ρ g_{μν} = 0 for all ρ, μ, ν. -/
  56def IsMetricCompatible (Γ : ConnectionCoeffs) (g : MetricTensor) : Prop :=
  57  ∀ x ρ μ ν, cov_deriv_metric Γ g x ρ μ ν = 0
  58
  59/-! ## §2 Christoffel Symbols Are Torsion-Free -/
  60
  61/-- `Curvature.christoffel` is torsion-free.
  62    This is already proved as `christoffel_symmetric`. -/
  63theorem levi_civita_torsion_free (g : MetricTensor) :
  64    IsTorsionFree (christoffel g) :=
  65  fun x ρ μ ν => christoffel_symmetric g x ρ μ ν
  66
  67/-! ## §3 Metric Compatibility of the Christoffel Connection
  68
  69The metric compatibility ∇_ρ g_{μν} = 0 for the Levi-Civita connection
  70follows from the algebraic structure of the Christoffel symbols.