Curvature of a product metric

Give M × N the product of smooth Riemannian metrics on M and N. Its Riemann curvature tensor is the product of the curvature tensors of the factors:

R((u₁, u₂), (v₁, v₂)) (w₁, w₂) = (R(u₁, v₁) w₁, R(u₂, v₂) w₂),

its Ricci tensor is the sum of the Ricci tensors of the factors:

Ric((u₁, u₂), (v₁, v₂)) = Ric(u₁, v₁) + Ric(u₂, v₂),

and its scalar curvature is the sum of the scalar curvatures of the factors:

Scal(x, y) = Scal(x) + Scal(y).

So mixed curvature terms vanish, and a flat factor contributes nothing to the Ricci tensor. This reduces the Ricci tensor of the product geometries S² × ℝ and ℍ² × ℝ to that of their surface factor. Since every isometry preserves the Ricci tensor (TauCeti.IsLocalRiemannianIsometry.ricciTensor_mfderiv), it is the curvature input for showing that the isometries of these geometries preserve the line factor. The scalar curvature formula is the input for constructing metrics of positive scalar curvature on products.

The curvature tensor is evaluated on smooth product fields, on which the Levi-Civita connection of the product acts factor by factor (TauCeti.Manifold.leviCivitaConnection_prodVectorField) and whose Lie brackets are computed factor by factor (TauCeti.Manifold.mlieBracket_prodVectorField).

Main results

• TauCeti.Manifold.curvatureOperator_leviCivitaConnection_prodVectorField: the curvature operator of the product metric on smooth product fields.
• TauCeti.Manifold.tangentSpaceProdEquiv_curvatureTensor_leviCivitaConnection_prod: the curvature tensor of the product metric is the product of the curvature tensors.
• TauCeti.Manifold.ricciTensor_leviCivitaConnection_prod: the Ricci tensor of the product metric is the sum of the Ricci tensors.
• TauCeti.Manifold.scalarCurvature_leviCivitaConnection_prod: the scalar curvature of the product metric is the sum of the scalar curvatures.
• Bundle.ContMDiffRiemannianMetric.scalarCurvature_prodTangentSpace: the same for the product Bundle.ContMDiffRiemannianMetric.prodTangentSpace of two smooth metrics.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 7 (the curvature tensor, the Ricci tensor and the scalar curvature).

theorem TauCeti.Manifold.curvatureOperator_leviCivitaConnection_prodVectorField {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] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J (↑⊤) N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsContMDiffRiemannianBundle J (↑⊤) F fun (y : N) => TangentSpace J y] {X₁ Y₁ Z₁ : (x : M) → TangentSpace I x} {X₂ Y₂ Z₂ : (y : N) → TangentSpace J y} (hX₁ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X₁ x⟩) (hY₁ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y₁ x⟩) (hZ₁ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z₁ x⟩) (hX₂ : ContMDiff J J.tangent ↑⊤ fun (y : N) => ⟨y, X₂ y⟩) (hY₂ : ContMDiff J J.tangent ↑⊤ fun (y : N) => ⟨y, Y₂ y⟩) (hZ₂ : ContMDiff J J.tangent ↑⊤ fun (y : N) => ⟨y, Z₂ y⟩) : (CovariantDerivative.leviCivitaConnection (I.prod J) (M × N)).curvatureOperator (prodVectorField X₁ X₂) (prodVectorField Y₁ Y₂) (prodVectorField Z₁ Z₂) = prodVectorField ((CovariantDerivative.leviCivitaConnection I M).curvatureOperator X₁ Y₁ Z₁) ((CovariantDerivative.leviCivitaConnection J N).curvatureOperator X₂ Y₂ Z₂)

The curvature operator of the product metric on smooth product fields is the product of the curvature operators of the factors.

theorem TauCeti.Manifold.tangentSpaceProdEquiv_curvatureTensor_leviCivitaConnection_prod {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] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J (↑⊤) N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsContMDiffRiemannianBundle J (↑⊤) F fun (y : N) => TangentSpace J y] [T2Space M] [T2Space N] (p : M × N) (u v w : TangentSpace (I.prod J) p) : (tangentSpaceProdEquiv p) (((((CovariantDerivative.leviCivitaConnection (I.prod J) (M × N)).curvatureTensor p) u) v) w) = (((((CovariantDerivative.leviCivitaConnection I M).curvatureTensor p.1) ((tangentSpaceProdEquiv p) u).1) ((tangentSpaceProdEquiv p) v).1) ((tangentSpaceProdEquiv p) w).1, ((((CovariantDerivative.leviCivitaConnection J N).curvatureTensor p.2) ((tangentSpaceProdEquiv p) u).2) ((tangentSpaceProdEquiv p) v).2) ((tangentSpaceProdEquiv p) w).2)

The curvature tensor of a product metric is the product of the curvature tensors of the factors: R((u₁, u₂), (v₁, v₂)) (w₁, w₂) = (R(u₁, v₁) w₁, R(u₂, v₂) w₂).

theorem TauCeti.Manifold.ricciTensor_leviCivitaConnection_prod {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] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J (↑⊤) N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsContMDiffRiemannianBundle J (↑⊤) F fun (y : N) => TangentSpace J y] [T2Space M] [T2Space N] (p : M × N) (u v : TangentSpace (I.prod J) p) : (((CovariantDerivative.leviCivitaConnection (I.prod J) (M × N)).ricciTensor p) u) v = (((CovariantDerivative.leviCivitaConnection I M).ricciTensor p.1) ((tangentSpaceProdEquiv p) u).1) ((tangentSpaceProdEquiv p) v).1 + (((CovariantDerivative.leviCivitaConnection J N).ricciTensor p.2) ((tangentSpaceProdEquiv p) u).2) ((tangentSpaceProdEquiv p) v).2

The Ricci tensor of a product metric is the sum of the Ricci tensors of the factors: Ric((u₁, u₂), (v₁, v₂)) = Ric(u₁, v₁) + Ric(u₂, v₂).

theorem TauCeti.Manifold.scalarCurvature_leviCivitaConnection_prod {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] [IsManifold I (↑⊤) M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J (↑⊤) N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsContMDiffRiemannianBundle J (↑⊤) F fun (y : N) => TangentSpace J y] [T2Space M] [T2Space N] (p : M × N) : (CovariantDerivative.leviCivitaConnection (I.prod J) (M × N)).scalarCurvature p = (CovariantDerivative.leviCivitaConnection I M).scalarCurvature p.1 + (CovariantDerivative.leviCivitaConnection J N).scalarCurvature p.2

The scalar curvature of a product metric is the sum of the scalar curvatures of the factors: Scal(x, y) = Scal(x) + Scal(y).

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_prodTangentSpace {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] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [T2Space N] [ChartedSpace G N] [IsManifold J (↑⊤) N] (g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (g₂ : ContMDiffRiemannianMetric J (↑⊤) F fun (y : N) => TangentSpace J y) (p : M × N) : (g₁.prodTangentSpace g₂).scalarCurvature p = g₁.scalarCurvature p.1 + g₂.scalarCurvature p.2

The scalar curvature of a product metric g₁ × g₂ is the sum of the scalar curvatures of the factors: Scal(x, y) = Scal_{g₁}(x) + Scal_{g₂}(y).