Existence of the Levi-Civita connection

The Koszul formula 2 ⟪∇_X Y, Z⟫ = koszul I X Y Z characterises the Levi-Civita connection of a Riemannian metric, and its right-hand side involves the metric alone. This file turns that characterisation into a construction: on a finite-dimensional Riemannian manifold there is a torsion-free metric covariant derivative on the tangent bundle, so that together with CovariantDerivative.IsLeviCivita.difference_eq_zero the Levi-Civita connection exists and is unique.

The construction has three steps. The Koszul expression is tensorial in its first argument as well as in its third, so Mathlib's TensorialAt.mkHom₂ packages (X, Z) ↦ koszul I X Y Z x as a continuous bilinear form TauCeti.Manifold.koszulHom on the fibre T_x M. The fibrewise Fréchet–Riesz equivalence Riemannian.Tensor.rieszDual then converts the last slot of that bilinear form into a vector, giving the unbundled candidate. Finally the covariant-derivative axioms for the candidate are read off the behaviour of the Koszul expression in its second argument: TauCeti.Manifold.koszul_add_second gives additivity, and TauCeti.Manifold.koszul_smul_second — which says that replacing Y by f • Y adds 2 (df X) ⟪Y, Z⟫ — gives the Leibniz rule.

Since a covariant derivative in Mathlib is a total function on sections, constrained only at sections which are differentiable at the point under consideration, the unbundled candidate is given by the Koszul recipe when Y is differentiable at x and is the junk value 0 otherwise. Every theorem about its value accordingly carries a differentiability hypothesis, and uniqueness is the vanishing of CovariantDerivative.difference rather than equality of bundled connections.

Main definitions and results

• TauCeti.Manifold.koszulHom: the Koszul expression of a section differentiable at x, as a continuous bilinear form on T_x M.
• CovariantDerivative.leviCivita: the Levi-Civita connection of the supplied Riemannian bundle instance.
• CovariantDerivative.two_inner_leviCivita_eq_koszul: it obeys the Koszul formula.
• CovariantDerivative.isLeviCivita_leviCivita: it is torsion free and metric.
• CovariantDerivative.exists_isLeviCivita: existence of the Levi-Civita connection.

References

• Geodesics, the exponential map, and the Hopf–Rinow theorem roadmap, Layer 1, "The Levi-Civita connection".
• mathlib4#36845: this construction follows its tensoriality-and-Riesz design, adapted to the APIs in Tau Ceti's Mathlib pin.
• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 2, Thm. 3.6.
• J. M. Lee, Introduction to Riemannian Manifolds, GTM 176, 2018, Thm. 5.10.

The Koszul form of a section

noncomputable def TauCeti.Manifold.koszulHom {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (Y : (y : M) → TangentSpace I y) {x : M} (hY : (MDiffAt fun (y : M) => ⟨y, Y y⟩) x) : TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ

The Koszul expression of a section Y differentiable at x, as a continuous bilinear form on the tangent fibre at x. For sections X and Z differentiable at x, its value at (X x, Z x) is koszul I X Y Z x; see koszulHom_apply.

Equations

• TauCeti.Manifold.koszulHom Y hY = TensorialAt.mkHom₂ (fun (X Z : (x : M) → TangentSpace I x) => TauCeti.Manifold.koszul I X Y Z x) x ⋯ ⋯

@[simp]

theorem TauCeti.Manifold.koszulHom_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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {X Y Z : (x : M) → TangentSpace I x} {x : M} (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) (hX : (MDiffAt fun (x : M) => ⟨x, X x⟩) x) (hZ : (MDiffAt fun (x : M) => ⟨x, Z x⟩) x) : ((koszulHom Y hY) (X x)) (Z x) = koszul I X Y Z x

theorem TauCeti.Manifold.koszulHom_apply_eq_extend {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {x : M} (Y : (y : M) → TangentSpace I y) (hY : (MDiffAt fun (y : M) => ⟨y, Y y⟩) x) (v w : TangentSpace I x) : ((koszulHom Y hY) v) w = koszul I (FiberBundle.extend E v) Y (FiberBundle.extend E w) x

The Koszul form evaluated at arbitrary tangent vectors, expressed using their canonical local extensions.

The connection

noncomputable def CovariantDerivative.leviCivita {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] : CovariantDerivative I E fun (x : M) => TangentSpace I x

The Levi-Civita connection of the supplied Riemannian bundle instance: the torsion-free covariant derivative on the tangent bundle which is compatible with the metric.

Equations

• CovariantDerivative.leviCivita I M = { toFun := CovariantDerivative.leviCivitaFun✝, isCovariantDerivativeOnUniv := ⋯ }

theorem CovariantDerivative.two_inner_leviCivita_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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {Y : (x : M) → TangentSpace I x} {x : M} (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) (v w : TangentSpace I x) : 2 * inner ℝ ((↑(leviCivita I M) Y x) v) w = ((TauCeti.Manifold.koszulHom Y hY) v) w

The defining identity for the Levi-Civita connection at arbitrary tangent vectors.

theorem CovariantDerivative.two_inner_leviCivita_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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {X Y Z : (x : M) → TangentSpace I x} {x : M} (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 * inner ℝ ((↑(leviCivita I M) Y x) (X x)) (Z x) = TauCeti.Manifold.koszul I X Y Z x

The Koszul formula for the Levi-Civita connection.

Existence

theorem CovariantDerivative.isLeviCivita_leviCivita {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] : (leviCivita I M).IsLeviCivita

Existence of the Levi-Civita connection: the connection built from the Koszul formula is torsion free and compatible with the metric.

theorem CovariantDerivative.exists_isLeviCivita {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] : ∃ (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x), cov.IsLeviCivita

Existence of the Levi-Civita connection, in existential form.