Tubular neighbourhoods in a Euclidean space

Let f : M → V be a C² embedding of a compact boundaryless manifold into a finite-dimensional real inner product space. Its normal space at x is the orthogonal complement of the range of the differential of f at x, and its normal vectors of length less than ε form the set TauCeti.normalTube I f ε ⊆ M × V. This file proves the tubular neighbourhood theorem in this setting: for some ε > 0 the map (x, v) ↦ f x + v is an open embedding of that normal tube into V. Its image is therefore an open neighbourhood of f '' M which the normal tube identifies with a neighbourhood of the zero section of the normal bundle. Packaged with the subspace topology on the total space of the normal bundle, this is the data TauCeti.IsTubularNeighborhood asks for. Only compact M is treated, with a constant radius; for noncompact submanifolds the radius has to be a positive continuous function on M.

Main definitions

• TauCeti.normalSubspace I f x: the orthogonal complement in V of the range of the differential of f at x.
• TauCeti.normalTube I f ε: the normal vectors of length less than ε, as a subset of M × V.
• TauCeti.normalTubeOfRadius I f r: the normal vectors shorter than a radius r depending on their base point.

Main results

• TauCeti.exists_isOpenEmbedding_normalTube: the tubular neighbourhood theorem for a compact C² embedded submanifold of a Euclidean space.
• TauCeti.exists_isTubularNeighborhood_normalBundle: the same statement as TauCeti.IsTubularNeighborhood data on the total space of the normal bundle.

References

The proof follows Lee's.

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer (2013), Theorem 6.24.
• M. W. Hirsch, Differential Topology, Graduate Texts in Mathematics 33, Springer (1976), Chapter 4, Theorem 6.3.

noncomputable def TauCeti.normalSubspace {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) (x : M) : Submodule ℝ V

The normal space of a map f : M → V into a real inner product space at x: the orthogonal complement in V of the range of the differential of f at x. It realizes the quotient normal space TauCeti.SmoothEmbedding.NormalSpace as a subspace of V, using the inner product.

instance TauCeti.instCompleteSpaceNormalSubspace {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] [CompleteSpace V] (f : M → V) (x : M) : CompleteSpace ↥(normalSubspace I f x)

A normal space is complete when the ambient inner product space is complete.

theorem TauCeti.finrank_normalSubspace {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ 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} {x : M} (himm : Function.Injective ⇑(mfderiv% f x)) : Module.finrank ℝ ↥(normalSubspace I f x) = Module.finrank ℝ V - Module.finrank ℝ E

At an immersion point, the dimension of the normal space is the codimension.

@[simp]

theorem TauCeti.mem_normalSubspace_iff {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} {x : M} {v : V} : v ∈ normalSubspace I f x ↔ ∀ (u : E), inner ℝ v ((mfderiv% f x) u) = 0

A vector is normal to f at x exactly when it is orthogonal to every value of the differential of f at x.

def TauCeti.normalTube {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) (ε : ℝ) : Set (M × V)

The normal vectors along f : M → V of length less than ε, as a subset of M × V.

@[simp]

theorem TauCeti.mem_normalTube {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} {ε : ℝ} {p : M × V} : p ∈ normalTube I f ε ↔ p.2 ∈ normalSubspace I f p.1 ∧ ‖p.2‖ < ε

def TauCeti.normalTubeOfRadius {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) (r : M → ℝ) : Set (M × V)

The normal vectors along f shorter than a radius depending on their base point.

@[simp]

theorem TauCeti.mem_normalTubeOfRadius {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} {r : M → ℝ} {p : M × V} : p ∈ normalTubeOfRadius I f r ↔ p.2 ∈ normalSubspace I f p.1 ∧ ‖p.2‖ < r p.1

@[simp]

theorem TauCeti.normalTubeOfRadius_const {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) (ε : ℝ) : (normalTubeOfRadius I f fun (x : M) => ε) = normalTube I f ε

A constant radius gives the usual normal tube.

theorem TauCeti.isOpenEmbedding_normalTubeOfRadius_of_le {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} {r R : M → ℝ} (hr : Continuous r) (hrR : ∀ (x : M), r x ≤ R x) (h : Topology.IsOpenEmbedding ((normalTubeOfRadius I f R).domRestrict fun (p : M × V) => f p.1 + p.2)) : Topology.IsOpenEmbedding ((normalTubeOfRadius I f r).domRestrict fun (p : M × V) => f p.1 + p.2)

Shrinking a variable normal tube to a smaller continuous radius preserves the open embedding of normal addition. No regularity of the original radius is needed.

theorem TauCeti.normalSubspace_eq_of_mem_source {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] [IsManifold I 1 M] {f : M → V} {x y : M} (hy : y ∈ (extChartAt I x).source) (hg : DifferentiableAt ℝ (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) y)) : normalSubspace I f y = (↑(fderiv ℝ (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) y))).rangeᗮ

At a point y of the source of a chart, the normal space of f is the orthogonal complement of the range of the derivative of the coordinate expression of f.

theorem TauCeti.exists_injOn_isOpen_image_normalTube {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ 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] [I.Boundaryless] [IsManifold I 2 M] {f : M → V} (hf : ContMDiff I (modelWithCornersSelf ℝ V) 2 f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (x₀ : M) : ∃ (W : Set M), IsOpen W ∧ x₀ ∈ W ∧ ∃ δ > 0, Set.InjOn (fun (p : M × V) => f p.1 + p.2) {p : M × V | p.1 ∈ W ∧ p ∈ normalTube I f δ} ∧ ∀ (O : Set (M × V)), IsOpen O → IsOpen ((fun (p : M × V) => f p.1 + p.2) '' (O ∩ {p : M × V | p.1 ∈ W ∧ p ∈ normalTube I f δ}))

The local tubular neighbourhood theorem on M: around every point there is an open set W and a radius δ such that the normal map is injective, and sends relatively open sets to open sets, on the normal vectors of length less than δ at points of W.

theorem TauCeti.exists_isOpenEmbedding_normalTube {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ 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] [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) : ∃ ε > 0, Topology.IsOpenEmbedding ((normalTube I f ε).domRestrict fun (p : M × V) => f p.1 + p.2)

Tubular neighbourhood theorem for a compact C² embedded submanifold of a Euclidean space: for some ε > 0, the map (x, v) ↦ f x + v is an open embedding of the normal vectors of length less than ε into V.

@[instance_reducible]

instance TauCeti.instTopologicalSpaceTotalSpaceNormalSubspace {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 : Type u_5} (f : M → V) : TopologicalSpace (Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x))

The total space of the normal bundle of f carries the topology of a subspace of M × V, independently of its model-fibre parameter F.

theorem TauCeti.isEmbedding_totalSpace_normalSubspace {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 : Type u_5} (f : M → V) : Topology.IsEmbedding fun (p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)) => (p.proj, ↑p.snd)

The total space of the normal bundle of f is embedded in M × V.

theorem TauCeti.exists_isTubularNeighborhood_normalBundle {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ 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] [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) : ∃ ε > 0, IsTubularNeighborhood f {p : Bundle.TotalSpace V fun (x : M) => ↥(normalSubspace I f x) | ‖↑p.snd‖ < ε} fun (p : ↑{p : Bundle.TotalSpace V fun (x : M) => ↥(normalSubspace I f x) | ‖↑p.snd‖ < ε}) => f (↑p).proj + ↑(↑p).snd

Tubular neighbourhood theorem for a compact C² embedded submanifold of a Euclidean space, as IsTubularNeighborhood data: for some ε > 0, the normal vectors of length less than ε, in the total space of the normal bundle, are mapped by (x, v) ↦ f x + v homeomorphically onto an open subset of V. The model-fibre parameter of Bundle.TotalSpace is taken to be V, which contains every fibre.