Tubular neighbourhoods parametrized by the whole normal bundle

For a compact embedded submanifold of a Euclidean space, the whole normal bundle is homeomorphic to an open neighbourhood of the submanifold, inside any prescribed open neighbourhood. The normal vectors need not be globally bounded: each fibre is compressed radially into a ball before applying the normal map. The compression fixes the zero section and preserves the base point.

normalBundleHomeomorphTube supplies the fibrewise reparametrization, with the subspace topology on the normal bundle inherited from M × V. The existence theorem exists_isOpenEmbedding_normalBundle_subset combines it with the bounded-radius tubular neighbourhood theorem. This is the topological whole-bundle form; it does not assert a smooth vector-bundle structure or smoothness of the resulting embedding.

The radial compression reuses Mathlib's Homeomorph.unitBall, by Yury Kudryashov and Oliver Nash. No trivialization or framing of the normal bundle is chosen.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Theorem 6.24.
• M. W. Hirsch, Differential Topology, Chapter 4, Theorem 6.3.

noncomputable def TauCeti.normalBundleHomeomorphTube {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (f : M → V) {ε : ℝ} (hε : 0 < ε) : (Bundle.TotalSpace V fun (x : M) => ↥(normalSubspace I f x)) ≃ₜ ↑(normalTube I f ε)

Radially compressing each normal fibre identifies the whole normal bundle with its open tube of radius ε. It preserves the base point and fixes the zero section.

@[simp]

theorem TauCeti.normalBundleHomeomorphTube_apply_fst {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (f : M → V) {ε : ℝ} (hε : 0 < ε) (p : Bundle.TotalSpace V fun (x : M) => ↥(normalSubspace I f x)) : (↑((normalBundleHomeomorphTube f hε) p)).1 = p.proj

The radial compression leaves the base point unchanged.

@[simp]

theorem TauCeti.normalBundleHomeomorphTube_symm_apply_proj {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (f : M → V) {ε : ℝ} (hε : 0 < ε) (q : ↑(normalTube I f ε)) : ((normalBundleHomeomorphTube f hε).symm q).proj = (↑q).1

The inverse radial compression also leaves the base point unchanged.

@[simp]

theorem TauCeti.normalBundleHomeomorphTube_apply_snd {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (f : M → V) {ε : ℝ} (hε : 0 < ε) (p : Bundle.TotalSpace V fun (x : M) => ↥(normalSubspace I f x)) : (↑((normalBundleHomeomorphTube f hε) p)).2 = ε • (√(1 + ‖↑p.snd‖ ^ 2))⁻¹ • ↑p.snd

The fibre coordinate of radial compression, read in the ambient Euclidean space.

@[simp]

theorem TauCeti.normalBundleHomeomorphTube_symm_apply_snd {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (f : M → V) {ε : ℝ} (hε : 0 < ε) (q : ↑(normalTube I f ε)) : ↑((normalBundleHomeomorphTube f hε).symm q).snd = (√(1 - ‖ε⁻¹ • (↑q).2‖ ^ 2))⁻¹ • ε⁻¹ • (↑q).2

The fibre coordinate of inverse radial compression, read in the ambient Euclidean space.

@[simp]

theorem TauCeti.normalBundleHomeomorphTube_zeroSection {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (f : M → V) {ε : ℝ} (hε : 0 < ε) (x : M) : (normalBundleHomeomorphTube f hε) (Bundle.zeroSection V (fun (x : M) => ↥(normalSubspace I f x)) x) = ⟨(x, 0), ⋯⟩

The zero section is carried to the zero vectors of the bounded normal tube.

theorem TauCeti.exists_isOpenEmbedding_normalBundle_subset {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ V] [I.Boundaryless] [IsManifold I 2 M] [CompactSpace M] {f : M → V} (hf : ContMDiff I (modelWithCornersSelf ℝ V) 2 f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (hinj : Function.Injective f) {O : Set V} (hO : IsOpen O) (hfO : Set.range f ⊆ O) : ∃ (Φ : (Bundle.TotalSpace V fun (x : M) => ↥(normalSubspace I f x)) → V), Topology.IsOpenEmbedding Φ ∧ (∀ (x : M), Φ (Bundle.zeroSection V (fun (x : M) => ↥(normalSubspace I f x)) x) = f x) ∧ Set.range Φ ⊆ O

The whole normal bundle form of the tubular neighbourhood theorem. A compact C² embedded submanifold of a Euclidean space has an open tubular embedding of its entire normal bundle inside any given open neighbourhood of its image. The embedding fixes the core.

theorem TauCeti.exists_isTubularNeighborhood_wholeNormalBundle_subset {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ V] [I.Boundaryless] [IsManifold I 2 M] [CompactSpace M] {f : M → V} (hf : ContMDiff I (modelWithCornersSelf ℝ V) 2 f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (hinj : Function.Injective f) {O : Set V} (hO : IsOpen O) (hfO : Set.range f ⊆ O) : ∃ (Φ : (Bundle.TotalSpace V fun (x : M) => ↥(normalSubspace I f x)) → V), IsTubularNeighborhood f Set.univ (Set.univ.domRestrict Φ) ∧ Set.range Φ ⊆ O

The whole-bundle tubular embedding inside a prescribed open neighbourhood, packaged in the IsTubularNeighborhood interface with domain the entire normal bundle.