Tubular neighbourhoods without a prescribed metric

The intrinsic normal bundle of a smooth embedding between finite-dimensional, boundaryless real manifolds is diffeomorphic to an open neighbourhood of its image. The neighbourhood can be chosen inside any prescribed open neighbourhood, and the zero section is sent to the original embedding. The ambient manifold is Hausdorff and second countable; neither compactness nor closedness of the image is required.

An auxiliary smooth Riemannian metric is chosen on the ambient tangent bundle using TauCeti.nonempty_contMDiffRiemannianMetric. The Riemannian tubular theorem SmoothEmbedding.exists_diffeomorph_normalBundle_riemannian_subset then supplies the coordinates. The conclusion uses the intrinsic quotient normal bundle and its existing complementary-coordinate atlas, both independent of that metric.

Projecting the tubular neighbourhood to the base gives a smooth retraction of an open neighbourhood of the image onto the embedded manifold (TauCeti.SmoothEmbedding.exists_contMDiffOn_retraction).

References

• J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 6.24.
• M. Hirsch, Differential Topology, Chapter 4, Theorem 6.3.

theorem TauCeti.SmoothEmbedding.exists_diffeomorph_normalBundle_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} [I.Boundaryless] [J.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J (↑⊤) N] [T2Space N] [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_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 tubular neighbourhood theorem. The entire intrinsic normal bundle of a smooth embedding is diffeomorphic to an arbitrarily small open neighbourhood of its image, with the zero section sent to the embedding. No Riemannian metric is part of the input or output, and the image need not be closed or compact.

theorem TauCeti.SmoothEmbedding.exists_contMDiffOn_retraction {E : Type u_1} {V : Type u_2} {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] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ V G} [I.Boundaryless] [J.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J (↑⊤) N] [T2Space N] [SecondCountableTopology N] [Nonempty M] (f : SmoothEmbedding I J (↑⊤) M N) {O : Set N} (hO : IsOpen O) (hfO : Set.range ⇑f ⊆ O) : ∃ (W : Set N), IsOpen W ∧ Set.range ⇑f ⊆ W ∧ W ⊆ O ∧ ∃ (r : N → M), ContMDiffOn J I (↑⊤) r W ∧ ∀ (x : M), r (f x) = x

Smooth retractions onto embedded submanifolds. A smooth embedding f : M → N of a nonempty boundaryless manifold into a second countable Hausdorff boundaryless manifold has a smooth retraction r : N → M on an open neighbourhood W of its image, inside any prescribed open neighbourhood O of the image: r is smooth on W and r ∘ f = id. Outside W the values of r are arbitrary.