Smoothness of the normal exponential #
The natural domain of the normal exponential is open in the intrinsic normal bundle, and the
normal exponential is smooth there. Both statements concern the total space, so the base point
and normal vector vary together. The domain contains the zero section by
SmoothEmbedding.zeroSection_mem_normalExpDomain.
These are the regularity inputs to the inverse function theorem in the construction of tubular neighbourhoods. They do not assert injectivity or the existence of a tubular diffeomorphism.
References #
- M. W. Hirsch, Differential Topology, Chapter 4, Theorem 6.3.
theorem
TauCeti.SmoothEmbedding.isOpen_normalExpDomain
{E : Type u_1}
{V : Type u_2}
{P : Type u_3}
{H : Type u_4}
{G : Type u_5}
{M : Type u_6}
{N : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[FiniteDimensional ℝ P]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
[IsManifold J (↑⊤) N]
[J.Boundaryless]
[T2Space N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y]
[IsManifold I 1 M]
(f : SmoothEmbedding I J n M N)
(hn : n ≠ 0)
(hdim : Module.finrank ℝ P = Module.finrank ℝ V - Module.finrank ℝ E)
:
IsOpen (f.normalExpDomain hn)
The natural normal-exponential domain is open in the total intrinsic normal bundle.
theorem
TauCeti.SmoothEmbedding.contMDiffOn_normalExp
{E : Type u_1}
{V : Type u_2}
{P : Type u_3}
{H : Type u_4}
{G : Type u_5}
{M : Type u_6}
{N : Type u_7}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[FiniteDimensional ℝ V]
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[FiniteDimensional ℝ P]
[TopologicalSpace H]
[TopologicalSpace G]
{I : ModelWithCorners ℝ E H}
{J : ModelWithCorners ℝ V G}
[TopologicalSpace M]
[ChartedSpace H M]
[TopologicalSpace N]
[ChartedSpace G N]
[IsManifold J (↑⊤) N]
[J.Boundaryless]
[T2Space N]
{n : WithTop ℕ∞}
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y]
{m : WithTop ℕ∞}
[ENat.LEInfty m]
[IsManifold I (m + 1) M]
(f : SmoothEmbedding I J n M N)
(hn : n ≠ 0)
(hm : m + 1 ≤ n)
(hdim : Module.finrank ℝ P = Module.finrank ℝ V - Module.finrank ℝ E)
:
ContMDiffOn (I.prod (modelWithCornersSelf ℝ P)) J m (f.normalExp hn) (f.normalExpDomain hn)
The normal exponential is C^m on its natural open domain in the total normal bundle for a
C^n embedding with m + 1 ≤ n.