The topology of the intrinsic normal bundle

Give the total space of intrinsic normal classes the quotient topology from the ambient tangent bundle pulled back along the embedding. This construction uses no metric or complement, and applies to embeddings in arbitrary ambient manifolds. Its projection and zero section are continuous.

A commuting square with differentiable base map and C¹ ambient map induces a continuous map of these total spaces: the ambient tangent map descends through the quotient. This is the topological compatibility needed to express normal-bundle coordinates in different ambient manifold charts.

Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, the normal-bundle construction preceding Theorem 6.24. The fibre maps are the existing SmoothEmbedding.normalMap.

noncomputable def TauCeti.SmoothEmbedding.normalQuotientMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} {K : Type u_8} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (p : Bundle.TotalSpace F (⇑f *ᵖ (TangentSpace J))) : Bundle.TotalSpace K fun (x : M) => f.NormalSpace x hn

Take normal classes in the pulled-back ambient tangent bundle. The model parameter K of the target total space does not affect the quotient construction.

@[simp]

theorem TauCeti.SmoothEmbedding.normalQuotientMap_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} {K : Type u_8} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (p : Bundle.TotalSpace F (⇑f *ᵖ (TangentSpace J))) : f.normalQuotientMap hn p = ⟨p.proj, (f.normalClass p.proj hn) p.snd⟩

The quotient map preserves the base and takes the fibrewise normal class.

theorem TauCeti.SmoothEmbedding.normalQuotientMap_surjective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} {K : Type u_8} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) : Function.Surjective (f.normalQuotientMap hn)

Every point of the intrinsic normal total space has an ambient tangent representative.

@[instance_reducible]

noncomputable instance TauCeti.SmoothEmbedding.instTopologicalSpaceNormalBundle {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} {K : Type u_8} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) : TopologicalSpace (Bundle.TotalSpace K fun (x : M) => f.NormalSpace x hn)

The intrinsic normal total space has the quotient topology from the pulled-back ambient tangent bundle.

theorem TauCeti.SmoothEmbedding.isQuotientMap_normalQuotientMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} {K : Type u_8} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) : Topology.IsQuotientMap (f.normalQuotientMap hn)

Ambient tangent representatives give a quotient map onto the intrinsic normal bundle.

theorem TauCeti.SmoothEmbedding.continuous_normalBundle_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} {K : Type u_8} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) {X : Type u_9} [TopologicalSpace X] {q : (Bundle.TotalSpace K fun (x : M) => f.NormalSpace x hn) → X} : Continuous q ↔ Continuous (q ∘ f.normalQuotientMap hn)

A map out of the normal bundle is continuous exactly when its expression on ambient tangent representatives is continuous.

theorem TauCeti.SmoothEmbedding.continuous_normalBundle_proj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} {K : Type u_8} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) : Continuous Bundle.TotalSpace.proj

The intrinsic normal-bundle projection is continuous.

theorem TauCeti.SmoothEmbedding.continuous_normalBundle_zeroSection {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} {K : Type u_8} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) : Continuous (Bundle.zeroSection K fun (x : M) => f.NormalSpace x hn)

The zero section of the intrinsic normal bundle is continuous.

@[simp]

theorem TauCeti.SmoothEmbedding.normalBundleMap_normalQuotientMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} {K : Type u_8} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {E' : Type u_9} {F' : Type u_10} {H' : Type u_11} {G' : Type u_12} {M' : Type u_13} {N' : Type u_14} {K' : Type u_15} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [TopologicalSpace H'] [TopologicalSpace G'] {I' : ModelWithCorners 𝕜 E' H'} {J' : ModelWithCorners 𝕜 F' G'} [TopologicalSpace M'] [ChartedSpace H' M'] [TopologicalSpace N'] [ChartedSpace G' N'] {m : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (g : SmoothEmbedding I' J' m M' N') (hn : n ≠ 0) (hm : m ≠ 0) {u : M → M'} {v : N → N'} (hu : MDiff u) (hv : MDiff v) (h : v ∘ ⇑f = ⇑g ∘ u) (p : Bundle.TotalSpace F (⇑f *ᵖ (TangentSpace J))) : f.normalBundleMap g hn hm hu hv h (f.normalQuotientMap hn p) = g.normalQuotientMap hm ⟨u p.proj, (tangentSpaceCast J' (v (f p.proj)) (g (u p.proj))) ((mfderiv% v (f p.proj)) p.snd)⟩

On an ambient tangent representative, the induced normal-bundle map takes the normal class of the ambient differential of the representative.

theorem TauCeti.SmoothEmbedding.continuous_normalBundleMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {H : Type u_4} {G : Type u_5} {M : Type u_6} {N : Type u_7} {K : Type u_8} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} {E' : Type u_9} {F' : Type u_10} {H' : Type u_11} {G' : Type u_12} {M' : Type u_13} {N' : Type u_14} {K' : Type u_15} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [TopologicalSpace H'] [TopologicalSpace G'] {I' : ModelWithCorners 𝕜 E' H'} {J' : ModelWithCorners 𝕜 F' G'} [TopologicalSpace M'] [ChartedSpace H' M'] [TopologicalSpace N'] [ChartedSpace G' N'] {m : WithTop ℕ∞} [IsManifold J' 1 N'] (f : SmoothEmbedding I J n M N) (g : SmoothEmbedding I' J' m M' N') (hn : n ≠ 0) (hm : m ≠ 0) {u : M → M'} {v : N → N'} (hu : MDiff u) (hv : ContMDiff J J' 1 v) (h : v ∘ ⇑f = ⇑g ∘ u) : Continuous (f.normalBundleMap g hn hm hu ⋯ h)

A commuting square with differentiable base map and C¹ ambient map induces a continuous map of intrinsic normal bundles.