Assembling smooth tubular inverses

If normal addition is a local diffeomorphism along the zero section of a Euclidean normal bundle, it identifies a sufficiently small variable-radius tube smoothly with an open neighbourhood of the embedded image. Radial compression then identifies the entire normal bundle with that neighbourhood. Both directions are smooth, and the neighbourhood can be chosen inside any prescribed open neighbourhood of the image.

These are global assembly theorems: local invertibility of normal addition at zero vectors is an explicit input, not a conclusion. They provide smooth normal coordinates on arbitrarily small ambient neighbourhoods, either from a variable-radius tube or from the whole normal bundle.

The source must be nonempty because a PartialDiffeomorph has an inverse defined everywhere, including outside its target. No compactness or properness of the embedding is needed.

Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 6.24.

theorem TauCeti.exists_partialDiffeomorph_normalBundle_add_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] [Nonempty M] {f : M → V} (hf : ContMDiff I (modelWithCornersSelf ℝ V) 2 f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (hind : Topology.IsInducing f) (hdim : Module.finrank ℝ F = Module.finrank ℝ V - Module.finrank ℝ E) (hlocal : ∀ (x : M), IsLocalDiffeomorphAt (I.prod (modelWithCornersSelf ℝ F)) (modelWithCornersSelf ℝ V) (↑⊤) (fun (p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)) => f p.proj + ↑p.snd) (Bundle.zeroSection F (fun (x : M) => ↥(normalSubspace I f x)) x)) {O : Set V} (hO : IsOpen O) (hfO : Set.range f ⊆ O) : ∃ (r : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤), (∀ (x : M), 0 < r x) ∧ ∃ (Φ : PartialDiffeomorph (I.prod (modelWithCornersSelf ℝ F)) (modelWithCornersSelf ℝ V) (Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)) V ↑⊤), Φ.source = {p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x) | ‖↑p.snd‖ < r p.proj} ∧ Φ.target ⊆ O ∧ ∀ (p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)), ↑Φ.toPartialEquiv p = f p.proj + ↑p.snd

Local invertibility of normal addition along the zero section upgrades a sufficiently small smooth tubular radius to a partial diffeomorphism. Its source is exactly the open normal ball bundle and its target lies in the prescribed ambient neighbourhood.

theorem TauCeti.exists_partialDiffeomorph_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] [Nonempty 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) (hlocal : ∀ (x : M), IsLocalDiffeomorphAt (I.prod (modelWithCornersSelf ℝ F)) (modelWithCornersSelf ℝ V) (↑⊤) (fun (p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)) => f p.proj + ↑p.snd) (Bundle.zeroSection F (fun (x : M) => ↥(normalSubspace I f x)) x)) {O : Set V} (hO : IsOpen O) (hfO : Set.range f ⊆ O) : ∃ (r : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤), (∀ (x : M), 0 < r x) ∧ ∃ (Φ : PartialDiffeomorph (I.prod (modelWithCornersSelf ℝ F)) (modelWithCornersSelf ℝ V) (Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)) V ↑⊤), Φ.source = Set.univ ∧ Φ.target ⊆ O ∧ (∀ (p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)), ↑Φ.toPartialEquiv p = f p.proj + r p.proj • ↑OpenPartialHomeomorph.univUnitBall ↑p.snd) ∧ ∀ (x : M), ↑Φ.toPartialEquiv (Bundle.zeroSection F (fun (x : M) => ↥(normalSubspace I f x)) x) = f x

Radial compression and local invertibility along the zero section give a smooth identification of the whole normal bundle with an open ambient neighbourhood. The map has the explicit compressed-normal-vector formula and fixes the embedded core.