Smooth tubular neighbourhoods of Euclidean embeddings

The whole normal bundle of a smooth Euclidean embedding is diffeomorphic to an open neighbourhood of its image, with the zero section sent to the original embedding. The neighbourhood may be chosen inside any prescribed open neighbourhood, even for noncompact sources.

The construction combines local invertibility of normal addition with smooth variable-radius compression. These coordinates supply smooth tubular inverses, rather than only regularity of the forward parametrization. For the intrinsic quotient normal bundle in general ambient manifolds, see TauCeti.Geometry.Manifold.TubularNeighborhood.Existence.

References

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

theorem TauCeti.exists_diffeomorph_wholeNormalBundle_subset {V : Type u_1} {E : Type u_2} {F : Type u_3} {H : Type u_4} {M : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {f : M → V} (hf : ContMDiff I (modelWithCornersSelf ℝ V) (↑⊤) f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (hind : Topology.IsInducing f) (hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E) {O : Set V} (hO : IsOpen O) (hfO : Set.range f ⊆ O) : ∃ (W : TopologicalSpace.Opens V), ↑W ⊆ O ∧ ∃ (Φ : Diffeomorph (I.prod (modelWithCornersSelf ℝ F)) (modelWithCornersSelf ℝ V) (Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)) ↥W ↑⊤), ∀ (x : M), ↑(Φ (Bundle.zeroSection F (fun (x : M) => ↥(normalSubspace I f x)) x)) = f x

Smooth Euclidean tubular neighbourhood theorem. The whole orthogonal normal bundle of a smooth immersion inducing the source topology is diffeomorphic to an open neighbourhood of its image, inside any prescribed open neighbourhood. The identification fixes the core. Neither compactness nor closedness of the image is required.