Extending smooth data from an embedded submanifold

A smooth embedding of a boundaryless manifold admits local smooth retractions. In particular a smooth map which near a point takes values in the image of the embedding factors there through the embedding by a map smooth at that point (Manifold.IsImmersionAt.exists_contMDiffAt_comp_eventuallyEq), which does not need the source to be boundaryless. Consequently, vector-valued smooth data on its source extend to the ambient manifold along any closed portion of its image. The ambient extension can be supported inside a prescribed open neighbourhood, and has compact support when the portion is compact. Neither the full embedded image nor the source needs to be compact or closed.

The same holds for sections of a smooth vector bundle on the ambient manifold given along the embedding, such as tangent vectors at the points of the image. Near an image point, the section is moved to nearby fibres by reading it at the retracted point in a local trivialization. The local extensions are glued by Mathlib's exists_contMDiffSection_forall_mem_convex_of_local, with the convex constraint of agreeing with the given section on the image portion and vanishing off the prescribed neighbourhood. Here the embedding need only be a topological embedding which is an immersion at the points of the portion.

These are the local-coordinate and partition-of-unity steps in extending an isotopy's velocity to an ambient vector field. The local retraction uses Mathlib's immersion normal form, projecting (u, v) to u; gluing uses IsClosed.exists_contMDiffMap_eqOn. The source must be boundaryless because that projection must land in an open source-chart target.

Reference: M. Hirsch, Differential Topology, Chapter 8, §1 (isotopy extension).

theorem Manifold.IsImmersionAt.exists_contMDiffOn_retraction {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E' : Type u_3} {H : Type u_4} {H' : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H] [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace H' N] [I.Boundaryless] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) (hf : Topology.IsEmbedding f) : ∃ (V : Set N), IsOpen V ∧ f x ∈ V ∧ ∃ (r : N → M), ContMDiffOn J I n r V ∧ ∀ (y : M), f y ∈ V → r (f y) = y

A topological embedding with a C^n immersion normal form at x admits a local C^n retraction to its boundaryless source. Its left-inverse law holds for every source point whose image is in the chosen neighbourhood, not just for one source chart. No immersion or smoothness hypothesis is needed away from x.

theorem Manifold.IsImmersionAt.exists_contMDiffAt_comp_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E' : Type u_3} {H : Type u_4} {H' : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H] [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : IsImmersionAt I J n f x) (hf : Topology.IsEmbedding f) {E'' : Type u_8} {H'' : Type u_9} {P : Type u_10} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [TopologicalSpace H''] {K : ModelWithCorners 𝕜 E'' H''} [TopologicalSpace P] [ChartedSpace H'' P] {g : P → N} {p : P} (hg : ContMDiffAt K J n g p) (hgp : g p = f x) (hrange : ∀ᶠ (q : P) in nhds p, g q ∈ Set.range f) : ∃ (τ : P → M), ContMDiffAt K I n τ p ∧ τ p = x ∧ f ∘ τ =ᶠ[nhds p] g

A map g which is C^n at p, with g p = f x, and which near p takes values in the image of a topological embedding f with a C^n immersion normal form at x, factors near p through f by a map which is C^n at p and sends p to x: compose g with a local retraction.

theorem Manifold.IsImmersionAt.exists_contMDiffOn_section_extension {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {E' : Type u_3} {F : Type u_4} {H : Type u_5} {H' : Type u_6} {M : Type u_7} {N : Type u_8} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace H] [TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace H' N] [I.Boundaryless] {n : WithTop ℕ∞} {f : M → N} {x : M} {V : N → Type u_9} [(y : N) → AddCommGroup (V y)] [(y : N) → Module 𝕜 (V y)] [(y : N) → TopologicalSpace (V y)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] [ContMDiffVectorBundle n F V J] (h : IsImmersionAt I J n f x) (hf : Topology.IsEmbedding f) (s : (x : M) → V (f x)) (hs : ContMDiff I (J.prod (modelWithCornersSelf 𝕜 F)) n fun (x : M) => ⟨f x, s x⟩) : ∃ (W : Set N), IsOpen W ∧ f x ∈ W ∧ ∃ (σ : (y : N) → V y), ContMDiffOn J (J.prod (modelWithCornersSelf 𝕜 F)) n (fun (y : N) => ⟨y, σ y⟩) W ∧ ∀ (y : M), f y ∈ W → σ (f y) = s y

Near the image of a point where a topological embedding has a C^n immersion normal form, a C^n section of a vector bundle along the embedding extends to a C^n local section of the bundle on an open neighbourhood, agreeing with it at every source point whose image lies there.

theorem TauCeti.SmoothEmbedding.exists_contMDiffMap_extension {E : Type u_1} {E' : Type u_2} {F : Type u_3} {H : Type u_4} {H' : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ E' H'} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace H' N] [I.Boundaryless] [IsManifold J (↑⊤) N] [T2Space N] [SigmaCompactSpace N] {n : ℕ∞} (f : SmoothEmbedding I J (↑n) M N) (g : ContMDiffMap I (modelWithCornersSelf ℝ F) M F ↑n) {K : Set M} (hK : IsClosed (⇑f '' K)) {U : Set N} (hU : IsOpen U) (hKU : ⇑f '' K ⊆ U) : ∃ (G : ContMDiffMap J (modelWithCornersSelf ℝ F) N F ↑n), Set.EqOn (⇑G ∘ ⇑f) (⇑g) K ∧ tsupport ⇑G ⊆ U

Extend smooth vector-valued data along a closed portion of an embedded boundaryless manifold, with topological support inside a prescribed open set. Closedness is required only of the portion of the image where agreement is requested.

theorem TauCeti.SmoothEmbedding.exists_contMDiffMap_extension_hasCompactSupport {E : Type u_1} {E' : Type u_2} {F : Type u_3} {H : Type u_4} {H' : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ E' H'} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace H' N] [I.Boundaryless] [IsManifold J (↑⊤) N] [T2Space N] [SigmaCompactSpace N] {n : ℕ∞} (f : SmoothEmbedding I J (↑n) M N) (g : ContMDiffMap I (modelWithCornersSelf ℝ F) M F ↑n) {K : Set M} (hK : IsCompact K) {U : Set N} (hU : IsOpen U) (hKU : ⇑f '' K ⊆ U) : ∃ (G : ContMDiffMap J (modelWithCornersSelf ℝ F) N F ↑n), Set.EqOn (⇑G ∘ ⇑f) (⇑g) K ∧ HasCompactSupport ⇑G ∧ tsupport ⇑G ⊆ U

Data on a compact portion of an embedded boundaryless manifold admit a compactly supported smooth ambient extension inside any prescribed open neighbourhood.

theorem Topology.IsEmbedding.exists_contMDiffSection_extension {E : Type u_1} {E' : Type u_2} {F : Type u_3} {H : Type u_4} {H' : Type u_5} {M : Type u_6} {N : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [TopologicalSpace H] [TopologicalSpace H'] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ E' H'} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace H' N] [I.Boundaryless] [IsManifold J (↑⊤) N] [T2Space N] [SigmaCompactSpace N] {n : ℕ∞} {V : N → Type u_8} [(y : N) → AddCommGroup (V y)] [(y : N) → Module ℝ (V y)] [(y : N) → TopologicalSpace (V y)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle (↑n) F V J] {f : M → N} (hf : IsEmbedding f) {K : Set M} (himm : ∀ x ∈ K, Manifold.IsImmersionAt I J (↑n) f x) (hK : IsClosed (f '' K)) {U : Set N} (hU : IsOpen U) (hKU : f '' K ⊆ U) (s : (x : M) → V (f x)) (hs : ContMDiff I (J.prod (modelWithCornersSelf ℝ F)) ↑n fun (x : M) => ⟨f x, s x⟩) : ∃ (σ : ContMDiffSection J F (↑n) V), (∀ x ∈ K, σ (f x) = s x) ∧ ∀ y ∉ U, σ y = 0

A C^n section of a vector bundle along a topological embedding of a boundaryless manifold extends to a global C^n section of the bundle. The extension agrees with the given section on a portion K of the source with closed image, at whose points the embedding is a C^n immersion, and vanishes outside a prescribed open neighbourhood of that image.