Local Riemannian isometries #
A local Riemannian isometry f : M → N is a smooth map whose differential at every point is an
invertible linear map preserving the Riemannian inner product. Unlike a Riemannian isometry
(TauCeti.RiemannianIsometry), it need not be injective or surjective: the inclusion of an open
submanifold carrying the restricted metric, the inclusion of one component of a disjoint union, and
a Riemannian covering map are all local Riemannian isometries.
Every local construction of Riemannian geometry is natural under local Riemannian isometries,
since pulling vector fields back along f only involves the differential of f at each point.
This file sets up the pointwise API used to transport the Levi-Civita connection and the curvature
along such maps.
Main definitions and results #
TauCeti.IsLocalRiemannianIsometry: a smooth map with invertible differentials preserving the inner product.TauCeti.IsLocalRiemannianIsometry.exists_linearIsometryEquiv_eq_mfderiv: the differential at each point is a linear isometric equivalence of tangent spaces.TauCeti.IsLocalRiemannianIsometry.mfderiv_apply_mpullback: the differential sends a pulled-back vector field to the original field.TauCeti.IsLocalRiemannianIsometry.inner_mpullback: pulling back vector fields preserves their pointwise inner products.TauCeti.IsLocalRiemannianIsometry.exists_contMDiff_mpullback_apply_eq: every tangent vector is the value of the pullback of a smooth vector field.TauCeti.IsLocalRiemannianIsometry.idandTauCeti.IsLocalRiemannianIsometry.comp: the identity and composites.TauCeti.RiemannianIsometry.isLocalRiemannianIsometry: a Riemannian isometry is a local Riemannian isometry.
References #
- J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 2 (local isometries).
structure
TauCeti.IsLocalRiemannianIsometry
{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]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
(J : ModelWithCorners ℝ F H')
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(f : M → N)
:
A smooth map f : M → N between Riemannian manifolds is a local Riemannian isometry if its
differential at every point is an invertible continuous linear map preserving the inner product
of tangent vectors.
A local Riemannian isometry is smooth.
- isInvertible_mfderiv (x : M) : (mfderiv% f x).IsInvertible
The differential of a local Riemannian isometry is invertible at every point.
- inner_mfderiv (x : M) (v w : TangentSpace I x) : inner ℝ ((mfderiv% f x) v) ((mfderiv% f x) w) = inner ℝ v w
The differential of a local Riemannian isometry preserves the inner product.
Instances For
theorem
TauCeti.IsLocalRiemannianIsometry.mdifferentiableAt
{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]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
{f : M → N}
(hf : IsLocalRiemannianIsometry I J f)
(x : M)
:
MDiffAt f x
A local Riemannian isometry is differentiable at each point.
theorem
TauCeti.IsLocalRiemannianIsometry.mfderiv_injective
{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]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
{f : M → N}
(hf : IsLocalRiemannianIsometry I J f)
(x : M)
:
Function.Injective ⇑(mfderiv% f x)
The differential of a local Riemannian isometry at a point is injective.
theorem
TauCeti.IsLocalRiemannianIsometry.mfderiv_surjective
{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]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
{f : M → N}
(hf : IsLocalRiemannianIsometry I J f)
(x : M)
:
Function.Surjective ⇑(mfderiv% f x)
The differential of a local Riemannian isometry at a point is surjective onto the tangent space at the image point.
theorem
TauCeti.IsLocalRiemannianIsometry.exists_linearIsometryEquiv_eq_mfderiv
{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]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
{f : M → N}
(hf : IsLocalRiemannianIsometry I J f)
(x : M)
:
∃ (e : TangentSpace I x ≃ₗᵢ[ℝ] TangentSpace J (f x)), ∀ (v : TangentSpace I x), e v = (mfderiv% f x) v
The differential of a local Riemannian isometry at a point is a linear isometric equivalence of tangent spaces.
@[simp]
theorem
TauCeti.IsLocalRiemannianIsometry.mfderiv_apply_mpullback
{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]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
{f : M → N}
(hf : IsLocalRiemannianIsometry I J f)
(V : (y : N) → TangentSpace J y)
(x : M)
:
The differential of a local Riemannian isometry sends the pullback of a vector field at x to
the value of the field at f x.
theorem
TauCeti.IsLocalRiemannianIsometry.mpullback_apply_eq_iff
{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]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
{f : M → N}
(hf : IsLocalRiemannianIsometry I J f)
(V : (y : N) → TangentSpace J y)
{x : M}
(v : TangentSpace I x)
:
The pullback of a vector field along a local Riemannian isometry takes the value v at x
exactly when the field takes the value df_x v at f x.
@[simp]
theorem
TauCeti.IsLocalRiemannianIsometry.inner_mpullback
{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]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
{f : M → N}
(hf : IsLocalRiemannianIsometry I J f)
(Y Z : (y : N) → TangentSpace J y)
(x : M)
:
inner ℝ (VectorField.mpullback I J f Y x) (VectorField.mpullback I J f Z x) = inner ℝ (Y (f x)) (Z (f x))
Pulling back vector fields along a local Riemannian isometry preserves their pointwise inner products.
theorem
TauCeti.IsLocalRiemannianIsometry.mdifferentiableAt_mpullback
{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]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
{f : M → N}
[CompleteSpace E]
[IsManifold I 2 M]
[IsManifold J 2 N]
(hf : IsLocalRiemannianIsometry I J f)
{V : (y : N) → TangentSpace J y}
{x : M}
(hV : (MDiffAt fun (y : N) => ⟨y, V y⟩) (f x))
:
(MDiffAt fun (x : M) => ⟨x, VectorField.mpullback I J f V x⟩) x
Pulling back a differentiable vector field along a local Riemannian isometry gives a differentiable vector field.
theorem
TauCeti.IsLocalRiemannianIsometry.contMDiff_mpullback
{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]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
{f : M → N}
[CompleteSpace E]
[IsManifold I 2 M]
[IsManifold J 2 N]
(hf : IsLocalRiemannianIsometry I J f)
{V : (y : N) → TangentSpace J y}
(hV : ContMDiff J J.tangent ↑⊤ fun (y : N) => ⟨y, V y⟩)
:
ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, VectorField.mpullback I J f V x⟩
Pulling back a smooth vector field along a local Riemannian isometry gives a smooth vector field.
theorem
TauCeti.IsLocalRiemannianIsometry.exists_contMDiff_mpullback_apply_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]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
{f : M → N}
[FiniteDimensional ℝ F]
[IsManifold J (↑⊤) N]
[T2Space N]
(hf : IsLocalRiemannianIsometry I J f)
{x : M}
(u : TangentSpace I x)
:
∃ (X : (y : N) → TangentSpace J y),
(ContMDiff J J.tangent ↑⊤ fun (y : N) => ⟨y, X y⟩) ∧ VectorField.mpullback I J f X x = u ∧ X (f x) = (mfderiv% f x) u
Every tangent vector u at x is the value at x of the pullback of a smooth vector field
on N, namely of any smooth field taking the value df_x u at f x.
theorem
TauCeti.IsLocalRiemannianIsometry.id
{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]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
:
The identity map is a local Riemannian isometry.
theorem
TauCeti.IsLocalRiemannianIsometry.comp
{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]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
{f : M → N}
{G : Type u_7}
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{H'' : Type u_8}
[TopologicalSpace H'']
{K : ModelWithCorners ℝ G H''}
{P : Type u_9}
[TopologicalSpace P]
[ChartedSpace H'' P]
[Bundle.RiemannianBundle fun (z : P) => TangentSpace K z]
{g : N → P}
(hg : IsLocalRiemannianIsometry J K g)
(hf : IsLocalRiemannianIsometry I J f)
:
IsLocalRiemannianIsometry I K (g ∘ f)
The composite of two local Riemannian isometries is a local Riemannian isometry.
@[simp]
theorem
TauCeti.RiemannianIsometry.isLocalRiemannianIsometry
{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]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
(Φ : RiemannianIsometry I J M N)
:
IsLocalRiemannianIsometry I J ⇑Φ
A smooth Riemannian isometry is a local Riemannian isometry.