The normal exponential of a smooth embedding #
For a smooth embedding into a finite-dimensional Riemannian manifold, every intrinsic normal class has a unique representative orthogonal to the tangent space of the embedded submanifold. The normal exponential sends that representative through the ambient Riemannian exponential. Its natural domain consists of the classes whose representatives lie in the domain of the ambient exponential map; this domain contains the zero section and is star-convex in each fibre.
This is the local map used to construct tubular neighbourhoods in a general ambient manifold. The tubular-neighbourhood theorem additionally shrinks its domain so that the normal exponential is injective and a diffeomorphism onto an ambient neighbourhood.
References #
- J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 6.24.
- M. W. Hirsch, Differential Topology, Chapter 4, Theorem 6.3.
def
TauCeti.SmoothEmbedding.normalExpDomain
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsManifold J (↑⊤) N]
[IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(hn : n ≠ 0)
:
Set (Bundle.TotalSpace P fun (x : M) => f.NormalSpace x hn)
The natural domain of the normal exponential: the intrinsic normal classes whose orthogonal representatives lie in the domain of the ambient Riemannian exponential.
Instances For
@[simp]
theorem
TauCeti.SmoothEmbedding.mem_normalExpDomain
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsManifold J (↑⊤) N]
[IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(hn : n ≠ 0)
(p : Bundle.TotalSpace P fun (x : M) => f.NormalSpace x hn)
:
p ∈ f.normalExpDomain hn ↔ (f.normalRepresentative p.proj hn) p.snd ∈ Manifold.expDomain J N (f p.proj)
Membership in the natural normal-exponential domain means that the orthogonal representative lies in the natural domain of the ambient exponential at its base point.
theorem
TauCeti.SmoothEmbedding.normalExpDomain_fiber_eq_preimage
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsManifold J (↑⊤) N]
[IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(hn : n ≠ 0)
(x : M)
:
{v : ↥(f.tangentRange x hn)ᗮ | ⟨x, (f.normalClass x hn) ↑v⟩ ∈ f.normalExpDomain hn} = Subtype.val ⁻¹' Manifold.expDomain J N (f x)
On an orthogonal normal fibre, the normal-exponential domain is the preimage of the ambient exponential domain under the inclusion into the tangent space.
theorem
TauCeti.SmoothEmbedding.zeroSection_mem_normalExpDomain
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsManifold J (↑⊤) N]
[IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(hn : n ≠ 0)
(x : M)
:
The zero normal class at every point lies in the natural domain of the normal exponential.
theorem
TauCeti.SmoothEmbedding.starConvex_normalExpDomain_fiber
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsManifold J (↑⊤) N]
[IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(hn : n ≠ 0)
(x : M)
:
StarConvex ℝ 0 {v : f.NormalSpace x hn | ⟨x, v⟩ ∈ f.normalExpDomain hn}
Every fibre slice of the natural normal-exponential domain is star-convex at zero.
noncomputable def
TauCeti.SmoothEmbedding.normalExp
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsManifold J (↑⊤) N]
[IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(hn : n ≠ 0)
(p : Bundle.TotalSpace P fun (x : M) => f.NormalSpace x hn)
:
N
The normal exponential sends an intrinsic normal class to the ambient exponential of its
orthogonal representative. It takes the base point as a junk value outside its natural domain,
following Manifold.riemannianExp.
Instances For
theorem
TauCeti.SmoothEmbedding.normalExp_apply
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsManifold J (↑⊤) N]
[IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(hn : n ≠ 0)
(p : Bundle.TotalSpace P fun (x : M) => f.NormalSpace x hn)
:
The normal exponential is the ambient Riemannian exponential of the orthogonal representative.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalExp_zeroSection
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsManifold J (↑⊤) N]
[J.Boundaryless]
[T2Space N]
[IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(hn : n ≠ 0)
(x : M)
:
The normal exponential sends the zero section to the original embedding.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalExp_of_notMem_normalExpDomain
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsManifold J (↑⊤) N]
[J.Boundaryless]
[IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(hn : n ≠ 0)
{p : Bundle.TotalSpace P fun (x : M) => f.NormalSpace x hn}
(hp : p ∉ f.normalExpDomain hn)
:
Outside its natural domain, the normal exponential takes its base point as a junk value.
@[simp]
theorem
TauCeti.SmoothEmbedding.normalExp_normalClass
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsManifold J (↑⊤) N]
[IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(hn : n ≠ 0)
(x : M)
(v : TangentSpace J (f x))
:
f.normalExp hn ⟨x, (f.normalClass x hn) v⟩ = Manifold.riemannianExp J N (f x) ((f.tangentRange x hn)ᗮ.starProjection v)
On the class of an ambient tangent vector, the normal exponential uses its orthogonal projection to the normal directions.
theorem
TauCeti.SmoothEmbedding.normalExp_normalClass_orthogonal
{E : Type u_1}
{V : Type u_2}
{H : Type u_3}
{G : Type u_4}
{M : Type u_5}
{N : Type u_6}
{P : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsManifold J (↑⊤) N]
[IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y]
(f : SmoothEmbedding I J n M N)
(hn : n ≠ 0)
(x : M)
(v : ↥(f.tangentRange x hn)ᗮ)
:
On an orthogonal normal vector, the normal exponential agrees with the ambient Riemannian exponential without an additional projection.