Existence of the Levi-Civita connection for a nondegenerate metric

The Koszul expression of a smooth symmetric nondegenerate metric is tensorial in its first and third arguments. Raising its third index produces a covariant derivative, without any positivity assumption. The resulting leviCivitaConnection is metric compatible and torsion free. Its positive-definite specialization agrees with Mathlib's connection on differentiable vector fields.

The value on a vector field not differentiable at the evaluation point is chosen to be zero; connection laws and uniqueness only concern differentiable fields.

References

• B. O'Neill, Semi-Riemannian Geometry with Applications to Relativity, Ch. 3, Thm. 11.
• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Thm. 5.10.
• TauCeti.Geometry.Manifold.VectorBundle.CovariantDerivative.LeviCivita.Basic: the shared bilinear Koszul tensoriality and Leibniz identities used in the construction.
• Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.LeviCivita: the construction using TensorialAt.mkHom₂, adapted here by replacing the Riesz isomorphism with the nondegenerate metric's sharp isomorphism.

noncomputable def TauCeti.Manifold.ContMDiffNondegenerateMetric.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] (g : ContMDiffNondegenerateMetric) [FiniteDimensional ℝ E] : CovariantDerivative I E fun (x : M) => TangentSpace I x

The Levi-Civita connection of a smooth symmetric nondegenerate metric. It is chosen to vanish on vector fields that are not differentiable at the evaluation point.

@[simp]

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.leviCivitaConnection_eq_zero_of_not_mdifferentiableAt {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 : (x : M) → TangentSpace I x} {x : M} [FiniteDimensional ℝ E] (hY : ¬(MDiffAt fun (x : M) => ⟨x, Y x⟩) x) : ↑g.leviCivitaConnection Y x = 0

The Levi-Civita connection vanishes on a vector field not differentiable at the point.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.two_apply_leviCivitaConnection_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) {X Y Z : (x : M) → TangentSpace I x} {x : M} [FiniteDimensional ℝ E] (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) ((↑g.leviCivitaConnection Y x) (X x))) (Z x) = g.koszul X Y Z x

The connection constructed from a nondegenerate metric satisfies the Koszul formula.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.isLeviCivitaConnection_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] (g : ContMDiffNondegenerateMetric) [FiniteDimensional ℝ E] : g.IsLeviCivitaConnection g.leviCivitaConnection

The connection constructed from the Koszul formula is metric compatible and torsion free.

theorem TauCeti.Manifold.ContMDiffNondegenerateMetric.leviCivitaConnection_apply_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) {Y : (x : M) → TangentSpace I x} {x : M} [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) (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) (v : TangentSpace I x) : (↑g.leviCivitaConnection Y x) v = (↑(CovariantDerivative.leviCivitaConnection I M) Y x) v

For a positive metric, the nondegenerate Koszul construction agrees with Mathlib's Riemannian Levi-Civita connection on differentiable vector fields.