Curvature of a disjoint union of Riemannian manifolds

Let g₁ and g₂ be smooth Riemannian metrics on manifolds M and M' modelled on the same space, and let g₁ ⊔ g₂ be the metric on the disjoint union M ⊕ M' which is g₁ on M and g₂ on M' (Bundle.ContMDiffRiemannianMetric.sumTangentSpace). The inclusions of M and M' into M ⊕ M' are local Riemannian isometries, so every curvature quantity of g₁ ⊔ g₂ at a point of a summand is that of the metric of the summand. In particular the scalar curvature of g₁ ⊔ g₂ is Scal(g₁) on M and Scal(g₂) on M'.

Main results

• Bundle.ContMDiffRiemannianMetric.isLocalRiemannianIsometry_sumInl and Bundle.ContMDiffRiemannianMetric.isLocalRiemannianIsometry_sumInr: the inclusions of the summands are local Riemannian isometries.
• Bundle.ContMDiffRiemannianMetric.scalarCurvature_sumTangentSpace_inl and Bundle.ContMDiffRiemannianMetric.scalarCurvature_sumTangentSpace_inr: the scalar curvature of the disjoint union metric on each summand is that of the metric of the summand.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 2 (local isometries) and Proposition 7.6 (naturality of the curvature tensor).

theorem Bundle.ContMDiffRiemannianMetric.isLocalRiemannianIsometry_sumInl {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] {M' : Type u_4} [TopologicalSpace M'] [ChartedSpace H M'] [IsManifold I 1 M] [IsManifold I 1 M'] {n : WithTop ℕ∞} (g₁ : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (g₂ : ContMDiffRiemannianMetric I n E fun (x : M') => TangentSpace I x) : TauCeti.IsLocalRiemannianIsometry I I Sum.inl

The inclusion of M into M ⊕ M' is a local Riemannian isometry from g₁ to the disjoint union of g₁ and g₂.

theorem Bundle.ContMDiffRiemannianMetric.isLocalRiemannianIsometry_sumInr {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] {M' : Type u_4} [TopologicalSpace M'] [ChartedSpace H M'] [IsManifold I 1 M] [IsManifold I 1 M'] {n : WithTop ℕ∞} (g₁ : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (g₂ : ContMDiffRiemannianMetric I n E fun (x : M') => TangentSpace I x) : TauCeti.IsLocalRiemannianIsometry I I Sum.inr

The inclusion of M' into M ⊕ M' is a local Riemannian isometry from g₂ to the disjoint union of g₁ and g₂.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_sumTangentSpace_inl {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] {M' : Type u_4} [TopologicalSpace M'] [ChartedSpace H M'] [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] [T2Space M'] [IsManifold I (↑⊤) M'] (g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (g₂ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M') => TangentSpace I x) (x : M) : (g₁.sumTangentSpace g₂).scalarCurvature (Sum.inl x) = g₁.scalarCurvature x

The scalar curvature of the disjoint union of metrics g₁ and g₂ at a point of M is the scalar curvature of g₁ there.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.scalarCurvature_sumTangentSpace_inr {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] {M' : Type u_4} [TopologicalSpace M'] [ChartedSpace H M'] [FiniteDimensional ℝ E] [T2Space M] [IsManifold I (↑⊤) M] [T2Space M'] [IsManifold I (↑⊤) M'] (g₁ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (g₂ : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M') => TangentSpace I x) (y : M') : (g₁.sumTangentSpace g₂).scalarCurvature (Sum.inr y) = g₂.scalarCurvature y

The scalar curvature of the disjoint union of metrics g₁ and g₂ at a point of M' is the scalar curvature of g₂ there.