Pointwise curvature tensors

The curvature of a smooth connection on a finite-rank real vector bundle is a trilinear map on each fibre. CovariantDerivative.curvatureTensor bundles this map, with two tangent-vector arguments and one bundle-vector argument. On the tangent bundle it is the pointwise (1,3) curvature tensor, ready for contraction or pairing with a metric.

The construction uses globally smooth extensions of fibre vectors and the pointwise independence theorem CovariantDerivative.curvatureOperator_congr. Its characteristic equation curvatureTensor_apply computes it on any smooth fields and section, so callers do not depend on the chosen extensions; curvatureTensor_apply_of_contMDiffOn does so for inputs which are only smooth near the point, such as local frames. No metric or torsion assumption is needed.

The sign convention is that of J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 7, pp. 196–198: R(X,Y)σ = ∇_X ∇_Y σ - ∇_Y ∇_X σ - ∇_[X,Y] σ.

noncomputable def CovariantDerivative.curvatureTensor {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle (↑⊤) F V I] (cov : CovariantDerivative I F V) [cov.ContMDiffCovariantDerivative ↑⊤] (x : M) : TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] V x →ₗ[ℝ] V x

The pointwise curvature tensor of a smooth connection, linear in two tangent vectors and one bundle vector. On the tangent bundle this is the (1,3) curvature tensor.

theorem CovariantDerivative.curvatureTensor_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle (↑⊤) F V I] (cov : CovariantDerivative I F V) [cov.ContMDiffCovariantDerivative ↑⊤] (x : M) {X Y : (y : M) → TangentSpace I y} {σ : (y : M) → V y} (hX : ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, X y⟩) (hY : ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, Y y⟩) (hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (y : M) => ⟨y, σ y⟩) : (((cov.curvatureTensor x) (X x)) (Y x)) (σ x) = cov.curvatureOperator X Y σ x

The pointwise tensor agrees with the curvature operator on any globally smooth vector fields and bundle section.

theorem CovariantDerivative.curvatureTensor_apply_of_contMDiffOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle (↑⊤) F V I] (cov : CovariantDerivative I F V) [cov.ContMDiffCovariantDerivative ↑⊤] (x : M) {U : Set M} (hU : IsOpen U) (hx : x ∈ U) {X Y : (y : M) → TangentSpace I y} {σ : (y : M) → V y} (hX : ContMDiffOn I I.tangent (↑⊤) (fun (y : M) => ⟨y, X y⟩) U) (hY : ContMDiffOn I I.tangent (↑⊤) (fun (y : M) => ⟨y, Y y⟩) U) (hσ : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ F)) (↑⊤) (fun (y : M) => ⟨y, σ y⟩) U) : (((cov.curvatureTensor x) (X x)) (Y x)) (σ x) = cov.curvatureOperator X Y σ x

The pointwise tensor agrees with the curvature operator on vector fields and a bundle section which are smooth on a neighbourhood of the point, such as the members of a local frame.

theorem CovariantDerivative.eq_curvatureTensor_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle (↑⊤) F V I] (cov : CovariantDerivative I F V) [cov.ContMDiffCovariantDerivative ↑⊤] (x : M) (R : TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] V x →ₗ[ℝ] V x) : R = cov.curvatureTensor x ↔ ∀ (X Y : (y : M) → TangentSpace I y) (σ : (y : M) → V y), (ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, X y⟩) → (ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, Y y⟩) → (ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (y : M) => ⟨y, σ y⟩) → ((R (X x)) (Y x)) (σ x) = cov.curvatureOperator X Y σ x

Evaluation on smooth sections uniquely characterizes the pointwise curvature tensor.

theorem CovariantDerivative.curvatureTensor_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle (↑⊤) F V I] (cov : CovariantDerivative I F V) [cov.ContMDiffCovariantDerivative ↑⊤] {cov' : CovariantDerivative I F V} [cov'.ContMDiffCovariantDerivative ↑⊤] (h : ∀ (σ : (y : M) → V y), (ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (y : M) => ⟨y, σ y⟩) → ∀ (y : M), ↑cov σ y = ↑cov' σ y) (x : M) : cov.curvatureTensor x = cov'.curvatureTensor x

Two smooth connections which agree on every smooth section have the same curvature tensor. A connection is unconstrained on sections which are not differentiable, so this is the form in which two connections determined by the same data, such as two Levi-Civita connections of one metric, are compared.

theorem CovariantDerivative.curvatureTensor_antisymm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle (↑⊤) F V I] (cov : CovariantDerivative I F V) [cov.ContMDiffCovariantDerivative ↑⊤] (x : M) (u v : TangentSpace I x) : ((cov.curvatureTensor x) u) v = -((cov.curvatureTensor x) v) u

Swapping the two tangent-vector arguments negates the curvature endomorphism.

@[simp]

theorem CovariantDerivative.curvatureTensor_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle (↑⊤) F V I] (cov : CovariantDerivative I F V) [cov.ContMDiffCovariantDerivative ↑⊤] (x : M) (u : TangentSpace I x) : ((cov.curvatureTensor x) u) u = 0

The curvature endomorphism vanishes when its tangent-vector arguments coincide.

theorem CovariantDerivative.curvatureTensor_eq_zero_of_finrank_le_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle (↑⊤) F V I] (cov : CovariantDerivative I F V) [cov.ContMDiffCovariantDerivative ↑⊤] (x : M) (hdim : Module.finrank ℝ (TangentSpace I x) ≤ 1) : cov.curvatureTensor x = 0

On a base of tangent dimension at most one, every smooth connection has zero curvature: the alternating pair of tangent arguments is necessarily dependent.