The Levi-Civita connection on a Riemannian manifold

This file defines the Levi-Civita connection on a (finite-dimensional) Riemannian manifold (M, g). A connection ∇ on the tangent bundle of a Riemannian manifold (M, g) is called a Levi-Civita connection if it is both compatible with the metric g and torsion-free. Any two such connections are equal (on differentiable vector fields), which is why one speaks of the Levi-Civita connection on TM. We prove this uniqueness, construct a Levi-Civita connection and prove that is defines a compatible torsion-free connection.

Future PRs will prove smoothness: if M is C^{n+2} and g is C^{n+1}, the Levi-Civita connection is a C^n connection.

Main definitions and results

• CovariantDerivative.IsLeviCivitaConnection: a covariant derivative ∇ on (M, g) is a Levi-Civita connection if and only if it is both torsion-free and compatible with g

• CovariantDerivative.IsLeviCivitaConnection.apply_eq: the Koszul formula, expressing the term ⟨∇ X Y, Z⟩ for all differentiable vector fields X, Y and Z, without reference to ∇.

• CovariantDerivative.IsLeviCivitaConnection.uniqueness: a Levi-Civita connection on (M, g) is uniquely determined on differentiable vector fields

• CovariantDerivative.leviCivitaConnection: a choice of Levi-Civita connection on the tangent bundle TM of a Riemannian manifold (M, g): this is unique up to the value on non-differentiable vector fields. If you know the Levi-Civita connection already, you can use IsLeviCivitaConnection instead.

• CovariantDerivative.isLeviCivitaConnection_leviCivitaConnection: leviCivitaConnection is a Levi-Civita connection (i.e., compatible and torsion-free)

Implementation notes

• The starting observation to the construction of the Levi-Civita is the Koszul formula, expressing a term ⟪∇ X Y, Z⟫ (for differentiable vector fields X, Y and Z) without reference to the Levi-Civita connection. Our construction recovers ∇ X Y from expressions ⟪∇ X Y, Z⟫ by duality. We use a tensoriality argument and the musical isomorphism: the metric g induces a map from (2,0)-tensors (i.e., a map T_pM × T_pM → ℝ at each point) to (1,1)-tensors (i.e., a map T_pM → (T_pM)* at each point); we apply this to the (2,0)-tensor (X, Z) ↦ ⟪∇ X Y, Z⟫, to obtain a (1,1)-tensor denoted ∇ Y. This avoids the use of local frames and trivializations (which require auxiliary choices and/or gluing on local constructions).

Tags

Levi-Civita connection, metric, torsion-free, Koszul formula, musical isomorphism

theorem injective_inner_mdifferentiableAt_section {EB : Type u_1} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB] (IB : ModelWithCorners ℝ EB HB) {B : Type u_3} [TopologicalSpace B] [ChartedSpace HB B] (F : Type u_4) [NormedAddCommGroup F] [NormedSpace ℝ F] (E : B → Type u_5) [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] (x : B) : Function.Injective fun (X₀ : E x) (Z : (x : B) → E x) (x_1 : (MDiffAt fun (x : B) => ⟨x, Z x⟩) x) => inner ℝ X₀ (Z x)

A vector in E x is uniquely determined by its scalar product with sections that are differentiable at x

theorem injective_inner_contMDiffAt_section {EB : Type u_1} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB] (IB : ModelWithCorners ℝ EB HB) {B : Type u_3} [TopologicalSpace B] [ChartedSpace HB B] (F : Type u_4) [NormedAddCommGroup F] [NormedSpace ℝ F] (E : B → Type u_5) [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] (n : WithTop ℕ∞) (x : B) : Function.Injective fun (X₀ : E x) (Z : (x : B) → E x) (x_1 : ContMDiffAt IB (IB.prod (modelWithCornersSelf ℝ F)) n (fun (x : B) => ⟨x, Z x⟩) x) => inner ℝ X₀ (Z x)

A vector in E x is uniquely determined by its scalar product with sections that are C^n at x

structure CovariantDerivative.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 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (cov : CovariantDerivative I E (TangentSpace I)) [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] : Prop

A covariant derivative on the tangent bundle TM to a Riemannian manifold is called a Levi-Civita connection if it is torsion-free and compatible with g. Note that the bundle metric on TM is implicitly hidden in this definition.

• isMetricCompatible : cov.IsMetricCompatible
• torsion : cov.torsion = 0

theorem CovariantDerivative.IsLeviCivitaConnection.apply_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 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {X Y Z : (x : M) → TangentSpace I x} {cov : CovariantDerivative I E (TangentSpace I)} [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {x : M} [FiniteDimensional ℝ E] (h : IsLeviCivitaConnection I 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) : (fun (x : M) => inner ℝ ((fun (x : M) => (↑cov Y x) (X x)) x) (Z x)) x = (((d% fun (x : M) => inner ℝ (Y x) (Z x)) x) (X x) + ((d% fun (x : M) => inner ℝ (Z x) (X x)) x) (Y x) - ((d% fun (x : M) => inner ℝ (X x) (Y x)) x) (Z x) - (fun (x : M) => inner ℝ (Y x) (VectorField.mlieBracket I X Z x)) x - (fun (x : M) => inner ℝ (Z x) (VectorField.mlieBracket I Y X x)) x + (fun (x : M) => inner ℝ (X x) (VectorField.mlieBracket I Z Y x)) x) / 2

The Koszul formula, expressing the term ⟨∇ X Y, Z⟩ for all differentiable vector fields X, Y and Z, without reference to ∇. This is the key insight to prove uniqueness of the Levi-Civita connection.

theorem CovariantDerivative.IsLeviCivitaConnection.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] [IsManifold I 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {Y Z : (x : M) → TangentSpace I x} {cov : CovariantDerivative I E (TangentSpace I)} [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] (h : IsLeviCivitaConnection I cov) {x : M} (X₀ : TangentSpace I x) (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) (hZ : (MDiffAt fun (x : M) => ⟨x, Z x⟩) x) : inner ℝ ((↑cov Y x) X₀) (Z x) = (((d% fun (x : M) => inner ℝ (Y x) (Z x)) x) X₀ + ((d% fun (x_1 : M) => inner ℝ (Z x_1) (FiberBundle.extend E X₀ x_1)) x) (Y x) - ((d% fun (x_1 : M) => inner ℝ (FiberBundle.extend E X₀ x_1) (Y x_1)) x) (Z x) - (fun (x_1 : M) => inner ℝ (Y x_1) (VectorField.mlieBracket I (FiberBundle.extend E X₀) Z x_1)) x - (fun (x_1 : M) => inner ℝ (Z x_1) (VectorField.mlieBracket I Y (FiberBundle.extend E X₀) x_1)) x + inner ℝ X₀ (VectorField.mlieBracket I Z Y x)) / 2

The Koszul formula, expressing the term ⟨∇ X Y, Z⟩ for all differentiable vector fields X, Y and Z, without reference to ∇. This is the key insight to prove uniqueness of the Levi-Civita connection. This version of IsLeviCivitaConnection.apply_eq does not require the direction in which we are differentiating to be coming from a differentiable vector field.

theorem CovariantDerivative.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 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {Y : (x : M) → TangentSpace I x} {cov cov' : CovariantDerivative I E (TangentSpace I)} [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {x : M} [FiniteDimensional ℝ E] (hcov : IsLeviCivitaConnection I cov) (hcov' : IsLeviCivitaConnection I cov') (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) (X₀ : TangentSpace I x) : (↑cov Y x) X₀ = (↑cov' Y x) X₀

The Levi-Civita connection on (M, g) is uniquely determined on differentiable vector fields.

Note that the differentiability hypothesis on Y is required, since CovariantDerivative objects are unconstrained in their behaviour on non-differentiable vector fields.

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

A choice of Levi-Civita connection on the tangent bundle TM of a Riemannian manifold (M, g): this is unique up to the value on non-differentiable vector fields. If you know the Levi-Civita connection already, you can use IsLeviCivitaConnection instead.

Equations

• CovariantDerivative.leviCivitaConnection I M = { toFun := CovariantDerivative.leviCivitaAux✝ I, isCovariantDerivativeOnUniv := ⋯ }

theorem CovariantDerivative.leviCivitaConnection_apply_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 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {X Y Z : (x : M) → TangentSpace I x} [IsContMDiffRiemannianBundle I 1 E fun (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) : inner ℝ ((↑(leviCivitaConnection I M) Y x) (X x)) (Z x) = (((d% fun (x : M) => inner ℝ (Y x) (Z x)) x) (X x) + ((d% fun (x : M) => inner ℝ (Z x) (X x)) x) (Y x) - ((d% fun (x : M) => inner ℝ (X x) (Y x)) x) (Z x) - (fun (x : M) => inner ℝ (Y x) (VectorField.mlieBracket I X Z x)) x - (fun (x : M) => inner ℝ (Z x) (VectorField.mlieBracket I Y X x)) x + (fun (x : M) => inner ℝ (X x) (VectorField.mlieBracket I Z Y x)) x) / 2

theorem CovariantDerivative.leviCivitaConnection_apply_inner_right {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 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {X Y Z : (x : M) → TangentSpace I x} [IsContMDiffRiemannianBundle I 1 E fun (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) : inner ℝ (X x) ((↑(leviCivitaConnection I M) Y x) (Z x)) = (((d% fun (x : M) => inner ℝ (Y x) (X x)) x) (Z x) + ((d% fun (x : M) => inner ℝ (X x) (Z x)) x) (Y x) - ((d% fun (x : M) => inner ℝ (Z x) (Y x)) x) (X x) - (fun (x : M) => inner ℝ (Y x) (VectorField.mlieBracket I Z X x)) x - (fun (x : M) => inner ℝ (X x) (VectorField.mlieBracket I Y Z x)) x + (fun (x : M) => inner ℝ (Z x) (VectorField.mlieBracket I X Y x)) x) / 2

theorem CovariantDerivative.isMetricCompatible_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 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] : (leviCivitaConnection I M).IsMetricCompatible

theorem CovariantDerivative.torsion_leviCivitaConnection_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 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] : (leviCivitaConnection I M).torsion = 0

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

leviCivitaConnection is a Levi-Civita connection (i.e., compatible and torsion-free)