Smooth transitions of intrinsic normal coordinates

Fixed complementary coordinates for the normal spaces of an embedding have smooth transition operators on their overlaps. When the product of the source and complementary model spaces is complete, the transitions of a C^n embedding are C^m when m + 1 ≤ n, including smooth and analytic orders. The source and ambient manifolds may have corners.

The transition takes a complementary representative in the old ambient tangent chart, changes ambient tangent coordinates, and projects onto the new complement. We identify the transitions of the actual local normal-bundle trivializations with this operator formula. Thus smooth normal bundle constructions can use the quotient topology and the existing complementary charts without assuming regularity of their transitions.

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

theorem TauCeti.SmoothEmbedding.normalSpaceTrivializationOfComplement_coordChangeL {𝕜 : 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 H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [IsManifold I 1 M] [IsManifold J 1 N] [TopologicalSpace P] [AddCommGroup P] [Module 𝕜 P] (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) (x₀ x₁ : M) (U V : Set M) (hUopen : IsOpen U) (hVopen : IsOpen V) (hU : U ⊆ (chartAt H x₀).source ∩ ⇑f ⁻¹' (chartAt G (f x₀)).source) (hV : V ⊆ (chartAt H x₁).source ∩ ⇑f ⁻¹' (chartAt G (f x₁)).source) (B C : P →L[𝕜] F) (hB : ∀ x ∈ U, ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x).coprod B).IsInvertible) (hC : ∀ x ∈ V, ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₁ x).coprod C).IsInvertible) (hcoordB : Continuous fun (p : ↑U × F) => ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ ↑p.1).quotientRangeCoordinate B) p.2) (hcoordC : Continuous fun (p : ↑V × F) => ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₁ ↑p.1).quotientRangeCoordinate C) p.2) {x : M} (hx : x ∈ U ∩ V) : ↑(Bundle.Trivialization.coordChangeL 𝕜 (f.normalSpaceTrivializationOfComplement hn x₀ U hUopen hU B hB hcoordB) (f.normalSpaceTrivializationOfComplement hn x₁ V hVopen hV C hC hcoordC) x) = (inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₁ x).quotientRangeCoordinate C ∘SL ↑(Bundle.Trivialization.coordChangeL 𝕜 (trivializationAt F (TangentSpace J) (f x₀)) (trivializationAt F (TangentSpace J) (f x₁)) (f x)) ∘SL B

The transition of the actual quotient-topology normal trivializations is the complementary normal transition operator. The complementary model need only be a topological module; no global normal-bundle atlas is required.

theorem TauCeti.SmoothEmbedding.contMDiffOn_normalSpaceTrivializationOfComplement_coordChangeL {𝕜 : 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 H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [NormedAddCommGroup P] [NormedSpace 𝕜 P] [CompleteSpace (E × P)] (f : SmoothEmbedding I J n M N) (x₀ x₁ : M) (U V : Set M) (hUopen : IsOpen U) (hVopen : IsOpen V) (hU : U ⊆ (chartAt H x₀).source ∩ ⇑f ⁻¹' (chartAt G (f x₀)).source) (hV : V ⊆ (chartAt H x₁).source ∩ ⇑f ⁻¹' (chartAt G (f x₁)).source) (B C : P →L[𝕜] F) {m : WithTop ℕ∞} [IsManifold I (m + 1) M] [IsManifold J (m + 1) N] (hm : m + 1 ≤ n) : have hn := ⋯; ∀ (hB : ∀ x ∈ U, ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x).coprod B).IsInvertible) (hC : ∀ x ∈ V, ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₁ x).coprod C).IsInvertible) (hcoordB : Continuous fun (p : ↑U × F) => ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ ↑p.1).quotientRangeCoordinate B) p.2) (hcoordC : Continuous fun (p : ↑V × F) => ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₁ ↑p.1).quotientRangeCoordinate C) p.2), ContMDiffOn I (modelWithCornersSelf 𝕜 (P →L[𝕜] P)) m (fun (x : M) => ↑(Bundle.Trivialization.coordChangeL 𝕜 (f.normalSpaceTrivializationOfComplement hn x₀ U hUopen hU B hB hcoordB) (f.normalSpaceTrivializationOfComplement hn x₁ V hVopen hV C hC hcoordC) x)) (U ∩ V)

The complementary normal trivializations have C^m transition operators on their base-set overlaps for a C^n embedding with m + 1 ≤ n, provided the product of the source and complementary model spaces is complete. This supplies the transition regularity needed to assemble the intrinsic normal spaces as a smooth vector bundle.