Warped products of Riemannian manifolds

Given Riemannian manifolds M and N and a nowhere vanishing function f : M → ℝ, the warped product M ×_f N is M × N with the Riemannian metric

⟪(u₁, u₂), (v₁, v₂)⟫ = ⟪u₁, v₁⟫ + f(x)² ⟪u₂, v₂⟫

at (x, y). The fibres {x} × N are copies of N rescaled by the constant f(x)², the horizontal slices M × {y} are isometric copies of M, and the two are orthogonal. A constant warping function f = 1 gives the product metric, which TauCeti.Geometry.Manifold.Riemannian.Prod.Basic constructs as that case. Warped products are the standard models of rotationally symmetric metrics: the Euclidean metric away from the origin is (0, ∞) ×_r S^(n-1), the round sphere minus two antipodal points is (0, π) ×_(sin r) S^(n-1), and hyperbolic space minus a point is (0, ∞) ×_(sinh r) S^(n-1).

The predicate TauCeti.Manifold.IsWarpedProduct I J N f says that the Riemannian metric installed on M × N is the warped product of the metrics installed on the factors. Geometric quantities of a warped product, such as its Levi-Civita connection, are computed for any metric satisfying it, so that they apply both to the construction below and to any metric shown to have the warped form.

Main definitions

• Bundle.RiemannianMetric.warpedProdTangentSpace: the warped product of two Riemannian metrics with a nowhere vanishing warping function.
• Bundle.ContMDiffRiemannianMetric.warpedProdTangentSpace: the warped product of two C^n Riemannian metrics with a nowhere vanishing C^n warping function, as a C^n Riemannian metric.
• TauCeti.Manifold.IsWarpedProduct: the metric of M × N is the warped product of the metrics of M and N with warping function f.

Main results

• TauCeti.Manifold.IsWarpedProduct.tangentSpaceProdLinearIsometryEquiv: multiplying the vertical tangent component by the warping function identifies the warped tangent space isometrically with the L² product of the factor tangent spaces.
• TauCeti.Manifold.isWarpedProduct_of_eq: the warped product metric is a warped product.
• TauCeti.Manifold.IsWarpedProduct.isContMDiffRiemannianBundle: a warped product of C^n metrics with a C^n warping function is C^n.

References

• R. L. Bishop and B. O'Neill, Manifolds of negative curvature, Trans. Amer. Math. Soc. 145 (1969), 1–49, Section 7.
• B. O'Neill, Semi-Riemannian Geometry, Academic Press (1983), Chapter 7.

noncomputable def Bundle.RiemannianMetric.warpedProdTangentSpace {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] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] (g₁ : RiemannianMetric fun (x : M) => TangentSpace I x) (f : M → ℝ) (hf : ∀ (x : M), f x ≠ 0) (g₂ : RiemannianMetric fun (y : N) => TangentSpace J y) : RiemannianMetric fun (p : M × N) => TangentSpace (I.prod J) p

The warped product of Riemannian metrics g₁ on M and g₂ on N with a nowhere vanishing warping function f : M → ℝ: the Riemannian metric on M × N whose inner product of tangent vectors (v₁, v₂) and (w₁, w₂) at (x, y) is g₁ x v₁ w₁ + f(x)² g₂ y v₂ w₂.

@[simp]

theorem Bundle.RiemannianMetric.warpedProdTangentSpace_inner {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] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] (g₁ : RiemannianMetric fun (x : M) => TangentSpace I x) (f : M → ℝ) (hf : ∀ (x : M), f x ≠ 0) (g₂ : RiemannianMetric fun (y : N) => TangentSpace J y) (p : M × N) (v w : TangentSpace (I.prod J) p) : (((g₁.warpedProdTangentSpace f hf g₂).inner p) v) w = ((g₁.inner p.1) ((TauCeti.Manifold.tangentSpaceProdEquiv p) v).1) ((TauCeti.Manifold.tangentSpaceProdEquiv p) w).1 + f p.1 ^ 2 * ((g₂.inner p.2) ((TauCeti.Manifold.tangentSpaceProdEquiv p) v).2) ((TauCeti.Manifold.tangentSpaceProdEquiv p) w).2

The warped product metric pairs tangent vectors factor by factor, with the second factor rescaled by the square of the warping function.

noncomputable def Bundle.ContMDiffRiemannianMetric.warpedProdTangentSpace {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] [IsManifold I 1 M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (g₁ : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (f : M → ℝ) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f) (hf₀ : ∀ (x : M), f x ≠ 0) (g₂ : ContMDiffRiemannianMetric J n F fun (y : N) => TangentSpace J y) : ContMDiffRiemannianMetric (I.prod J) n (E × F) fun (p : M × N) => TangentSpace (I.prod J) p

The warped product of C^n Riemannian metrics on M and N with a nowhere vanishing C^n warping function f : M → ℝ is a C^n Riemannian metric on M × N.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.warpedProdTangentSpace_inner {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] [IsManifold I 1 M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (g₁ : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (f : M → ℝ) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f) (hf₀ : ∀ (x : M), f x ≠ 0) (g₂ : ContMDiffRiemannianMetric J n F fun (y : N) => TangentSpace J y) (p : M × N) (v w : TangentSpace (I.prod J) p) : (((g₁.warpedProdTangentSpace f hf hf₀ g₂).inner p) v) w = ((g₁.inner p.1) ((TauCeti.Manifold.tangentSpaceProdEquiv p) v).1) ((TauCeti.Manifold.tangentSpaceProdEquiv p) w).1 + f p.1 ^ 2 * ((g₂.inner p.2) ((TauCeti.Manifold.tangentSpaceProdEquiv p) v).2) ((TauCeti.Manifold.tangentSpaceProdEquiv p) w).2

The warped product of C^n Riemannian metrics pairs tangent vectors factor by factor, with the second factor rescaled by the square of the warping function.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.warpedProdTangentSpace_toRiemannianMetric {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] [IsManifold I 1 M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (g₁ : ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) (f : M → ℝ) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f) (hf₀ : ∀ (x : M), f x ≠ 0) (g₂ : ContMDiffRiemannianMetric J n F fun (y : N) => TangentSpace J y) : (g₁.warpedProdTangentSpace f hf hf₀ g₂).toRiemannianMetric = g₁.toRiemannianMetric.warpedProdTangentSpace f hf₀ g₂.toRiemannianMetric

Forgetting smoothness after taking the warped product of two C^n Riemannian metrics gives the warped product of the underlying Riemannian metrics.

structure TauCeti.Manifold.IsWarpedProduct {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] {G : Type u_5} [TopologicalSpace G] (J : ModelWithCorners ℝ F G) (N : Type u_6) [TopologicalSpace N] [ChartedSpace G N] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [Bundle.RiemannianBundle fun (p : M × N) => TangentSpace (I.prod J) p] (f : M → ℝ) : Prop

The Riemannian metric installed on M × N is the warped product of the metrics of M and N with warping function f : M → ℝ: at (x, y) the inner product of (u₁, u₂) and (v₁, v₂) is ⟪u₁, v₁⟫ + f(x)² ⟪u₂, v₂⟫.

• inner_eq (p : M × N) (v w : TangentSpace (I.prod J) p) : inner ℝ v w = inner ℝ ((tangentSpaceProdEquiv p) v).1 ((tangentSpaceProdEquiv p) w).1 + f p.1 ^ 2 * inner ℝ ((tangentSpaceProdEquiv p) v).2 ((tangentSpaceProdEquiv p) w).2

  The inner product of the warped product.

noncomputable def TauCeti.Manifold.IsWarpedProduct.tangentSpaceProdLinearIsometryEquiv {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] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [Bundle.RiemannianBundle fun (p : M × N) => TangentSpace (I.prod J) p] {f : M → ℝ} (h : IsWarpedProduct I J N f) (p : M × N) (hf : f p.1 ≠ 0) : TangentSpace (I.prod J) p ≃ₗᵢ[ℝ] WithLp 2 (TangentSpace I p.1 × TangentSpace J p.2)

The tangent space of a warped product is isometric to the L² product of the factor tangent spaces after multiplying the vertical component by the warping function. The inverse divides the vertical component by that function, so it transports product orthonormal bases to orthonormal bases for the warped metric.

@[simp]

theorem TauCeti.Manifold.IsWarpedProduct.tangentSpaceProdLinearIsometryEquiv_apply {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] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [Bundle.RiemannianBundle fun (p : M × N) => TangentSpace (I.prod J) p] {f : M → ℝ} (h : IsWarpedProduct I J N f) (p : M × N) (hf : f p.1 ≠ 0) (v : TangentSpace (I.prod J) p) : (h.tangentSpaceProdLinearIsometryEquiv p hf) v = WithLp.toLp 2 (((tangentSpaceProdEquiv p) v).1, f p.1 • ((tangentSpaceProdEquiv p) v).2)

The warped tangent isometry multiplies precisely the vertical component by f.

@[simp]

theorem TauCeti.Manifold.IsWarpedProduct.tangentSpaceProdLinearIsometryEquiv_symm_apply {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] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [Bundle.RiemannianBundle fun (p : M × N) => TangentSpace (I.prod J) p] {f : M → ℝ} (h : IsWarpedProduct I J N f) (p : M × N) (hf : f p.1 ≠ 0) (v : WithLp 2 (TangentSpace I p.1 × TangentSpace J p.2)) : (h.tangentSpaceProdLinearIsometryEquiv p hf).symm v = (tangentSpaceProdEquiv p).symm (v.ofLp.1, (f p.1)⁻¹ • v.ofLp.2)

The inverse warped tangent isometry divides the vertical component by f.

theorem TauCeti.Manifold.IsWarpedProduct.eq_zero_of_warping_eq_zero {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] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [Bundle.RiemannianBundle fun (p : M × N) => TangentSpace (I.prod J) p] {f : M → ℝ} (h : IsWarpedProduct I J N f) {p : M × N} (hf₀ : f p.1 = 0) (a : TangentSpace J p.2) : a = 0

Where the warping function vanishes, a warped product has no vertical vectors, because the installed metric is positive definite.

theorem TauCeti.Manifold.isWarpedProduct_of_eq {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] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [Bundle.RiemannianBundle fun (p : M × N) => TangentSpace (I.prod J) p] {f : M → ℝ} (hf : ∀ (x : M), f x ≠ 0) (hg : Bundle.RiemannianBundle.g = Bundle.RiemannianBundle.g.warpedProdTangentSpace f hf Bundle.RiemannianBundle.g) : IsWarpedProduct I J N f

A metric on M × N equal to the warped product metric Bundle.RiemannianMetric.warpedProdTangentSpace of the metrics of M and N is a warped product.

theorem TauCeti.Manifold.IsWarpedProduct.isContMDiffRiemannianBundle {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] {G : Type u_5} [TopologicalSpace G] {J : ModelWithCorners ℝ F G} {N : Type u_6} [TopologicalSpace N] [ChartedSpace G N] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsManifold I 1 M] [IsManifold J 1 N] [Bundle.RiemannianBundle fun (p : M × N) => TangentSpace (I.prod J) p] {n : WithTop ℕ∞} {f : M → ℝ} [IsContMDiffRiemannianBundle I n E fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle J n F fun (y : N) => TangentSpace J y] (h : IsWarpedProduct I J N f) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) n f) : IsContMDiffRiemannianBundle (I.prod J) n (E × F) fun (p : M × N) => TangentSpace (I.prod J) p

A warped product of C^n metrics with a C^n warping function is a C^n metric.