Smooth normal-exponential coordinates

The normal exponential of an embedding into a Riemannian manifold is a local diffeomorphism at every zero normal vector. These local inverses assemble to a single smooth inverse on an open neighbourhood of the entire zero section. The ambient neighbourhood can be kept inside any prescribed open neighbourhood of the embedded image. Neither compactness nor closedness of the image nor a global normal framing is required.

Smooth radial compression also identifies the whole intrinsic normal bundle with an open ambient neighbourhood, fixing its zero section. An auxiliary smooth fibre metric is chosen only for compression; the normal exponential uses the given ambient Riemannian metric.

The construction uses the previously computed invertible differential of the normal exponential, and IsLocalDiffeomorphOn.exists_partialDiffeomorph_near_section for global injectivity and smoothness of the inverse.

References

• M. W. Hirsch, Differential Topology, Chapter 4, Theorem 6.3.

theorem TauCeti.SmoothEmbedding.isLocalDiffeomorphAt_normalExp_zeroSection {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] [I.Boundaryless] [J.Boundaryless] [T2Space N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y] {n m : WithTop ℕ∞} [ENat.LEInfty m] [IsManifold I (m + 1) M] (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (hm : m + 1 ≤ n) (hm1 : 1 ≤ m) (hdim : Module.finrank ℝ P = Module.finrank ℝ V - Module.finrank ℝ E) (x : M) : IsLocalDiffeomorphAt (I.prod (modelWithCornersSelf ℝ P)) J m (f.normalExp hn) (Bundle.zeroSection P (fun (x : M) => f.NormalSpace x hn) x)

The normal exponential is a C^m local diffeomorphism at every zero normal vector, for a C^n embedding with 1 ≤ m and m + 1 ≤ n.

theorem TauCeti.SmoothEmbedding.exists_partialDiffeomorph_normalExp_subset {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] [I.Boundaryless] [J.Boundaryless] [T2Space N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y] {n m : WithTop ℕ∞} [ENat.LEInfty m] [IsManifold I (m + 1) M] [SecondCountableTopology N] [Nonempty M] (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (hm : m + 1 ≤ n) (hm1 : 1 ≤ m) (hdim : Module.finrank ℝ P = Module.finrank ℝ V - Module.finrank ℝ E) {O : Set N} (hO : IsOpen O) (hfO : Set.range ⇑f ⊆ O) : ∃ (Φ : PartialDiffeomorph (I.prod (modelWithCornersSelf ℝ P)) J (Bundle.TotalSpace P fun (x : M) => f.NormalSpace x hn) N m), (∀ (x : M), Bundle.zeroSection P (fun (x : M) => f.NormalSpace x hn) x ∈ Φ.source) ∧ Φ.source ⊆ f.normalExpDomain hn ∧ Φ.target ⊆ O ∧ Φ.target = f.normalExp hn '' Φ.source ∧ ↑Φ.toPartialEquiv = f.normalExp hn

Normal exponential coordinates around an entire embedded submanifold have a single C^m inverse. Their source lies in the natural exponential domain, contains the whole zero section, and their target lies inside the prescribed open neighbourhood of the image. Nonemptiness is used only for values of the partial inverse outside its target.

theorem TauCeti.SmoothEmbedding.exists_diffeomorph_normalBundle_riemannian_subset {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] [I.Boundaryless] [J.Boundaryless] [T2Space N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsContMDiffRiemannianBundle J (↑⊤) V fun (y : N) => TangentSpace J y] [IsManifold I (↑⊤) M] [SecondCountableTopology N] (f : SmoothEmbedding I J (↑⊤) M N) (hdim : Module.finrank ℝ P = Module.finrank ℝ V - Module.finrank ℝ E) {O : Set N} (hO : IsOpen O) (hfO : Set.range ⇑f ⊆ O) : have hn := exists_diffeomorph_normalBundle_riemannian_subset._proof_1; ∃ (W : TopologicalSpace.Opens N), ↑W ⊆ O ∧ ∃ (Φ : Diffeomorph (I.prod (modelWithCornersSelf ℝ P)) J (Bundle.TotalSpace P fun (x : M) => f.NormalSpace x hn) ↥W ↑⊤), ∀ (x : M), ↑(Φ (Bundle.zeroSection P (fun (x : M) => f.NormalSpace x hn) x)) = f x

Smooth Riemannian tubular neighbourhood theorem. The entire intrinsic normal bundle of a smooth embedding is diffeomorphic to an open neighbourhood inside any prescribed open neighbourhood of its image. The zero section is sent to the original embedding. Neither compactness nor closedness of the embedded image nor completeness of the ambient metric is required.