Curvature of a metric-compatible connection

The curvature endomorphisms of a metric-compatible connection are skew-adjoint: ⟪R(X,Y)σ, τ⟫ = -⟪σ, R(X,Y)τ⟫. The first theorem applies to C^n fields and C^(n + 1) sections for 1 ≤ n, under the corresponding finite regularity hypotheses; the second specializes it to the smooth pointwise curvature tensor on arbitrary fibre vectors.

Under these hypotheses this is antisymmetry in the last two arguments of the metric-lowered Riemann tensor. Together with antisymmetry in the first two arguments, it makes the sectional-curvature numerator transform by the square of the determinant under a change of basis of a tangent plane. No torsion-free hypothesis is required: the result holds for any metric-compatible connection on a finite-rank real bundle satisfying the stated manifold, bundle, metric, and base-model assumptions.

The metric and curvature conventions are those of J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), equation (5.1) and Chapter 7, pp. 196–198: R(X,Y)σ = ∇_X ∇_Y σ - ∇_Y ∇_X σ - ∇_[X,Y] σ.

The predicate Bundle.RiemannianMetric.IsConstantCurvatureTensor records the pointwise constant-curvature equation for an arbitrary smooth covariant derivative and a Riemannian metric. Its specialization Bundle.ContMDiffRiemannianMetric.IsConstantCurvatureTensor uses the Levi-Civita connection of a smooth metric, providing the curvature condition used by the hyperbolic-geometry layer.

theorem CovariantDerivative.IsMetricCompatible.inner_curvatureOperator_eq_neg {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] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → NormedAddCommGroup (V x)] [(x : M) → InnerProductSpace ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] {cov : CovariantDerivative I F V} [CompleteSpace E] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] [ContMDiffVectorBundle 1 F V I] (hn : 1 ≤ n) [hmetric : have x := ⋯; IsContMDiffRiemannianBundle I 2 F V] [hreg : have x := ⋯; cov.ContMDiffCovariantDerivative n] (hcov : cov.IsMetricCompatible) {X Y : (x : M) → TangentSpace I x} {σ τ : (x : M) → V x} (hX : have x := ⋯; ContMDiff I I.tangent n fun (x : M) => ⟨x, X x⟩) (hY : have x := ⋯; ContMDiff I I.tangent n fun (x : M) => ⟨x, Y x⟩) (hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) (n + 1) fun (x : M) => ⟨x, σ x⟩) (hτ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) (n + 1) fun (x : M) => ⟨x, τ x⟩) (x : M) : inner ℝ (cov.curvatureOperator X Y σ x) (τ x) = -inner ℝ (σ x) (cov.curvatureOperator X Y τ x)

A C^n metric-compatible connection has skew-adjoint curvature on C^n fields and C^(n + 1) sections, for 1 ≤ n. The base model may be infinite-dimensional, provided it is complete.

theorem CovariantDerivative.IsMetricCompatible.inner_curvatureTensor_eq_neg {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] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → NormedAddCommGroup (V x)] [(x : M) → InnerProductSpace ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] {cov : CovariantDerivative I F V} [IsManifold I (↑⊤) M] [ContMDiffVectorBundle (↑⊤) F V I] [cov.ContMDiffCovariantDerivative ↑⊤] [IsContMDiffRiemannianBundle I 2 F V] [FiniteDimensional ℝ E] [T2Space M] (hcov : cov.IsMetricCompatible) (x : M) (u v : TangentSpace I x) (w z : V x) : inner ℝ ((((cov.curvatureTensor x) u) v) w) z = -inner ℝ w ((((cov.curvatureTensor x) u) v) z)

Every pointwise curvature endomorphism of a smooth metric-compatible connection is skew-adjoint. For the tangent bundle, this is the last-pair antisymmetry of the Riemann curvature tensor after lowering its output index with the metric.

def Bundle.RiemannianMetric.IsConstantCurvatureTensor {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] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : RiemannianMetric fun (x : M) => TangentSpace I x) (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) (hcov : cov.ContMDiffCovariantDerivative ↑⊤) (κ : ℝ) : Prop

A connection has constant-curvature tensor κ when R(w,u)v = κ (⟪u,v⟫ w - ⟪w,v⟫ u) at every point.

theorem Bundle.RiemannianMetric.isConstantCurvatureTensor_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] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : RiemannianMetric fun (x : M) => TangentSpace I x) (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) (hcov : cov.ContMDiffCovariantDerivative ↑⊤) (κ : ℝ) : g.IsConstantCurvatureTensor cov hcov κ ↔ ∀ (x : M) (w u v : TangentSpace I x), (((cov.curvatureTensor x) w) u) v = κ • (Inner.inner ℝ u v • w - Inner.inner ℝ w v • u)

A connection has constant-curvature tensor κ precisely when it satisfies the constant-curvature equation on every tangent triple.

theorem Bundle.RiemannianMetric.IsConstantCurvatureTensor.curvatureTensor_eq {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] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : RiemannianMetric fun (x : M) => TangentSpace I x) (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) (hcov : cov.ContMDiffCovariantDerivative ↑⊤) (κ : ℝ) (h : g.IsConstantCurvatureTensor cov hcov κ) (x : M) (w u v : TangentSpace I x) : (((cov.curvatureTensor x) w) u) v = κ • (Inner.inner ℝ u v • w - Inner.inner ℝ w v • u)

The pointwise curvature equation carried by h.

def Bundle.ContMDiffRiemannianMetric.IsConstantCurvatureTensor {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] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (κ : ℝ) : Prop

The Levi-Civita connection of g has constant curvature κ.

theorem Bundle.ContMDiffRiemannianMetric.isConstantCurvatureTensor_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] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (κ : ℝ) : g.IsConstantCurvatureTensor κ ↔ ∀ (x : M) (w u v : TangentSpace I x), ((((CovariantDerivative.leviCivitaConnection I M).curvatureTensor x) w) u) v = κ • (Inner.inner ℝ u v • w - Inner.inner ℝ w v • u)

A smooth metric has constant-curvature tensor precisely when its Levi-Civita connection satisfies the constant-curvature equation on every tangent triple.

theorem Bundle.ContMDiffRiemannianMetric.IsConstantCurvatureTensor.curvatureTensor_eq {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] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (κ : ℝ) (h : g.IsConstantCurvatureTensor κ) (x : M) (w u v : TangentSpace I x) : ((((CovariantDerivative.leviCivitaConnection I M).curvatureTensor x) w) u) v = κ • (Inner.inner ℝ u v • w - Inner.inner ℝ w v • u)

The pointwise curvature equation carried by the smooth metric predicate h.

theorem Bundle.ContMDiffRiemannianMetric.curvatureTensor_leviCivitaConnection_eq_of_riemannianBundle_eq {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] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [inst : RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (hg : RiemannianBundle.g = g.toRiemannianMetric) (x : M) : (CovariantDerivative.leviCivitaConnection I M).curvatureTensor x = (CovariantDerivative.leviCivitaConnection I M).curvatureTensor x

If the installed fibre metric is g, the curvature tensor of the Levi-Civita connection is that of g installed explicitly. This transports curvature along an equality of fibre metrics, such as Bundle.ContMDiffRiemannianMetric.rescale_one, which cannot be rewritten inside the instance-dependent arguments.

theorem Bundle.ContMDiffRiemannianMetric.isConstantCurvatureTensor_iff_of_riemannianBundle_eq {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] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [inst : RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (hg : RiemannianBundle.g = g.toRiemannianMetric) (κ : ℝ) : g.IsConstantCurvatureTensor κ ↔ ∀ (x : M) (w u v : TangentSpace I x), ((((CovariantDerivative.leviCivitaConnection I M).curvatureTensor x) w) u) v = κ • (Inner.inner ℝ u v • w - Inner.inner ℝ w v • u)

If the installed fibre metric is g, then g has constant-curvature tensor κ exactly when the Levi-Civita connection satisfies the constant-curvature equation for the installed inner product. This transports the predicate along an equality of fibre metrics, such as Bundle.ContMDiffRiemannianMetric.toRiemannianMetric_ofLE.