Levi-Civita connection

TheoremThe Levi-Civita connection of a vector space is the Fréchet derivative#✓fully proved

Let \(F\) be a finite-dimensional real inner product space with its standard Riemannian metric, let \(V\) be a vector field on \(F\) and \(x \in F\), and suppose \(V\) is differentiable at \(x\) as a section of the tangent bundle. Then for every tangent vector \(v \in T_xF\), the covariant derivative \(\nabla_v V\) of \(V\) at \(x\) for the Levi-Civita connection \(\nabla\) equals \(DV(x)(v)\), the Fréchet derivative of \(V\) at \(x\) applied to \(v\).

theorem CovariantDerivative.leviCivitaConnection_vectorSpace_apply
    {V : Π y : F, TangentSpace 𝓘(ℝ, F) y} {x : F} (hV : MDiffAt (T% V) x)
    (v : TangentSpace 𝓘(ℝ, F) x) :
    leviCivitaConnection 𝓘(ℝ, F) F V x v = fderiv ℝ V x v

Uses 3 · Used by 2

Proof usesThe Levi-Civita connection of Euclidean space kills constant vector fields · Extending a tangent vector of a normed space gives a constant vector field · Extensions of tangent vectors of a normed space are differentiable

Used byGeodesic velocity curves in Euclidean space · Killing fields on Euclidean space

DefinitionMetric-compatible covariant derivative#✓fully proved

Let \(M\) be a smooth manifold (possibly with corners) modelled on a finite-dimensional real normed space, with a smooth Riemannian metric \(\langle \cdot, \cdot \rangle\) on its tangent bundle. A covariant derivative \(\nabla\) on the tangent bundle is compatible with the metric if for all smooth vector fields \(Y, Z\) on \(M\), every point \(x \in M\) and every tangent vector \(v \in T_x M\),

\[ v \langle Y, Z \rangle = \langle \nabla_v Y, Z(x) \rangle + \langle Y(x), \nabla_v Z \rangle, \]

where \(v \langle Y, Z \rangle\) is the derivative at \(x\) in the direction \(v\) of the function \(y \mapsto \langle Y(y), Z(y) \rangle\).

def IsMetricCompatible
    {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))) : Prop :=
  ∀ (Y Z : Π x : M, TangentSpace I x),
    CMDiff ∞ (T% Y) → CMDiff ∞ (T% Z) →
    ∀ (x : M) (v : TangentSpace I x),
      mvfderiv I (fun y : M => inner ℝ (Y y) (Z y)) x v =
        inner ℝ (cov Y x v) (Z x) + inner ℝ (Y x) (cov Z x v)

Used by 4

Used byKoszul formula · Fundamental theorem of Riemannian geometry (Levi-Civita) · Differentiable sphere theorem · Topological sphere theorem

TheoremKoszul formula#●ready to prove

Let \(M\) be a smooth manifold, modelled with corners on a finite-dimensional real normed space, whose tangent bundle carries a smooth Riemannian metric \(\langle \cdot, \cdot \rangle\), and let \(\nabla\) be a smooth covariant derivative on the tangent bundle of \(M\) that is torsion-free and compatible with the metric. Then for all smooth vector fields \(X\), \(Y\), \(Z\) on \(M\) and every point \(x \in M\), evaluating every term at \(x\),

\[2 \langle \nabla_X Y, Z \rangle = X \langle Y, Z \rangle + Y \langle X, Z \rangle - Z \langle X, Y \rangle - \langle X, [Y, Z] \rangle - \langle Y, [X, Z] \rangle + \langle Z, [X, Y] \rangle,\]

where \(\nabla_X Y\) at \(x\) is the covariant derivative of \(Y\) in the direction \(X(x)\), \(X \langle Y, Z \rangle\) at \(x\) is the derivative of the function \(y \mapsto \langle Y(y), Z(y) \rangle\) in the direction \(X(x)\), and \([\cdot, \cdot]\) is the Lie bracket of vector fields.

MathlibExt.Geometry.KoszulFormulaWanted.Geometry.KoszulFormula.koszul_formula · 21 lines

public theorem_wanted koszul_formula
    {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 ∞]
    (_htor : cov.torsion = 0) (_hmet : IsMetricCompatible cov)
    (X Y Z : Π x : M, TangentSpace I x)
    (_hX : CMDiff ∞ (T% X)) (_hY : CMDiff ∞ (T% Y)) (_hZ : CMDiff ∞ (T% Z))
    (x : M) :
    2 * inner ℝ (cov Y x (X x)) (Z x) =
      mvfderiv I (fun y : M => inner ℝ (Y y) (Z y)) x (X x)
      + mvfderiv I (fun y : M => inner ℝ (X y) (Z y)) x (Y x)
      - mvfderiv I (fun y : M => inner ℝ (X y) (Y y)) x (Z x)
      - inner ℝ (X x) (mlieBracket I Y Z x)
      - inner ℝ (Y x) (mlieBracket I X Z x)
      + inner ℝ (Z x) (mlieBracket I X Y x)

Sources

• J.-L. Koszul (course notes, 1950s); cf. do Carmo, Riemannian Geometry. Listed as §38 additional statement in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem koszul_formula of the lean-eval benchmark.

Uses 1

Statement usesMetric-compatible covariant derivative

DefinitionAgreement of covariant derivatives on smooth vector fields#✓fully proved

Let \(M\) be a smooth manifold, possibly with boundary or corners, modelled on a finite-dimensional real normed space, whose tangent bundle carries a smooth Riemannian metric. Two covariant derivatives \(\nabla\) and \(\nabla'\) on the tangent bundle of \(M\) agree on smooth sections when \(\nabla_v Y = \nabla'_v Y\) for every smooth vector field \(Y\) on \(M\), every point \(x \in M\) and every tangent vector \(v\) at \(x\).

Covariant derivatives here act on all sections of the tangent bundle, not only smooth ones, so the uniqueness in the Levi-Civita theorem is stated as agreement on smooth vector fields.

def SameOnSmooth
    {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 cov' : CovariantDerivative I E (TangentSpace I (M := M))) : Prop :=
  ∀ (Y : Π x : M, TangentSpace I x), CMDiff ∞ (T% Y) →
    ∀ (x : M) (v : TangentSpace I x), cov Y x v = cov' Y x v

Used by 1

Used byFundamental theorem of Riemannian geometry (Levi-Civita)

TheoremFundamental theorem of Riemannian geometry (Levi-Civita)#●ready to prove

Let \(M\) be a Hausdorff smooth manifold, possibly with boundary or corners, modelled on a finite-dimensional real normed space, whose tangent bundle carries a smooth Riemannian metric. Then there is a smooth covariant derivative \(\nabla\) on the tangent bundle of \(M\) that is torsion-free and compatible with the metric, and every smooth, torsion-free, metric-compatible covariant derivative \(\nabla'\) on the tangent bundle of \(M\) agrees with \(\nabla\) on smooth vector fields: \(\nabla'_v Y = \nabla_v Y\) for every smooth vector field \(Y\) on \(M\), every point \(x \in M\) and every tangent vector \(v\) at \(x\).

MathlibExt.Geometry.LeviCivitaWanted.Geometry.LeviCivita.levi_civita_exists_unique · 15 lines

public theorem_wanted 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] [T2Space 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 ∧ IsMetricCompatible cov) ∧
      ∀ cov' : CovariantDerivative I E (TangentSpace I (M := M)),
        (ContMDiffCovariantDerivative cov' ∞ ∧
          cov'.torsion = 0 ∧ IsMetricCompatible cov') →
        SameOnSmooth cov cov'

Sources

• 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). Problem levi_civita_exists_unique of the lean-eval benchmark.

Uses 2

Statement usesAgreement of covariant derivatives on smooth vector fields · Metric-compatible covariant derivative

3 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.