Documentation

TauCeti.Geometry.Manifold.VectorBundle.CovariantDerivative.Curvature.Riemann

The metric-lowered Riemann curvature tensor #

Pairing the output of the pointwise (1,3) curvature tensor with the metric gives the (0,4) Riemann curvature tensor

Rm(u, v, w, z) = ⟨R(u, v)w, z⟩.

This file bundles that expression as a quadrilinear map and records its algebraic symmetries. Every connection gives antisymmetry in the first pair. Metric compatibility gives antisymmetry in the last pair, torsion-freeness gives the first Bianchi identity, and together these imply pair-interchange symmetry. The latter symmetry also makes the Ricci contraction symmetric. By polarization, these symmetries determine Rm from its values Rm(u, v, v, u) on linearly independent pairs u, v, the numerators of the sectional curvatures.

The sign and argument conventions follow J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 7.

Main declarations #

source
noncomputable def CovariantDerivative.riemannCurvatureTensor {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] [Bundle.RiemannianBundle (TangentSpace I)] (cov : CovariantDerivative I E (TangentSpace I)) [cov.ContMDiffCovariantDerivative ↑⊤] (x : M) :
TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] ℝ

The metric-lowered Riemann curvature tensor, with convention Rm(u, v, w, z) = ⟨R(u, v)w, z⟩.

Instances For
    source
    @[simp]
    theorem CovariantDerivative.riemannCurvatureTensor_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] [Bundle.RiemannianBundle (TangentSpace I)] (cov : CovariantDerivative I E (TangentSpace I)) [cov.ContMDiffCovariantDerivative ↑⊤] (x : M) (u v w z : TangentSpace I x) :
    ((((cov.riemannCurvatureTensor x) u) v) w) z = inner ℝ ((((cov.curvatureTensor x) u) v) w) z

    Evaluation of the metric-lowered Riemann curvature tensor.

    source
    theorem CovariantDerivative.ricciTensor_eq_sum_riemannCurvatureTensor {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] [Bundle.RiemannianBundle (TangentSpace I)] (cov : CovariantDerivative I E (TangentSpace I)) [cov.ContMDiffCovariantDerivative ↑⊤] {i : Type u_4} [Fintype i] (x : M) (b : OrthonormalBasis i ℝ (TangentSpace I x)) (u v : TangentSpace I x) :
    ((cov.ricciTensor x) u) v = ∑ j : i, ((((cov.riemannCurvatureTensor x) (b j)) u) v) (b j)

    In an orthonormal basis, Ricci curvature is the contraction of the first and fourth arguments of the Riemann curvature tensor.

    source
    theorem CovariantDerivative.scalarCurvature_eq_sum_riemannCurvatureTensor {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] [Bundle.RiemannianBundle (TangentSpace I)] (cov : CovariantDerivative I E (TangentSpace I)) [cov.ContMDiffCovariantDerivative ↑⊤] {i : Type u_4} [Fintype i] (x : M) (b : OrthonormalBasis i ℝ (TangentSpace I x)) :
    cov.scalarCurvature x = ∑ j : i, ∑ k : i, ((((cov.riemannCurvatureTensor x) (b k)) (b j)) (b j)) (b k)

    In an orthonormal basis, scalar curvature is the double contraction of the Riemann curvature tensor.

    source
    theorem CovariantDerivative.riemannCurvatureTensor_antisymm_first {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] [Bundle.RiemannianBundle (TangentSpace I)] (cov : CovariantDerivative I E (TangentSpace I)) [cov.ContMDiffCovariantDerivative ↑⊤] (x : M) (u v w z : TangentSpace I x) :
    ((((cov.riemannCurvatureTensor x) u) v) w) z = -((((cov.riemannCurvatureTensor x) v) u) w) z

    The Riemann curvature tensor is antisymmetric in its first pair of arguments.

    source
    theorem CovariantDerivative.riemannCurvatureTensor_cyclic_eq_zero {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] [Bundle.RiemannianBundle (TangentSpace I)] (cov : CovariantDerivative I E (TangentSpace I)) [cov.ContMDiffCovariantDerivative ↑⊤] (ht : cov.torsion = 0) (x : M) (u v w z : TangentSpace I x) :
    ((((cov.riemannCurvatureTensor x) u) v) w) z + ((((cov.riemannCurvatureTensor x) v) w) u) z + ((((cov.riemannCurvatureTensor x) w) u) v) z = 0

    For a torsion-free connection, the cyclic sum of the first three arguments of the Riemann curvature tensor vanishes.

    source
    theorem CovariantDerivative.IsMetricCompatible.riemannCurvatureTensor_antisymm_last {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] [Bundle.RiemannianBundle (TangentSpace I)] (cov : CovariantDerivative I E (TangentSpace I)) [cov.ContMDiffCovariantDerivative ↑⊤] [IsContMDiffRiemannianBundle I 2 E (TangentSpace I)] (hcov : cov.IsMetricCompatible) (x : M) (u v w z : TangentSpace I x) :
    ((((cov.riemannCurvatureTensor x) u) v) w) z = -((((cov.riemannCurvatureTensor x) u) v) z) w

    For a metric-compatible connection, the Riemann curvature tensor is antisymmetric in its last pair of arguments.

    source
    theorem CovariantDerivative.IsMetricCompatible.riemannCurvatureTensor_swap_pairs {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] [Bundle.RiemannianBundle (TangentSpace I)] (cov : CovariantDerivative I E (TangentSpace I)) [cov.ContMDiffCovariantDerivative ↑⊤] [IsContMDiffRiemannianBundle I 2 E (TangentSpace I)] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (x : M) (u v w z : TangentSpace I x) :
    ((((cov.riemannCurvatureTensor x) u) v) w) z = ((((cov.riemannCurvatureTensor x) w) z) u) v

    The Riemann curvature tensor of a metric-compatible torsion-free connection is unchanged when its two pairs of arguments are interchanged.

    source
    theorem CovariantDerivative.IsMetricCompatible.riemannCurvatureTensor_eq_of_forall_linearIndependent {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] [Bundle.RiemannianBundle (TangentSpace I)] {cov : CovariantDerivative I E (TangentSpace I)} [cov.ContMDiffCovariantDerivative ↑⊤] [IsContMDiffRiemannianBundle I 2 E (TangentSpace I)] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (x : M) {T : TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] ℝ} (h₁ : ∀ (u v w z : TangentSpace I x), (((T u) v) w) z = -(((T v) u) w) z) (h₂ : ∀ (u v w z : TangentSpace I x), (((T u) v) w) z = -(((T u) v) z) w) (h₃ : ∀ (u v w z : TangentSpace I x), (((T u) v) w) z + (((T v) w) u) z + (((T w) u) v) z = 0) (hT : ∀ (u v : TangentSpace I x), LinearIndependent ℝ ![u, v] → ((((cov.riemannCurvatureTensor x) u) v) v) u = (((T u) v) v) u) :
    cov.riemannCurvatureTensor x = T

    For a metric-compatible torsion-free connection, the Riemann curvature tensor at x is the only quadrilinear form with the algebraic symmetries of a curvature tensor whose values T(u, v, v, u) on linearly independent pairs are the sectional-curvature numerators ⟨R(u, v)v, u⟩.