Fixed complementary coordinates for intrinsic normal spaces

Near a point of a smooth embedding, the intrinsic normal fibres can all be identified with one closed subspace of the ambient model. These identifications take tangent-chart coordinates of an ambient representative and then project along the moving tangent range. Their inverse uses the fixed complementary representative in the same tangent chart.

The coordinate operators have one less derivative than the embedding. At a point this includes smooth and analytic regularity; for finite or analytic regularity we also obtain one open neighbourhood on which the operators have that regularity. Smoothness at a point alone does not supply a single neighbourhood for all derivative orders. These are fibre coordinates, independent of any topology or atlas on the total normal bundle, and supply local models for constructing it.

The construction composes normalSpaceEquivInTangentCoordinates with ContinuousLinearMap.quotientRangeEquiv. Local existence uses the fixed-complement theorem ContinuousAt.exists_isInvertible_coprod_subtypeL and Mathlib's regularity of the differential in tangent coordinates.

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

noncomputable def TauCeti.SmoothEmbedding.normalSpaceEquivOfComplement {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} {G : Type u_5} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} {N : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} {P : Type u_8} [TopologicalSpace P] [AddCommGroup P] [Module 𝕜 P] (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) (B : P →L[𝕜] F) (hB : ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x).coprod B).IsInvertible) : f.NormalSpace x hn ≃L[𝕜] P

Intrinsic normal coordinates in a fixed complementary parameter space. The complement is specified by B; invertibility says it complements the coordinate differential's range.

@[simp]

theorem TauCeti.SmoothEmbedding.normalSpaceEquivOfComplement_normalClass {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} {G : Type u_5} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} {N : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} {P : Type u_8} [TopologicalSpace P] [AddCommGroup P] [Module 𝕜 P] (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) (B : P →L[𝕜] F) (hB : ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x).coprod B).IsInvertible) (v : TangentSpace J (f x)) : (f.normalSpaceEquivOfComplement hn hx hy B hB) ((f.normalClass x hn) v) = ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x).quotientRangeCoordinate B) (↑(trivializationAt F (TangentSpace J) (f x₀)) ⟨f x, v⟩).2

On ambient tangent representatives, normal coordinates take the complementary component of tangent-chart coordinates.

@[simp]

theorem TauCeti.SmoothEmbedding.normalSpaceEquivOfComplement_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} {G : Type u_5} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} {N : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} {P : Type u_8} [TopologicalSpace P] [AddCommGroup P] [Module 𝕜 P] (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) (B : P →L[𝕜] F) (hB : ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x).coprod B).IsInvertible) (w : P) : (f.normalSpaceEquivOfComplement hn hx hy B hB).symm w = (f.normalClass x hn) ((trivializationAt F (TangentSpace J) (f x₀)).symm (f x) (B w))

Inverse normal coordinates use the chosen complementary vector in the inverse ambient tangent chart and take its normal class.

theorem TauCeti.SmoothEmbedding.normalSpaceEquivOfComplement_apply_symm_eq_quotientRangeCoordinate_coordChangeL {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} {G : Type u_5} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} {N : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} {P : Type u_8} [TopologicalSpace P] [AddCommGroup P] [Module 𝕜 P] {P' : Type u_9} [TopologicalSpace P'] [AddCommGroup P'] [Module 𝕜 P'] (f : SmoothEmbedding I J n M N) (hn : n ≠ 0) {x₀ x₁ x : M} (hx₀ : x ∈ (chartAt H x₀).source) (hy₀ : f x ∈ (chartAt G (f x₀)).source) (hx₁ : x ∈ (chartAt H x₁).source) (hy₁ : f x ∈ (chartAt G (f x₁)).source) (B : P →L[𝕜] F) (C : P' →L[𝕜] F) (hB : ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x).coprod B).IsInvertible) (hC : ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₁ x).coprod C).IsInvertible) (w : P) : (f.normalSpaceEquivOfComplement hn hx₁ hy₁ C hC) ((f.normalSpaceEquivOfComplement hn hx₀ hy₀ B hB).symm w) = ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₁ x).quotientRangeCoordinate C) ((Bundle.Trivialization.coordChangeL 𝕜 (trivializationAt F (TangentSpace J) (f x₀)) (trivializationAt F (TangentSpace J) (f x₁)) (f x)) (B w))

Changing the complement and the ambient tangent chart gives the normal-coordinate transition by applying the ambient tangent transition to the old complementary representative. Use this rule with rw; expanding a general transition during simplification can obscure the cancellation of a coordinate equivalence with its inverse.

@[simp]

theorem TauCeti.SmoothEmbedding.normalSpaceEquivOfComplement_apply_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} {G : Type u_5} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} {N : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} {P : Type u_8} [TopologicalSpace P] [AddCommGroup P] [Module 𝕜 P] (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) (B : P →L[𝕜] F) (hB : ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x).coprod B).IsInvertible) (w : P) : (f.normalSpaceEquivOfComplement hn hx hy B hB) ((f.normalSpaceEquivOfComplement hn hx hy B hB).symm w) = w

Normal coordinates recover a parameter from its complementary representative.

theorem TauCeti.SmoothEmbedding.contMDiffAt_inTangentCoordinates_quotientRangeCoordinate {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} {G : Type u_5} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} {N : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} [CompleteSpace F] {P : Type u_8} [NormedAddCommGroup P] [NormedSpace 𝕜 P] (f : SmoothEmbedding I J n M N) {m : WithTop ℕ∞} (hm : m + 1 ≤ n) (x₀ : M) (B : P →L[𝕜] F) (hB : ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x₀).coprod B).IsInvertible) : ContMDiffAt I (modelWithCornersSelf 𝕜 (F →L[𝕜] P)) m (fun (x : M) => (inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x).quotientRangeCoordinate B) x₀

For any valid fixed complement, the normal-coordinate operator is C^m at the chart centre when the embedding is C^(m+1) there. This includes smooth and analytic regularity.

theorem TauCeti.SmoothEmbedding.exists_contMDiffOn_inTangentCoordinates_quotientRangeCoordinate {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} {G : Type u_5} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} {N : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [TopologicalSpace N] [ChartedSpace G N] [IsManifold J 1 N] {n : WithTop ℕ∞} [CompleteSpace F] {m : WithTop ℕ∞} [IsManifold I m M] (f : SmoothEmbedding I J n M N) (hm : m + 1 ≤ n) (hm' : m ≠ ↑⊤) (x₀ : M) : ∃ (Q : Submodule 𝕜 F), IsClosed ↑Q ∧ ∃ (U : Set M), IsOpen U ∧ x₀ ∈ U ∧ U ⊆ (chartAt H x₀).source ∩ ⇑f ⁻¹' (chartAt G (f x₀)).source ∧ (∀ x ∈ U, ((inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x).coprod Q.subtypeL).IsInvertible) ∧ ContMDiffOn I (modelWithCornersSelf 𝕜 (F →L[𝕜] ↥Q)) m (fun (x : M) => (inTangentCoordinates I J _root_.id (⇑f) (mfderiv% ⇑f) x₀ x).quotientRangeCoordinate Q.subtypeL) U

A positive-regularity embedding has a fixed closed complementary model for its intrinsic normal fibres near each point. For every finite or analytic order m with m + 1 ≤ n, the complementary coordinate operators are C^m on one open neighbourhood contained in the source and ambient tangent-chart domains. No metric or finite-dimensionality is required.