Levi-Civita connections of nondegenerate metrics

Let g be a smooth field of symmetric nondegenerate bilinear forms on the tangent bundle of M, as bundled by TauCeti.Manifold.ContMDiffNondegenerateMetric; no positivity is assumed, so this covers pseudo-Riemannian metrics of every signature. This file states what it means for a covariant derivative ∇ on TM to be compatible with g,

X (g (Y, Z)) = g (∇_X Y, Z) + g (Y, ∇_X Z),

and to be a Levi-Civita connection of g, that is, torsion free and compatible with g.

The Koszul formula

2 g (∇_X Y, Z) = X g(Y, Z) + Y g(Z, X) - Z g(X, Y) + g([X, Y], Z) - g([X, Z], Y) - g([Y, Z], X)

holds for every Levi-Civita connection of g, and conversely characterizes them. Since g is nondegenerate, a tangent vector is determined by its pairings with differentiable vector fields, so the Koszul formula determines ∇_X Y for every Y differentiable at the base point: a Levi-Civita connection of a nondegenerate metric is unique on differentiable vector fields. This is the uniqueness half of the fundamental theorem of pseudo-Riemannian geometry.

For the metric of a Riemannian bundle instance, these notions agree with Mathlib's CovariantDerivative.IsMetricCompatible and CovariantDerivative.IsLeviCivitaConnection, and Mathlib's CovariantDerivative.leviCivitaConnection is a Levi-Civita connection of the nondegenerate metric obtained from the bundled Riemannian metric.

Main definitions and results

• TauCeti.Manifold.ContMDiffNondegenerateMetric.koszul: the Koszul expression of g.
• TauCeti.Manifold.ContMDiffNondegenerateMetric.IsMetricCompatible: compatibility of a covariant derivative on TM with g.
• TauCeti.Manifold.ContMDiffNondegenerateMetric.isMetricCompatible_iff_derivBilinearTensor_eq_zero characterizes compatibility with g as the vanishing of the covariant derivative ∇g of g.
• TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection: a torsion-free covariant derivative compatible with g.
• TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.two_apply_eq_koszul and TauCeti.Manifold.ContMDiffNondegenerateMetric.isLeviCivitaConnection_iff: the Koszul formula, and its characterization of the Levi-Civita connections of g.
• TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.uniqueness and TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.difference_eq_zero: uniqueness of the Levi-Civita connection of g on differentiable vector fields.
• TauCeti.Manifold.ContMDiffNondegenerateMetric.isLeviCivitaConnection_iff_of_apply_eq_inner: for a metric given by a Riemannian bundle instance, the comparison with CovariantDerivative.IsLeviCivitaConnection.

References

• B. O'Neill, Semi-Riemannian Geometry with Applications to Relativity, Academic Press, 1983, Ch. 3, Thm. 11.
• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Thm. 5.10.
• Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.LeviCivita: the injective_inner_mdifferentiableAt_vectorField, IsLeviCivitaConnection.apply_eq_extend, and IsLeviCivitaConnection.uniqueness arguments adapted here, with the inner product replaced by g and positivity by nondegeneracy.
• TauCeti.Geometry.Manifold.VectorBundle.CovariantDerivative.LeviCivita.Basic: the positive-definite Koszul development generalized here to g.

Nondegeneracy along differentiable vector fields

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.injective_apply_mdifferentiableAt_vectorField {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffNondegenerateMetric) (x : M) : Function.Injective fun (u : TangentSpace I x) (Z : (x : M) → TangentSpace I x) (x_1 : (MDiffAt fun (x : M) => ⟨x, Z x⟩) x) => ((g.toContMDiffSection x) u) (Z x)

A tangent vector is determined by its pairings under a nondegenerate metric with the values of vector fields that are differentiable at its base point.

The Koszul expression

noncomputable def TauCeti.Manifold.ContMDiffNondegenerateMetric.koszul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffNondegenerateMetric) (X Y Z : (x : M) → TangentSpace I x) (x : M) : ℝ

The right-hand side of the Koszul formula for the metric g,

X g(Y, Z) + Y g(Z, X) - Z g(X, Y) + g([X, Y], Z) - g([X, Z], Y) - g([Y, Z], X),

evaluated at x. For a Levi-Civita connection ∇ of g it computes 2 g(∇_X Y, Z), by TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.two_apply_eq_koszul.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.koszul_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffNondegenerateMetric) (X Y Z : (x : M) → TangentSpace I x) (x : M) : g.koszul X Y Z x = ((d% fun (y : M) => ((g.toContMDiffSection y) (Y y)) (Z y)) x) (X x) + ((d% fun (y : M) => ((g.toContMDiffSection y) (Z y)) (X y)) x) (Y x) - ((d% fun (y : M) => ((g.toContMDiffSection y) (X y)) (Y y)) x) (Z x) + ((g.toContMDiffSection x) (VectorField.mlieBracket I X Y x)) (Z x) - ((g.toContMDiffSection x) (VectorField.mlieBracket I X Z x)) (Y x) - ((g.toContMDiffSection x) (VectorField.mlieBracket I Y Z x)) (X x)

The defining formula for the Koszul expression of a nondegenerate metric.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.koszul_sub_koszul_swap_first_two {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffNondegenerateMetric) {X Y Z : (x : M) → TangentSpace I x} {x : M} : g.koszul X Y Z x - g.koszul Y X Z x = 2 * ((g.toContMDiffSection x) (VectorField.mlieBracket I X Y x)) (Z x)

Antisymmetrizing the Koszul expression in its first two arguments returns twice the pairing of the Lie bracket with the third argument.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.koszul_add_koszul_swap_last_two {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffNondegenerateMetric) {X Y Z : (x : M) → TangentSpace I x} {x : M} : g.koszul Z X Y x + g.koszul Z Y X x = 2 * ((d% fun (y : M) => ((g.toContMDiffSection y) (X y)) (Y y)) x) (Z x)

Symmetrizing the Koszul expression in its last two arguments returns twice the derivative of their pairing along the first argument.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.koszul_add_second {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffNondegenerateMetric) {X Y Z : (x : M) → TangentSpace I x} {x : M} [CompleteSpace E] {Y' : (x : M) → TangentSpace I x} (hX : (MDiffAt fun (x : M) => ⟨x, X x⟩) x) (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) (hY' : (MDiffAt fun (x : M) => ⟨x, Y' x⟩) x) (hZ : (MDiffAt fun (x : M) => ⟨x, Z x⟩) x) : g.koszul X (Y + Y') Z x = g.koszul X Y Z x + g.koszul X Y' Z x

The Koszul expression is additive in the differentiated vector field.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.koszul_smul_second {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffNondegenerateMetric) {X Y Z : (x : M) → TangentSpace I x} {x : M} [CompleteSpace E] {f : M → ℝ} (hf : MDiffAt f x) (hX : (MDiffAt fun (x : M) => ⟨x, X x⟩) x) (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) (hZ : (MDiffAt fun (x : M) => ⟨x, Z x⟩) x) : g.koszul X (f • Y) Z x = f x * g.koszul X Y Z x + 2 * (d% f x) (X x) * ((g.toContMDiffSection x) (Y x)) (Z x)

The Koszul expression obeys the connection Leibniz rule in its second argument.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.tensorialAt_koszul_first {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffNondegenerateMetric) {Y Z : (x : M) → TangentSpace I x} {x : M} [CompleteSpace E] (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) (hZ : (MDiffAt fun (x : M) => ⟨x, Z x⟩) x) : TensorialAt I E (fun (X : (y : M) → TangentSpace I y) => g.koszul X Y Z x) x

The Koszul expression is tensorial in its first argument.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.tensorialAt_koszul_third {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffNondegenerateMetric) {X Y : (x : M) → TangentSpace I x} {x : M} [CompleteSpace E] (hX : (MDiffAt fun (x : M) => ⟨x, X x⟩) x) (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) : TensorialAt I E (fun (Z : (y : M) → TangentSpace I y) => g.koszul X Y Z x) x

The Koszul expression is tensorial in its third argument.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.koszul_eq_of_apply_eq_inner {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffNondegenerateMetric) {X Y Z : (x : M) → TangentSpace I x} {x : M} [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (hg : ∀ (x : M) (v w : TangentSpace I x), ((g.toContMDiffSection x) v) w = inner ℝ v w) : g.koszul X Y Z x = Manifold.koszul I X Y Z x

For a metric whose pairing is the inner product of a Riemannian bundle instance, the Koszul expression is TauCeti.Manifold.koszul.

Compatibility with the metric

def TauCeti.Manifold.ContMDiffNondegenerateMetric.IsMetricCompatible {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffNondegenerateMetric) (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) : Prop

A covariant derivative ∇ on the tangent bundle is compatible with the nondegenerate metric g when v (g(Y, Z)) = g(∇_v Y, Z) + g(Y, ∇_v Z) for every tangent vector v at x and all vector fields Y, Z differentiable at x.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.isMetricCompatible_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffNondegenerateMetric) {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} : g.IsMetricCompatible cov ↔ ∀ ⦃x : M⦄ ⦃Y Z : (x : M) → TangentSpace I x⦄, (MDiffAt fun (x : M) => ⟨x, Y x⟩) x → (MDiffAt fun (x : M) => ⟨x, Z x⟩) x → ∀ (v : TangentSpace I x), ((d% fun (y : M) => ((g.toContMDiffSection y) (Y y)) (Z y)) x) v = ((g.toContMDiffSection x) ((↑cov Y x) v)) (Z x) + ((g.toContMDiffSection x) (Y x)) ((↑cov Z x) v)

Compatibility with a nondegenerate metric, in its defining arbitrary-tangent-vector form.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.IsMetricCompatible.mvfderiv_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {g : ContMDiffNondegenerateMetric} {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} {Y Z : (x : M) → TangentSpace I x} {x : M} (h : g.IsMetricCompatible cov) (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) (hZ : (MDiffAt fun (x : M) => ⟨x, Z x⟩) x) (v : TangentSpace I x) : ((d% fun (y : M) => ((g.toContMDiffSection y) (Y y)) (Z y)) x) v = ((g.toContMDiffSection x) ((↑cov Y x) v)) (Z x) + ((g.toContMDiffSection x) (Y x)) ((↑cov Z x) v)

The product rule satisfied by a covariant derivative compatible with a nondegenerate metric.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.isMetricCompatible_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {g : ContMDiffNondegenerateMetric} {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} : g.IsMetricCompatible cov ↔ ∀ ⦃x : M⦄ ⦃X Y Z : (x : M) → TangentSpace I x⦄, (MDiffAt fun (x : M) => ⟨x, X x⟩) x → (MDiffAt fun (x : M) => ⟨x, Y x⟩) x → (MDiffAt fun (x : M) => ⟨x, Z x⟩) x → ((d% fun (y : M) => ((g.toContMDiffSection y) (Y y)) (Z y)) x) (X x) = ((g.toContMDiffSection x) ((↑cov Y x) (X x))) (Z x) + ((g.toContMDiffSection x) (Y x)) ((↑cov Z x) (X x))

Compatibility with a nondegenerate metric may be tested along differentiable vector fields X rather than along arbitrary tangent vectors.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.isMetricCompatible_iff_of_apply_eq_inner {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {g : ContMDiffNondegenerateMetric} {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} [FiniteDimensional ℝ E] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (hg : ∀ (x : M) (v w : TangentSpace I x), ((g.toContMDiffSection x) v) w = inner ℝ v w) : g.IsMetricCompatible cov ↔ cov.IsMetricCompatible

For a metric whose pairing is the inner product of a Riemannian bundle instance, compatibility with the metric is Mathlib's CovariantDerivative.IsMetricCompatible.

Levi-Civita connections

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.isMetricCompatible_iff_derivBilinearTensor_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {g : ContMDiffNondegenerateMetric} {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} [FiniteDimensional ℝ E] : g.IsMetricCompatible cov ↔ ∀ (x : M), cov.derivBilinearTensor (⇑g.toContMDiffSection) x = 0

A covariant derivative on the tangent bundle is compatible with a nondegenerate metric g exactly when the covariant derivative ∇g of g, as a field of bilinear forms, vanishes.

structure TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffNondegenerateMetric) [FiniteDimensional ℝ E] (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) : Prop

A covariant derivative on the tangent bundle is a Levi-Civita connection of the nondegenerate metric g when it is torsion free and compatible with g.

• isMetricCompatible : g.IsMetricCompatible cov

  A Levi-Civita connection is compatible with the metric.

• torsion : cov.torsion = 0

  A Levi-Civita connection is torsion free.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.derivBilinearTensor_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {g : ContMDiffNondegenerateMetric} {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} [FiniteDimensional ℝ E] (h : g.IsLeviCivitaConnection cov) (x : M) : cov.derivBilinearTensor (⇑g.toContMDiffSection) x = 0

The covariant derivative of a nondegenerate metric along one of its Levi-Civita connections vanishes.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.two_apply_eq_koszul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {g : ContMDiffNondegenerateMetric} {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} {X Y Z : (x : M) → TangentSpace I x} {x : M} [FiniteDimensional ℝ E] (h : g.IsLeviCivitaConnection cov) (hX : (MDiffAt fun (x : M) => ⟨x, X x⟩) x) (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) (hZ : (MDiffAt fun (x : M) => ⟨x, Z x⟩) x) : 2 * ((g.toContMDiffSection x) ((↑cov Y x) (X x))) (Z x) = g.koszul X Y Z x

The Koszul formula: for a Levi-Civita connection ∇ of a nondegenerate metric g, 2 g(∇_X Y, Z) is the Koszul expression of g.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.isLeviCivitaConnection_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {g : ContMDiffNondegenerateMetric} {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} [FiniteDimensional ℝ E] : g.IsLeviCivitaConnection cov ↔ ∀ ⦃x : M⦄ ⦃X Y Z : (x : M) → TangentSpace I x⦄, (MDiffAt fun (x : M) => ⟨x, X x⟩) x → (MDiffAt fun (x : M) => ⟨x, Y x⟩) x → (MDiffAt fun (x : M) => ⟨x, Z x⟩) x → 2 * ((g.toContMDiffSection x) ((↑cov Y x) (X x))) (Z x) = g.koszul X Y Z x

A covariant derivative on the tangent bundle is a Levi-Civita connection of a nondegenerate metric exactly when it satisfies the Koszul formula.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.uniqueness {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {g : ContMDiffNondegenerateMetric} {cov cov' : CovariantDerivative I E fun (x : M) => TangentSpace I x} {Y : (x : M) → TangentSpace I x} {x : M} [FiniteDimensional ℝ E] (h : g.IsLeviCivitaConnection cov) (h' : g.IsLeviCivitaConnection cov') (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) (v : TangentSpace I x) : (↑cov Y x) v = (↑cov' Y x) v

Uniqueness of the Levi-Civita connection of a nondegenerate metric: two Levi-Civita connections of g agree on every vector field differentiable at the base point.

The differentiability hypothesis on Y is needed, since a CovariantDerivative is unconstrained on vector fields that are not differentiable.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.IsLeviCivitaConnection.difference_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {g : ContMDiffNondegenerateMetric} {cov cov' : CovariantDerivative I E fun (x : M) => TangentSpace I x} [FiniteDimensional ℝ E] (h : g.IsLeviCivitaConnection cov) (h' : g.IsLeviCivitaConnection cov') : cov.difference cov' = 0

Uniqueness of the Levi-Civita connection of a nondegenerate metric, as the vanishing of the endomorphism-valued one-form CovariantDerivative.difference of two of them.

The positive-definite specialization

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.isLeviCivitaConnection_iff_of_apply_eq_inner {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {g : ContMDiffNondegenerateMetric} {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} [FiniteDimensional ℝ E] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (hg : ∀ (x : M) (v w : TangentSpace I x), ((g.toContMDiffSection x) v) w = inner ℝ v w) : g.IsLeviCivitaConnection cov ↔ CovariantDerivative.IsLeviCivitaConnection I cov

For a metric whose pairing is the inner product of a Riemannian bundle instance, its Levi-Civita connections are those of Mathlib's CovariantDerivative.IsLeviCivitaConnection.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.isLeviCivitaConnection_ofRiemannianBundle_leviCivitaConnection {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] : (ofRiemannianBundle I M).IsLeviCivitaConnection (CovariantDerivative.leviCivitaConnection I M)

Mathlib's Levi-Civita connection of a smooth Riemannian manifold is a Levi-Civita connection of its metric, viewed as a nondegenerate metric.