Disjoint unions of Riemannian manifolds

The disjoint union M ⊕ M' of two manifolds modelled on the same space carries the Riemannian metric which is a given metric g₁ on M and a given metric g₂ on M'. This file constructs that metric and shows that it is C^n when g₁ and g₂ are. Each summand is open in M ⊕ M' and its charts are those of the summand, so near a point of M the tangent-bundle trivializations of M ⊕ M' are those of M, and the metric there is read in the same coordinates as g₁.

Disjoint unions are how manifolds with several components, such as the boundary of a bordism, are assembled from connected pieces; the curvature of the disjoint union metric is computed in TauCeti.Geometry.Manifold.Riemannian.Isometry.Sum.

Main definitions and results

• Bundle.ContMDiffRiemannianMetric.sumTangentSpace: the disjoint union of two C^n Riemannian metrics, as a C^n Riemannian metric.
• Bundle.ContMDiffRiemannianMetric.sumTangentSpace_inner_inl and Bundle.ContMDiffRiemannianMetric.sumTangentSpace_inner_inr: it restricts to the given metrics on the two summands.

def Bundle.ContMDiffRiemannianMetric.sumTangentSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {M' : Type u_4} [TopologicalSpace M'] [ChartedSpace H M'] [IsManifold I 1 M'] (g₁ : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (g₂ : ContMDiffRiemannianMetric I n E fun (x : M') => TangentSpace I x) : ContMDiffRiemannianMetric I n E fun (p : M ⊕ M') => TangentSpace I p

The disjoint union of C^n Riemannian metrics g₁ on M and g₂ on M': the C^n Riemannian metric on M ⊕ M' which is g₁ on M and g₂ on M'.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.sumTangentSpace_inner_inl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {M' : Type u_4} [TopologicalSpace M'] [ChartedSpace H M'] [IsManifold I 1 M'] (g₁ : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (g₂ : ContMDiffRiemannianMetric I n E fun (x : M') => TangentSpace I x) (x : M) (v w : TangentSpace I x) : (((g₁.sumTangentSpace g₂).inner (Sum.inl x)) v) w = ((g₁.inner x) v) w

On M, the disjoint union of the metrics g₁ and g₂ is g₁.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.sumTangentSpace_inner_inr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {M' : Type u_4} [TopologicalSpace M'] [ChartedSpace H M'] [IsManifold I 1 M'] (g₁ : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (g₂ : ContMDiffRiemannianMetric I n E fun (x : M') => TangentSpace I x) (y : M') (v w : TangentSpace I y) : (((g₁.sumTangentSpace g₂).inner (Sum.inr y)) v) w = ((g₂.inner y) v) w

On M', the disjoint union of the metrics g₁ and g₂ is g₂.