Intrinsic normal spaces in tangent coordinates

The intrinsic normal space of an embedding is the quotient of the ambient tangent space by the image of its differential. In tangent-bundle trivializations this becomes the quotient of the ambient model space by the range of inTangentCoordinates of the differential. The identification is a continuous linear equivalence and carries ambient tangent classes to their coordinate classes. Its forward and inverse maps are computed on representatives.

The coordinate differential has a continuous left inverse on the chart overlap. Thus it is a split-injective operator family, to which local fixed-complement constructions can be applied when assembling normal-bundle trivializations. No metric, finite-dimensionality, or choice of a normal complement is needed for these identifications.

The construction uses Mathlib's ContinuousLinearMap.inCoordinates_eq and the quotient transport ContinuousLinearEquiv.quotientEquiv. Reference: M. Hirsch, Differential Topology, Chapter 4, §5 (normal bundles).

theorem TauCeti.SmoothEmbedding.map_tangentRange_inTangentCoordinates {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) {x₀ x : M} (hx : x ∈ (chartAt H x₀).source) (hy : f x ∈ (chartAt G (f x₀)).source) : Submodule.map (↑↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F (TangentSpace J) (f x₀)) (f x) ⋯)) (f.tangentRange x hn) = (↑(inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x)).range

Ambient tangent coordinates send the intrinsic tangent range onto the range of the coordinate differential. The source coordinate change does not affect that range.

noncomputable def TauCeti.SmoothEmbedding.normalSpaceEquivInTangentCoordinates {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) {x₀ x : M} (hx : x ∈ (chartAt H x₀).source) (hy : f x ∈ (chartAt G (f x₀)).source) : f.NormalSpace x hn ≃L[𝕜] F ⧸ (↑(inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x)).range

The intrinsic normal fibre is the quotient of the ambient model by the coordinate differential's range on the overlap of the chosen source and target charts.

@[simp]

theorem TauCeti.SmoothEmbedding.normalSpaceEquivInTangentCoordinates_normalClass {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) {x₀ x : M} (hx : x ∈ (chartAt H x₀).source) (hy : f x ∈ (chartAt G (f x₀)).source) (v : TangentSpace J (f x)) : (f.normalSpaceEquivInTangentCoordinates hn hx hy) ((f.normalClass x hn) v) = Submodule.Quotient.mk (↑(trivializationAt F (TangentSpace J) (f x₀)) ⟨f x, v⟩).2

Normal coordinates send an ambient tangent class to its tangent-chart class.

@[simp]

theorem TauCeti.SmoothEmbedding.normalSpaceEquivInTangentCoordinates_symm_mk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} [TopologicalSpace H] {G : Type u_5} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) {x₀ x : M} (hx : x ∈ (chartAt H x₀).source) (hy : f x ∈ (chartAt G (f x₀)).source) (v : F) : (f.normalSpaceEquivInTangentCoordinates hn hx hy).symm (Submodule.Quotient.mk v) = (f.normalClass x hn) ((trivializationAt F (TangentSpace J) (f x₀)).symm (f x) v)

The inverse normal-coordinate map takes the class of a model vector to the class of the corresponding ambient tangent vector.