LoweredConnectionIdentity

formal source

 125    Γ_{ρμν} + Γ_{νρμ} = ∂_μ g_{ρν}
 126
 127    This is equation (3.1.18) in Wald. -/
 128def LoweredConnectionIdentity (Γ : ConnectionCoeffs) (g : MetricTensor)
 129    (x : Fin 4 → ℝ) : Prop :=
 130  ∀ ρ μ ν,
 131    lowered_connection Γ g x ρ μ ν + lowered_connection Γ g x ν ρ μ =
 132    partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then ρ else ν)) μ x
 133
 134/-- Uniqueness: any torsion-free, metric-compatible connection has lowered coefficients
 135    uniquely determined by the metric. The Koszul formula gives:
 136
 137    Γ_{ρμν} = (1/2)(∂_μ g_{ρν} + ∂_ν g_{ρμ} - ∂_ρ g_{μν})
 138
 139    which, after raising the index with g^{ρσ}, yields `Curvature.christoffel`. -/
 140theorem connection_uniqueness_lowered
 141    (Γ : ConnectionCoeffs) (g : MetricTensor) (x : Fin 4 → ℝ)
 142    (h_tf : IsTorsionFree Γ)
 143    (h_id : LoweredConnectionIdentity Γ g x) :
 144    ∀ ρ μ ν,
 145      lowered_connection Γ g x ρ μ ν =
 146      (1/2 : ℝ) * (
 147        partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then ρ else ν)) μ x +
 148        partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then ρ else μ)) ν x -
 149        partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then μ else ν)) ρ x
 150      ) := by
 151  intro ρ μ ν
 152  -- Three permutations of Γ_{abc} + Γ_{cab} = ∂_b g_{ac}:
 153  have hA := h_id ρ μ ν
 154  have hB := h_id ρ ν μ
 155  have hC := h_id ν ρ μ
 156  -- Torsion-free: Γ_{abc} = Γ_{acb}
 157  have h_sym : ∀ a b c, lowered_connection Γ g x a b c = lowered_connection Γ g x a c b := by
 158    intro a b c