Changes of complementary normal coordinates

In tangent charts, the normal fibre of an immersion is the quotient of the ambient model by the range of its coordinate differential. A complementary parametrization identifies that quotient with a fixed vector space. Changing the ambient chart and the complement gives the operator obtained by inserting the ambient tangent transition between the complementary representative and the new quotient-coordinate operator.

These transitions are invertible on chart overlaps and inherit the differentiability of the differential, losing one derivative from the original map. Together with ContinuousLinearMap.quotientRangeCoordinate_comp_cocycle, these are the compatibility conditions for assembling the smooth normal-bundle atlas. They require neither a metric nor finite-dimensionality; all choices of charts and complementary parametrizations are explicit.

Reuse Mathlib's smooth tangent-bundle transitions, the fixed-chart differential regularity theorem, and ContinuousLinearMap.quotientRangeCoordinate. References: M. Hirsch, Differential Topology, Chapter 4, §5 (normal bundles); J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 6.24 (tubular neighbourhoods).

theorem TauCeti.isInvertible_normalQuotientCoordinateChange {𝕜 : 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] [TopologicalSpace N] [ChartedSpace G N] {Q : Type u_8} {Q' : Type u_9} [TopologicalSpace Q] [AddCommGroup Q] [Module 𝕜 Q] [TopologicalSpace Q'] [AddCommGroup Q'] [Module 𝕜 Q'] [IsManifold I 1 M] [IsManifold J 1 N] (f : M → N) (x₀ x₁ x : M) (B : Q →L[𝕜] F) (B' : Q' →L[𝕜] F) (hx₀ : x ∈ (chartAt H x₀).source) (hx₁ : x ∈ (chartAt H x₁).source) (hy₀ : f x ∈ (chartAt G (f x₀)).source) (hy₁ : f x ∈ (chartAt G (f x₁)).source) (hB : ((inTangentCoordinates I J id f (mfderiv% f) x₀ x).coprod B).IsInvertible) (hB' : ((inTangentCoordinates I J id f (mfderiv% f) x₁ x).coprod B').IsInvertible) : ((inTangentCoordinates I J id f (mfderiv% f) x₁ x).quotientRangeCoordinate B' ∘SL ↑(Bundle.Trivialization.coordChangeL 𝕜 (trivializationAt F (TangentSpace J) (f x₀)) (trivializationAt F (TangentSpace J) (f x₁)) (f x)) ∘SL B).IsInvertible

Valid complementary coordinates for the differential are related by an invertible operator when both source and target tangent charts contain the evaluation points. The complementary parameter spaces need only be topological modules.

theorem ContMDiffOn.normalQuotientCoordinateChange {𝕜 : 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] [TopologicalSpace N] [ChartedSpace G N] {Q : Type u_8} {Q' : Type u_9} [NormedAddCommGroup Q] [NormedSpace 𝕜 Q] [NormedAddCommGroup Q'] [NormedSpace 𝕜 Q'] {m n : WithTop ℕ∞} [IsManifold I (m + 1) M] [IsManifold J (m + 1) N] {f : M → N} {s : Set M} [CompleteSpace (E × Q')] (hf : ContMDiffOn I J n f s) (hmn : m + 1 ≤ n) (hs : IsOpen s) (x₀ x₁ : M) (B : Q →L[𝕜] F) (B' : Q' →L[𝕜] F) (hx₁ : ∀ x ∈ s, x ∈ (chartAt H x₁).source) (hy₀ : ∀ x ∈ s, f x ∈ (chartAt G (f x₀)).source) (hy₁ : ∀ x ∈ s, f x ∈ (chartAt G (f x₁)).source) (hB' : ∀ x ∈ s, ((inTangentCoordinates I J id f (mfderiv% f) x₁ x).coprod B').IsInvertible) : ContMDiffOn I (modelWithCornersSelf 𝕜 (Q →L[𝕜] Q')) m (fun (x : M) => (inTangentCoordinates I J id f (mfderiv% f) x₁ x).quotientRangeCoordinate B' ∘SL ↑(Bundle.Trivialization.coordChangeL 𝕜 (trivializationAt F (TangentSpace J) (f x₀)) (trivializationAt F (TangentSpace J) (f x₁)) (f x)) ∘SL B) s

Changes between fixed complementary normal coordinates are C^m on an open overlap for a C^n map with m + 1 ≤ n. Smooth and analytic orders are included. Only the new complement must be valid to establish regularity of the operator formula.