Products of Riemannian manifolds #
The product M × N of two Riemannian manifolds carries the product Riemannian metric, in which
the inner product of tangent vectors (v₁, v₂) and (w₁, w₂) at (x, y) is
⟪v₁, w₁⟫ + ⟪v₂, w₂⟫: the two factors are orthogonal and each carries its own metric. This is
the warped product (TauCeti.Geometry.Manifold.Riemannian.WarpedProd) with constant warping
function 1. This file constructs that metric as that case and shows that it is C^n,
respectively continuous, when the metrics of both factors are. Products such as S² × ℝ and
ℍ² × ℝ are among Thurston's model geometries, and isometries of products are in
TauCeti.Geometry.Manifold.Riemannian.Isometry.Prod.Basic.
Main definitions #
Bundle.RiemannianMetric.prodTangentSpace: the product of two Riemannian metrics.Bundle.ContMDiffRiemannianMetric.prodTangentSpace: the product of twoC^nRiemannian metrics, as aC^nRiemannian metric.TauCeti.Manifold.instRiemannianBundleProd,TauCeti.Manifold.instIsContinuousRiemannianBundleProd, andTauCeti.Manifold.instIsContMDiffRiemannianBundleProd: the corresponding instances, in theTauCetiscope; useopen scoped TauCetito install them.
Main results #
TauCeti.Manifold.inner_tangentSpace_prod: the inner product of the product metric is the sum of the inner products of the components.TauCeti.Manifold.isWarpedProduct_one: the product metric is the warped product with warping function1.TauCeti.Manifold.inner_tangentSpace_prod_mk_zeroandTauCeti.Manifold.inner_tangentSpace_prod_zero_mk: tangent vectors supported in one factor have that factor's inner product.TauCeti.Manifold.tangentSpaceProdLinearIsometryEquiv: in the product metric, the tangent space ofM × Nis isometric to theL²product of the tangent spaces of the factors.
References #
- J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176, Chapter 2 (product metrics).
noncomputable def
Bundle.RiemannianMetric.prodTangentSpace
{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)
(g₂ : RiemannianMetric fun (y : N) => TangentSpace J y)
:
RiemannianMetric fun (p : M × N) => TangentSpace (I.prod J) p
The product of Riemannian metrics g₁ on M and g₂ on N: 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₁ + g₂ y v₂ w₂. This is the warped product warpedProdTangentSpace with warping
function 1, whose properties it inherits; its inner product drops the factor 1 ^ 2, so that it
pairs the factors definitionally.
Instances For
@[simp]
theorem
Bundle.RiemannianMetric.prodTangentSpace_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)
(g₂ : RiemannianMetric fun (y : N) => TangentSpace J y)
(p : M × N)
(v w : TangentSpace (I.prod J) p)
:
(((g₁.prodTangentSpace g₂).inner p) v) w = ((g₁.inner p.1) ((TauCeti.Manifold.tangentSpaceProdEquiv p) v).1) ((TauCeti.Manifold.tangentSpaceProdEquiv p) w).1 + ((g₂.inner p.2) ((TauCeti.Manifold.tangentSpaceProdEquiv p) v).2) ((TauCeti.Manifold.tangentSpaceProdEquiv p) w).2
The product metric pairs tangent vectors factor by factor.
noncomputable def
Bundle.ContMDiffRiemannianMetric.prodTangentSpace
{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)
(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 product of C^n Riemannian metrics on M and N is a C^n Riemannian metric on
M × N.
Instances For
@[simp]
theorem
Bundle.ContMDiffRiemannianMetric.prodTangentSpace_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)
(g₂ : ContMDiffRiemannianMetric J n F fun (y : N) => TangentSpace J y)
(p : M × N)
(v w : TangentSpace (I.prod J) p)
:
(((g₁.prodTangentSpace g₂).inner p) v) w = ((g₁.inner p.1) ((TauCeti.Manifold.tangentSpaceProdEquiv p) v).1) ((TauCeti.Manifold.tangentSpaceProdEquiv p) w).1 + ((g₂.inner p.2) ((TauCeti.Manifold.tangentSpaceProdEquiv p) v).2) ((TauCeti.Manifold.tangentSpaceProdEquiv p) w).2
The product of C^n Riemannian metrics pairs tangent vectors factor by factor.
@[simp]
theorem
Bundle.ContMDiffRiemannianMetric.prodTangentSpace_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)
(g₂ : ContMDiffRiemannianMetric J n F fun (y : N) => TangentSpace J y)
:
Forgetting smoothness after taking the product of two C^n Riemannian metrics gives the
product of the underlying Riemannian metrics.
@[instance_reducible]
noncomputable def
TauCeti.Manifold.instRiemannianBundleProd
{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
A product of Riemannian manifolds carries the product Riemannian metric.
Instances For
@[simp]
theorem
TauCeti.Manifold.riemannianBundleProd_g
{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]
:
The metric installed on a product is the product of the metrics of the factors.
@[simp]
theorem
TauCeti.Manifold.inner_tangentSpace_prod
{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]
(p : M × N)
(v w : TangentSpace (I.prod J) p)
:
inner ℝ v w = inner ℝ ((tangentSpaceProdEquiv p) v).1 ((tangentSpaceProdEquiv p) w).1 + inner ℝ ((tangentSpaceProdEquiv p) v).2 ((tangentSpaceProdEquiv p) w).2
In the product metric, the inner product of two tangent vectors is the sum of the inner products of their components.
theorem
TauCeti.Manifold.isWarpedProduct_one
{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]
:
IsWarpedProduct I J N fun (x : M) => 1
The product metric is the warped product with the constant warping function 1.
theorem
TauCeti.Manifold.instIsContinuousRiemannianBundleProd
{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]
[IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x]
[IsContinuousRiemannianBundle F fun (y : N) => TangentSpace J y]
:
IsContinuousRiemannianBundle (E × F) fun (p : M × N) => TangentSpace (I.prod J) p
The product metric is continuous when the metrics of both factors are.
theorem
TauCeti.Manifold.instIsContMDiffRiemannianBundleProd
{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]
{n : WithTop ℕ∞}
[IsManifold I 1 M]
[IsManifold J 1 N]
[IsContMDiffRiemannianBundle I n E fun (x : M) => TangentSpace I x]
[IsContMDiffRiemannianBundle J n F fun (y : N) => TangentSpace J y]
:
IsContMDiffRiemannianBundle (I.prod J) n (E × F) fun (p : M × N) => TangentSpace (I.prod J) p
The product metric is C^n when the metrics of both factors are.
@[simp]
theorem
TauCeti.Manifold.inner_tangentSpace_prod_mk_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]
(p : M × N)
(v w : TangentSpace I p.1)
:
Tangent vectors supported in the first factor have that factor's inner product.
@[simp]
theorem
TauCeti.Manifold.inner_tangentSpace_prod_zero_mk
{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]
(p : M × N)
(v w : TangentSpace J p.2)
:
Tangent vectors supported in the second factor have that factor's inner product.
noncomputable def
TauCeti.Manifold.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]
(p : M × N)
:
In the product metric, the tangent space of M × N at p is isometric to the L² product of
the tangent spaces of the factors, via the canonical identification tangentSpaceProdEquiv.
Orthonormal bases of the two factors therefore combine into an orthonormal basis of the product
(OrthonormalBasis.prod).
Instances For
@[simp]
theorem
TauCeti.Manifold.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]
(p : M × N)
(v : TangentSpace (I.prod J) p)
:
@[simp]
theorem
TauCeti.Manifold.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]
(p : M × N)
(v : WithLp 2 (TangentSpace I p.1 × TangentSpace J p.2))
: