Local trivializations of intrinsic normal bundles

The intrinsic normal spaces of a smooth embedding in an arbitrary ambient manifold admit local product coordinates. Fix source and ambient tangent charts at a point and a closed complement to the coordinate differential there. On a sufficiently small open set, projection along the moving tangent range identifies every intrinsic normal fibre with that fixed complement.

This file assembles those fibrewise equivalences into a topological bundle trivialization while retaining the quotient topology on the intrinsic normal total space. Its forward coordinate map is the quotient-range coordinate operator in tangent charts, and its inverse takes the normal class of the fixed complementary representative. The construction is the local topological input for the normal vector bundle and the tubular-neighbourhood theorem in a general ambient manifold.

The construction follows J. M. Lee, Introduction to Smooth Manifolds, second edition, the normal-bundle construction preceding Theorem 6.24. It uses the quotient-total-space coordinates in SmoothEmbedding.normalQuotientMap and the intrinsic fibre coordinates in SmoothEmbedding.normalSpaceEquivOfComplement.

noncomputable def TauCeti.SmoothEmbedding.normalSpaceTrivializationOfComplement {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {P : Type u_4} {H : Type u_5} {G : Type u_6} {M : Type u_7} {N : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace P] [AddCommGroup P] [Module 𝕜 P] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F 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) (x₀ : M) (U : Set M) (hUopen : IsOpen U) (hU : U ⊆ (chartAt H x₀).source ∩ ⇑f ⁻¹' (chartAt G (f x₀)).source) (B : P →L[𝕜] F) (hB : ∀ x ∈ U, ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x).coprod B).IsInvertible) (hcoord : Continuous fun (p : ↑U × F) => ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ ↑p.1).quotientRangeCoordinate B) p.2) : Bundle.Trivialization P Bundle.TotalSpace.proj

Local product coordinates on the intrinsic normal bundle from a fixed complement in tangent coordinates. The total space retains its quotient topology from ambient tangent representatives.

The open set must lie in the source and ambient tangent-chart domains, and B must complement the coordinate differential throughout it. Joint continuity of the quotient coordinates of ambient representatives over the open set is the only regularity input needed for this topological trivialization. For a normed model fibre it follows from continuity of the operator-valued quotient coordinate, via ContinuousOn.clm_apply.

@[simp]

theorem TauCeti.SmoothEmbedding.normalSpaceTrivializationOfComplement_baseSet {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {P : Type u_4} {H : Type u_5} {G : Type u_6} {M : Type u_7} {N : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace P] [AddCommGroup P] [Module 𝕜 P] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F 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) (x₀ : M) (U : Set M) (hUopen : IsOpen U) (hU : U ⊆ (chartAt H x₀).source ∩ ⇑f ⁻¹' (chartAt G (f x₀)).source) (B : P →L[𝕜] F) (hB : ∀ x ∈ U, ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x).coprod B).IsInvertible) (hcoord : Continuous fun (p : ↑U × F) => ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ ↑p.1).quotientRangeCoordinate B) p.2) : (f.normalSpaceTrivializationOfComplement hn x₀ U hUopen hU B hB hcoord).baseSet = U

The base set of complementary normal coordinates is the prescribed open set.

@[simp]

theorem TauCeti.SmoothEmbedding.normalSpaceTrivializationOfComplement_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {P : Type u_4} {H : Type u_5} {G : Type u_6} {M : Type u_7} {N : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace P] [AddCommGroup P] [Module 𝕜 P] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F 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) (x₀ : M) (U : Set M) (hUopen : IsOpen U) (hU : U ⊆ (chartAt H x₀).source ∩ ⇑f ⁻¹' (chartAt G (f x₀)).source) (B : P →L[𝕜] F) (hB : ∀ x ∈ U, ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x).coprod B).IsInvertible) (hcoord : Continuous fun (p : ↑U × F) => ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ ↑p.1).quotientRangeCoordinate B) p.2) (p : Bundle.TotalSpace P fun (x : M) => f.NormalSpace x hn) (hp : p.proj ∈ U) : ↑(f.normalSpaceTrivializationOfComplement hn x₀ U hUopen hU B hB hcoord) p = (p.proj, (f.normalSpaceEquivOfComplement hn ⋯ ⋯ B ⋯) p.snd)

Complementary normal coordinates are the fibre equivalence supplied by the tangent charts.

@[simp]

theorem TauCeti.SmoothEmbedding.normalSpaceTrivializationOfComplement_symm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {P : Type u_4} {H : Type u_5} {G : Type u_6} {M : Type u_7} {N : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace P] [AddCommGroup P] [Module 𝕜 P] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F 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) (x₀ : M) (U : Set M) (hUopen : IsOpen U) (hU : U ⊆ (chartAt H x₀).source ∩ ⇑f ⁻¹' (chartAt G (f x₀)).source) (B : P →L[𝕜] F) (hB : ∀ x ∈ U, ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x).coprod B).IsInvertible) (hcoord : Continuous fun (p : ↑U × F) => ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ ↑p.1).quotientRangeCoordinate B) p.2) (p : M × P) (hp : p.1 ∈ U) : ↑(f.normalSpaceTrivializationOfComplement hn x₀ U hUopen hU B hB hcoord).symm p = ⟨p.1, (f.normalSpaceEquivOfComplement hn ⋯ ⋯ B ⋯).symm p.2⟩

Inverse complementary normal coordinates take the normal class of the corresponding complementary ambient tangent vector.

instance TauCeti.SmoothEmbedding.instIsLinearNormalSpaceTrivializationOfComplement {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {P : Type u_4} {H : Type u_5} {G : Type u_6} {M : Type u_7} {N : Type u_8} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace P] [AddCommGroup P] [Module 𝕜 P] [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F 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) (x₀ : M) (U : Set M) (hUopen : IsOpen U) (hU : U ⊆ (chartAt H x₀).source ∩ ⇑f ⁻¹' (chartAt G (f x₀)).source) (B : P →L[𝕜] F) (hB : ∀ x ∈ U, ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x).coprod B).IsInvertible) (hcoord : Continuous fun (p : ↑U × F) => ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ ↑p.1).quotientRangeCoordinate B) p.2) : Bundle.Trivialization.IsLinear 𝕜 (f.normalSpaceTrivializationOfComplement hn x₀ U hUopen hU B hB hcoord)

Complementary normal coordinates are linear on every fibre over their base set.