The Levi-Civita connection of a warped product

Let M × N carry the warped product ⟪(u₁, u₂), (v₁, v₂)⟫ = ⟪u₁, v₁⟫ + f(x)² ⟪u₂, v₂⟫ of the Riemannian metrics of M and N (TauCeti.Manifold.IsWarpedProduct). Its Levi-Civita connection on a product vector field (Y₁, Y₂), in the direction (u₁, u₂) at (x, y), is

∇_(u₁, u₂) (Y₁, Y₂) = (∇_u₁ Y₁ - f ⟪u₂, Y₂⟫ grad f, ∇_u₂ Y₂ + (df(u₁) / f) Y₂ + (df(Y₁) / f) u₂),

where f, df and grad f are evaluated at x, and ⟪u₂, Y₂⟫ is the inner product of N. Splitting into horizontal fields X, Y (tangent to M) and vertical fields V, W (tangent to N), this is the classical description of Bishop and O'Neill:

• ∇_X Y is the horizontal lift of the Levi-Civita connection of M;
• ∇_X V = ∇_V X = (X f / f) V;
• ∇_V W is the Levi-Civita connection of N minus (⟪V, W⟫_warped / f) grad f.

Read off from these formulas, the slices M × {y} are totally geodesic, while the fibres {x} × N are totally umbilic, with second fundamental form -(⟪V, W⟫_warped / f) grad f; these consequences are not stated separately here. For f = 1 the formula is the Levi-Civita connection of the product metric (TauCeti.Manifold.leviCivitaConnection_prodVectorField).

As for products, the proof evaluates the Koszul formula on product fields. The inner product of two product fields is now a(x) + f(x)² b(y), whose derivative contributes the extra terms 2 f df(·) b.

The formula needs no nonvanishing hypothesis on f at the point considered: where f(x) = 0 the warped metric can only be nondegenerate if N is zero-dimensional, and the correction terms with 1 / f vanish with the convention a / 0 = 0.

Main results

• TauCeti.Manifold.IsWarpedProduct.koszul_prodVectorField: the Koszul expression of a warped product on product fields.
• TauCeti.Manifold.IsWarpedProduct.tangentSpaceProdEquiv_leviCivitaConnection_prodVectorField: the Levi-Civita connection of a warped product on product fields, in any direction.
• TauCeti.Manifold.IsWarpedProduct.tangentSpaceProdEquiv_leviCivitaConnection_prodVectorField_zero : its restriction to horizontal fields.

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, Proposition 35.

theorem TauCeti.Manifold.IsWarpedProduct.koszul_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 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 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 2 N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsContMDiffRiemannianBundle J 1 F fun (y : N) => TangentSpace J y] [Bundle.RiemannianBundle fun (p : M × N) => TangentSpace (I.prod J) p] {f : M → ℝ} {X₁ Y₁ Z₁ : (x : M) → TangentSpace I x} {X₂ Y₂ Z₂ : (y : N) → TangentSpace J y} {p : M × N} (h : IsWarpedProduct I J N f) (hf : MDiffAt f p.1) (hX₁ : (MDiffAt fun (x : M) => ⟨x, X₁ x⟩) p.1) (hY₁ : (MDiffAt fun (x : M) => ⟨x, Y₁ x⟩) p.1) (hZ₁ : (MDiffAt fun (x : M) => ⟨x, Z₁ x⟩) p.1) (hX₂ : (MDiffAt fun (y : N) => ⟨y, X₂ y⟩) p.2) (hY₂ : (MDiffAt fun (y : N) => ⟨y, Y₂ y⟩) p.2) (hZ₂ : (MDiffAt fun (y : N) => ⟨y, Z₂ y⟩) p.2) : koszul (I.prod J) (prodVectorField X₁ X₂) (prodVectorField Y₁ Y₂) (prodVectorField Z₁ Z₂) p = koszul I X₁ Y₁ Z₁ p.1 + f p.1 ^ 2 * koszul J X₂ Y₂ Z₂ p.2 + 2 * f p.1 * ((d% f p.1) (X₁ p.1) * inner ℝ (Y₂ p.2) (Z₂ p.2) + (d% f p.1) (Y₁ p.1) * inner ℝ (Z₂ p.2) (X₂ p.2) - (d% f p.1) (Z₁ p.1) * inner ℝ (X₂ p.2) (Y₂ p.2))

On product fields, the Koszul expression of a warped product with warping function f is K₁ + f² K₂ + 2 f (df(X₁) ⟪Y₂, Z₂⟫ + df(Y₁) ⟪Z₂, X₂⟫ - df(Z₁) ⟪X₂, Y₂⟫), where K₁ and K₂ are the Koszul expressions of the factors.

theorem TauCeti.Manifold.IsWarpedProduct.tangentSpaceProdEquiv_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 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 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 2 N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsContMDiffRiemannianBundle J 1 F fun (y : N) => TangentSpace J y] [Bundle.RiemannianBundle fun (p : M × N) => TangentSpace (I.prod J) p] {f : M → ℝ} {Y₁ : (x : M) → TangentSpace I x} {Y₂ : (y : N) → TangentSpace J y} {p : M × N} [IsContMDiffRiemannianBundle (I.prod J) 1 (E × F) fun (p : M × N) => TangentSpace (I.prod J) p] (h : IsWarpedProduct I J N f) (hf : MDiffAt f p.1) (hY₁ : (MDiffAt fun (x : M) => ⟨x, Y₁ x⟩) p.1) (hY₂ : (MDiffAt fun (y : N) => ⟨y, Y₂ y⟩) p.2) (v : TangentSpace (I.prod J) p) : (tangentSpaceProdEquiv p) ((↑(CovariantDerivative.leviCivitaConnection (I.prod J) (M × N)) (prodVectorField Y₁ Y₂) p) v) = ((↑(CovariantDerivative.leviCivitaConnection I M) Y₁ p.1) ((tangentSpaceProdEquiv p) v).1 - (f p.1 * inner ℝ ((tangentSpaceProdEquiv p) v).2 (Y₂ p.2)) • mgradient I f p.1, (↑(CovariantDerivative.leviCivitaConnection J N) Y₂ p.2) ((tangentSpaceProdEquiv p) v).2 + ((d% f p.1) ((tangentSpaceProdEquiv p) v).1 / f p.1) • Y₂ p.2 + ((d% f p.1) (Y₁ p.1) / f p.1) • ((tangentSpaceProdEquiv p) v).2)

The Levi-Civita connection of a warped product with warping function f, on a product field (Y₁, Y₂) in the direction v = (u₁, u₂) at p = (x, y):

∇_v (Y₁, Y₂) = (∇_u₁ Y₁ - f(x) ⟪u₂, Y₂ y⟫ grad f(x), ∇_u₂ Y₂ + (df_x(u₁) / f(x)) Y₂ y + (df_x(Y₁ x) / f(x)) u₂).

theorem TauCeti.Manifold.IsWarpedProduct.tangentSpaceProdEquiv_leviCivitaConnection_prodVectorField_zero {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 2 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 1 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 2 N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsContMDiffRiemannianBundle J 1 F fun (y : N) => TangentSpace J y] [Bundle.RiemannianBundle fun (p : M × N) => TangentSpace (I.prod J) p] {f : M → ℝ} {p : M × N} [IsContMDiffRiemannianBundle (I.prod J) 1 (E × F) fun (p : M × N) => TangentSpace (I.prod J) p] (h : IsWarpedProduct I J N f) {W : (x : M) → TangentSpace I x} (hf : MDiffAt f p.1) (hW : (MDiffAt fun (x : M) => ⟨x, W x⟩) p.1) (u : TangentSpace (I.prod J) p) : (tangentSpaceProdEquiv p) ((↑(CovariantDerivative.leviCivitaConnection (I.prod J) (M × N)) (prodVectorField W 0) p) u) = ((↑(CovariantDerivative.leviCivitaConnection I M) W p.1) ((tangentSpaceProdEquiv p) u).1, ((d% f p.1) (W p.1) / f p.1) • ((tangentSpaceProdEquiv p) u).2)

On a horizontal section W, the Levi-Civita connection of the warped product differs from the base connection only by the factor W f / f on the vertical component.