Smooth quotient maps to intrinsic normal bundles

For an embedding in an arbitrary finite-dimensional manifold, taking the normal class of an ambient tangent vector is smooth, with one derivative lost from the embedding. The projection also admits smooth local right inverses. Consequently a map out of the normal bundle is smooth exactly when its expression on ambient tangent representatives is smooth.

These results connect the quotient definition of the normal bundle with smooth constructions on ambient tangent vectors, as used in tubular neighbourhoods. No Riemannian metric, compactness, or boundarylessness is needed.

References

• J. M. Lee, Introduction to Smooth Manifolds, second edition, the normal-bundle construction preceding Theorem 6.24.

theorem TauCeti.SmoothEmbedding.contMDiff_normalQuotientMap {𝕜 : Type u_1} {E : Type u_2} {V : Type u_3} {P : Type u_4} {H : Type u_5} {G : Type u_6} {M : Type u_7} {N : Type u_8} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [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} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n m : WithTop ℕ∞} [IsManifold I (m + 1) M] [IsManifold J (m + 1) N] (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (hm : m + 1 ≤ n) (hdim : Module.finrank 𝕜 P = Module.finrank 𝕜 V - Module.finrank 𝕜 E) : ContMDiff (I.prod (modelWithCornersSelf 𝕜 V)) (I.prod (modelWithCornersSelf 𝕜 P)) m (f.normalQuotientMap hn)

Taking the intrinsic normal class of an ambient tangent vector is C^m for a C^n embedding when m + 1 ≤ n. Both bundles carry their usual bundle charts.

theorem TauCeti.SmoothEmbedding.exists_contMDiffOn_normalQuotientMap_rightInverse {𝕜 : Type u_1} {E : Type u_2} {V : Type u_3} {P : Type u_4} {H : Type u_5} {G : Type u_6} {M : Type u_7} {N : Type u_8} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [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} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n m : WithTop ℕ∞} [IsManifold I (m + 1) M] [IsManifold J (m + 1) N] (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (hm : m + 1 ≤ n) (hdim : Module.finrank 𝕜 P = Module.finrank 𝕜 V - Module.finrank 𝕜 E) (p : Bundle.TotalSpace P fun (x : M) => f.NormalSpace x hn) : ∃ (U : Set (Bundle.TotalSpace P fun (x : M) => f.NormalSpace x hn)), IsOpen U ∧ p ∈ U ∧ ∃ (s : (Bundle.TotalSpace P fun (x : M) => f.NormalSpace x hn) → Bundle.TotalSpace V (⇑f *ᵖ (TangentSpace J))), ContMDiffOn (I.prod (modelWithCornersSelf 𝕜 P)) (I.prod (modelWithCornersSelf 𝕜 V)) m s U ∧ Set.EqOn (f.normalQuotientMap hn ∘ s) _root_.id U

Near each intrinsic normal vector there is a C^m choice of ambient tangent representatives. The right-inverse identity holds on a neighbourhood of that normal vector.

theorem TauCeti.SmoothEmbedding.contMDiff_normalBundle_iff {𝕜 : Type u_1} {E : Type u_2} {V : Type u_3} {P : Type u_4} {H : Type u_5} {G : Type u_6} {M : Type u_7} {N : Type u_8} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [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} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n m : WithTop ℕ∞} [IsManifold I (m + 1) M] [IsManifold J (m + 1) N] (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (hm : m + 1 ≤ n) (hdim : Module.finrank 𝕜 P = Module.finrank 𝕜 V - Module.finrank 𝕜 E) {E' : Type u_9} {H' : Type u_10} {X : Type u_11} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} [TopologicalSpace X] [ChartedSpace H' X] (q : (Bundle.TotalSpace P fun (x : M) => f.NormalSpace x hn) → X) : ContMDiff (I.prod (modelWithCornersSelf 𝕜 P)) I' m q ↔ ContMDiff (I.prod (modelWithCornersSelf 𝕜 V)) I' m (q ∘ f.normalQuotientMap hn)

A map out of an intrinsic normal bundle is C^m exactly when it is C^m on ambient tangent representatives. This is the smooth descent property of the normal quotient.