Fundamental theorem of Riemannian geometry (Levi-Civita)

levi_civita_exists_unique

Submitter: Kim Morrison.

Notes: §38 of Knill's 'Some Fundamental Theorems in Mathematics'. On a C^∞ finite-dimensional Riemannian manifold, there exists a unique smooth torsion-free metric-compatible covariant derivative on TM (the Levi-Civita connection); uniqueness is stated on the smooth-section subspace via `SameOnSmooth` since mathlib's `CovariantDerivative` is bundled over all sections. Mathlib has the covariant-derivative / Riemannian-bundle / Lie-bracket machinery but no metric-compatibility predicate and no Levi-Civita existence/uniqueness.

Source: T. Levi-Civita, Nozione di parallelismo in una varietà qualunque, Rend. Circ. Mat. Palermo 42 (1917). Listed as §38 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: Existence + uniqueness via the Koszul formula. Solve 2·g(∇_X Y, Z) = X·g(Y,Z) + Y·g(X,Z) − Z·g(X,Y) − g(X,[Y,Z]) − g(Y,[X,Z]) + g(Z,[X,Y]) for the unknown ∇_X Y: the right-hand side is C^∞(M)-linear in Z and a derivation in Y, so by non-degeneracy of g it determines ∇_X Y as a smooth section. Direct verification that this `cov` is torsion-free and metric-compatible. For uniqueness: any other torsion-free metric-compatible smooth connection ∇' must satisfy the same Koszul identity, hence agrees with ∇ on smooth Y at every smooth X-direction.

theorem declaration uses `sorry`levi_civita_exists_unique {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
      [FiniteDimensional ℝ E] [CompleteSpace E]
    {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
    {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
      [IsManifold I ∞ M]
    [RiemannianBundle (fun (x : M) ↦ TangentSpace I x)]
    [IsContMDiffRiemannianBundle I ∞ E (fun (x : M) ↦ TangentSpace I x)] :
    ∃ cov : CovariantDerivative I E (TangentSpace I (M := M)),
      (ContMDiffCovariantDerivative cov ∞ ∧
        cov.torsion = 0 ∧ LeanEval.Geometry.LeviCivita.IsMetricCompatible cov) ∧
      ∀ cov' : CovariantDerivative I E (TangentSpace I (M := M)),
        (ContMDiffCovariantDerivative cov' ∞ ∧
          cov'.torsion = 0 ∧ LeanEval.Geometry.LeviCivita.IsMetricCompatible cov') →
        LeanEval.Geometry.LeviCivita.SameOnSmooth cov cov' := byE:Type u_1inst✝⁹:NormedAddCommGroup Einst✝⁸:NormedSpace ℝ Einst✝⁷:FiniteDimensional ℝ Einst✝⁶:CompleteSpace EH:Type u_2inst✝⁵:TopologicalSpace HI:ModelWithCorners ℝ E HM:Type u_3inst✝⁴:TopologicalSpace Minst✝³:ChartedSpace H Minst✝²:IsManifold I ∞ Minst✝¹:RiemannianBundle fun x => TangentSpace I xinst✝:IsContMDiffRiemannianBundle I ∞ E fun x => TangentSpace I x⊢ ∃ cov,
  (cov.ContMDiffCovariantDerivative ∞ ∧ cov.torsion = 0 ∧ IsMetricCompatible cov) ∧
    ∀ (cov' : CovariantDerivative I E (TangentSpace I)),
      cov'.ContMDiffCovariantDerivative ∞ ∧ cov'.torsion = 0 ∧ IsMetricCompatible cov' → SameOnSmooth cov cov'
  sorryAll goals completed! 🐙

Solved by

Not yet solved.