Intrinsic normal vector bundles in manifolds

The intrinsic normal spaces of a positive-regularity embedding between finite-dimensional manifolds form a vector bundle. The total space retains its quotient topology from the pulled-back ambient tangent bundle. No metric or boundarylessness assumption is needed.

Local coordinates use a fixed complement to the differential in tangent charts, identified with any chosen model of the codimension. These are the normal bundles needed for tubular neighbourhoods in an arbitrary ambient manifold.

The construction combines normalSpaceEquivOfComplement and normalSpaceTrivializationOfComplement. For the tubular-neighbourhood context, see M. Hirsch, Differential Topology, Chapter 4, §§5–6.

noncomputable def TauCeti.SmoothEmbedding.normalSpaceTrivialization {𝕜 : 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] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (hdim : Module.finrank 𝕜 P = Module.finrank 𝕜 V - Module.finrank 𝕜 E) (x₀ : M) : Bundle.Trivialization P Bundle.TotalSpace.proj

Preferred local coordinates on the intrinsic normal bundle in an arbitrary ambient manifold, using a fixed model of the codimension. The total space has its quotient topology.

@[simp]

theorem TauCeti.SmoothEmbedding.mem_normalSpaceTrivialization_baseSet {𝕜 : 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] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (hdim : Module.finrank 𝕜 P = Module.finrank 𝕜 V - Module.finrank 𝕜 E) (x : M) : x ∈ (f.normalSpaceTrivialization hn hdim x).baseSet

The preferred intrinsic normal coordinates contain their reference point.

theorem TauCeti.SmoothEmbedding.exists_normalSpaceTrivialization_symm_apply {𝕜 : 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] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (hdim : Module.finrank 𝕜 P = Module.finrank 𝕜 V - Module.finrank 𝕜 E) (x₀ : M) : ∃ (B : P →L[𝕜] V), (f.normalSpaceTrivialization hn hdim x₀).baseSet ⊆ (chartAt H x₀).source ∩ ⇑f ⁻¹' (chartAt G (f x₀)).source ∧ ∀ x ∈ (f.normalSpaceTrivialization hn hdim x₀).baseSet, ∀ (w : P), (f.normalSpaceTrivialization hn hdim x₀).symm x w = (f.normalClass x hn) ((trivializationAt V (TangentSpace J) (f x₀)).symm (f x) (B w))

The preferred intrinsic normal coordinates at x₀ invert by one fixed complementary representative: their base set lies in the source and ambient charts at x₀, and over it the normal vector with coordinates w is the normal class of the ambient tangent vector whose coordinates in the tangent chart at f x₀ are B w, for a fixed B : P →L[𝕜] V.

instance TauCeti.SmoothEmbedding.instIsLinearNormalSpaceTrivialization {𝕜 : 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] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (hdim : Module.finrank 𝕜 P = Module.finrank 𝕜 V - Module.finrank 𝕜 E) (x : M) : Bundle.Trivialization.IsLinear 𝕜 (f.normalSpaceTrivialization hn hdim x)

Preferred intrinsic normal coordinates are linear on each fibre.

theorem TauCeti.SmoothEmbedding.continuousOn_normalSpaceTrivialization_coordChangeL {𝕜 : 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] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (hdim : Module.finrank 𝕜 P = Module.finrank 𝕜 V - Module.finrank 𝕜 E) (x₀ x₁ : M) : ContinuousOn (fun (x : M) => ↑(Bundle.Trivialization.coordChangeL 𝕜 (f.normalSpaceTrivialization hn hdim x₀) (f.normalSpaceTrivialization hn hdim x₁) x)) ((f.normalSpaceTrivialization hn hdim x₀).baseSet ∩ (f.normalSpaceTrivialization hn hdim x₁).baseSet)

Transition operators for the preferred intrinsic normal coordinates are continuous.

theorem TauCeti.SmoothEmbedding.contMDiffOn_normalSpaceTrivialization_coordChangeL {𝕜 : 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) (x₀ x₁ : M) : ContMDiffOn I (modelWithCornersSelf 𝕜 (P →L[𝕜] P)) m (fun (x : M) => ↑(Bundle.Trivialization.coordChangeL 𝕜 (f.normalSpaceTrivialization hn hdim x₀) (f.normalSpaceTrivialization hn hdim x₁) x)) ((f.normalSpaceTrivialization hn hdim x₀).baseSet ∩ (f.normalSpaceTrivialization hn hdim x₁).baseSet)

Transition operators for the preferred intrinsic normal coordinates are C^m for a C^n embedding when m + 1 ≤ n.

@[instance_reducible]

noncomputable def TauCeti.SmoothEmbedding.normalSpaceFiberBundle {𝕜 : 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] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (hdim : Module.finrank 𝕜 P = Module.finrank 𝕜 V - Module.finrank 𝕜 E) : FiberBundle P fun (x : M) => f.NormalSpace x hn

The intrinsic normal fibre bundle in an arbitrary finite-dimensional ambient manifold. Install it locally to select the complementary-coordinate atlas. Its topology is the existing quotient topology on intrinsic normal classes.

@[simp]

theorem TauCeti.SmoothEmbedding.normalSpaceFiberBundle_trivializationAt {𝕜 : 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] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (hdim : Module.finrank 𝕜 P = Module.finrank 𝕜 V - Module.finrank 𝕜 E) (x : M) : trivializationAt P (fun (x : M) => f.NormalSpace x hn) x = f.normalSpaceTrivialization hn hdim x

The preferred bundle chart is the chosen complementary normal chart.

@[simp]

theorem TauCeti.SmoothEmbedding.mem_normalSpaceFiberBundle_trivializationAtlas_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] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (hdim : Module.finrank 𝕜 P = Module.finrank 𝕜 V - Module.finrank 𝕜 E) (e : Bundle.Trivialization P Bundle.TotalSpace.proj) : (e ∈ trivializationAtlas P fun (x : M) => f.NormalSpace x hn) ↔ ∃ (x : M), f.normalSpaceTrivialization hn hdim x = e

The intrinsic normal atlas consists exactly of the chosen complementary charts.

theorem TauCeti.SmoothEmbedding.normalSpaceVectorBundle {𝕜 : 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] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (hdim : Module.finrank 𝕜 P = Module.finrank 𝕜 V - Module.finrank 𝕜 E) : VectorBundle 𝕜 P fun (x : M) => f.NormalSpace x hn

The intrinsic normal fibres form a vector bundle with their quotient topology.

theorem TauCeti.SmoothEmbedding.normalSpaceContMDiffVectorBundle {𝕜 : 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) : ContMDiffVectorBundle m P (fun (x : M) => f.NormalSpace x hn) I

The intrinsic normal spaces of a C^n embedding form a C^m vector bundle when m + 1 ≤ n, retaining their quotient total-space topology.