The isotopy extension theorem

Let F be a smooth isotopy from f₀ to f₁, a jointly smooth motion of a boundaryless manifold M through smooth embeddings into a finite-dimensional boundaryless manifold N. On every compact subset A of M, the motion is the restriction of a compactly supported diffeotopy of N (TauCeti.SmoothIsotopy.exists_diffeotopy_apply_eq): there is a diffeotopy Φ, fixing every point outside a compact set, with Φ (t, f₀ x) = F (σ t, x) for x ∈ A, where σ is the smooth change of time Real.smoothTransition. In particular its final diffeomorphism carries f₀ to f₁ on A (TauCeti.SmoothIsotopy.exists_diffeotopy_final_apply_eq). This is the isotopy extension theorem of Hirsch, Chapter 8, Theorem 1.3, for compact parts of the source; the source itself need not be compact. The diffeotopy can moreover be chosen to fix a closed set C which the moving part of A never meets (TauCeti.SmoothIsotopy.exists_diffeotopy_apply_eq_of_forall_notMem): the ambient velocity field is cut off by a smooth function equal to 1 on the motion of that part and to 0 on C.

The proof integrates a velocity field. Run at the time σ s, the motion of A is stationary for s ≤ 0 and s ≥ 1, and TauCeti.SmoothIsotopy.exists_ambientVelocityField extends its velocity to a time-dependent vector field X on N vanishing outside a fixed compact set K. Such a field has a complete suspension (TauCeti.isCompleteVectorField_timeDependentSuspensionField), so its time-dependent flow from time 0 is a diffeotopy (TauCeti.timeDependentFlowDiffeotopy), fixing the complement of K. For x ∈ A, the curve s ↦ F (σ s, x) solves the time-dependent equation of X and starts at f₀ x, so by uniqueness of solutions (TauCeti.timeDependentFlowOf_eq_of_hasMFDerivAt) it is the flow line of f₀ x. The velocity field loses one derivative: a C^n isotopy, 2 ≤ n, gives a C^m diffeotopy for every m with 1 ≤ m and m + 1 ≤ n, and a smooth isotopy a smooth diffeotopy.

For a compact source, smooth isotopy and smooth ambient isotopy of smooth embeddings are therefore the same relation (TauCeti.smoothAmbientIsotopic_iff_smoothIsotopic); the forward implication is TauCeti.SmoothAmbientIsotopic.smoothIsotopic.

Main results

• TauCeti.SmoothIsotopy.exists_diffeotopy_apply_eq: a smooth isotopy is, on a compact subset of its source, the restriction of a compactly supported diffeotopy, after the change of time Real.smoothTransition.
• TauCeti.SmoothIsotopy.exists_diffeotopy_apply_eq_of_forall_notMem: the same, with the diffeotopy fixing a closed set missed by the moving part of the compact subset.
• TauCeti.SmoothIsotopy.exists_diffeotopy_final_apply_eq: the final diffeomorphism of that diffeotopy carries the initial embedding to the final one on the compact subset.
• TauCeti.SmoothIsotopic.smoothAmbientIsotopic: smoothly isotopic smooth maps of a compact boundaryless manifold are smoothly ambient isotopic.
• TauCeti.smoothAmbientIsotopic_iff_smoothIsotopic: for smooth embeddings of a compact boundaryless manifold, smooth ambient isotopy is smooth isotopy.

References

• M. W. Hirsch, Differential Topology, Graduate Texts in Mathematics 33, Springer (1976), Chapter 8, §1, Theorems 1.3 and 1.4.

theorem TauCeti.SmoothIsotopy.exists_diffeotopy_apply_eq_of_forall_notMem {E : Type u_1} {E' : Type u_2} {H : Type u_3} {H' : Type u_4} {M : Type u_5} {N : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ 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] [J.Boundaryless] [IsManifold J (↑⊤) N] [T2Space N] [SigmaCompactSpace N] {n m : ℕ∞} [IsManifold I (↑n) M] {f₀ f₁ : ContMDiffMap I J M N ↑n} (F : SmoothIsotopy f₀ f₁) {A₀ A : Set M} {C : Set N} (hA₀ : IsCompact A₀) (hA : IsCompact A) (hC : IsClosed C) (hA₀C : ∀ (t : ↑unitInterval), ∀ x ∈ A₀, F (t, x) ∉ C) (hstat : ∀ (t : ↑unitInterval), ∀ x ∈ A, x ∉ A₀ → F (t, x) = f₀ x) (hm : 1 ≤ m) (hmn : m + 1 ≤ n) : ∃ (Φ : Diffeotopy J (↑m) N) (K : Set N), IsCompact K ∧ (∀ (t : ↑unitInterval), ∀ y ∉ K, (fun (p : ↑unitInterval × N) => (Φ.toDiffeomorph p).2) (t, y) = y) ∧ (∀ (t : ↑unitInterval), ∀ x ∈ A, (fun (p : ↑unitInterval × N) => (Φ.toDiffeomorph p).2) (t, f₀ x) = F (⟨(↑t).smoothTransition, ⋯⟩, x)) ∧ ∀ (t : ↑unitInterval), ∀ y ∈ C, (fun (p : ↑unitInterval × N) => (Φ.toDiffeomorph p).2) (t, y) = y

Isotopy extension fixing a closed set. Let F be a C^n isotopy through smooth embeddings into a finite-dimensional boundaryless manifold, and A, A₀ compact subsets of the source such that F keeps fixed every point of A outside A₀. If the motion of A₀ never meets the closed set C, then the motion of A is the restriction of a C^m diffeotopy Φ of the target fixing every point of C and every point outside a compact set, for 1 ≤ m and m + 1 ≤ n: Φ (t, f₀ x) = F (σ t, x) for x ∈ A, where σ is the change of time Real.smoothTransition, and Φ (t, y) = y for y ∈ C.

This is how isotopy extension leaves alone a part of the target that the isotopy does not move, such as the rest of a line along which an arc is straightened.

theorem TauCeti.SmoothIsotopy.exists_diffeotopy_apply_eq {E : Type u_1} {E' : Type u_2} {H : Type u_3} {H' : Type u_4} {M : Type u_5} {N : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ 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] [J.Boundaryless] [IsManifold J (↑⊤) N] [T2Space N] [SigmaCompactSpace N] {n m : ℕ∞} [IsManifold I (↑n) M] {f₀ f₁ : ContMDiffMap I J M N ↑n} (F : SmoothIsotopy f₀ f₁) {A : Set M} (hA : IsCompact A) (hm : 1 ≤ m) (hmn : m + 1 ≤ n) : ∃ (Φ : Diffeotopy J (↑m) N) (K : Set N), IsCompact K ∧ (∀ (t : ↑unitInterval), ∀ y ∉ K, (fun (p : ↑unitInterval × N) => (Φ.toDiffeomorph p).2) (t, y) = y) ∧ ∀ (t : ↑unitInterval), ∀ x ∈ A, (fun (p : ↑unitInterval × N) => (Φ.toDiffeomorph p).2) (t, f₀ x) = F (⟨(↑t).smoothTransition, ⋯⟩, x)

Isotopy extension on a compact subset. A C^n isotopy F of a boundaryless manifold through smooth embeddings into a finite-dimensional boundaryless manifold is, on any compact subset A of the source, the restriction of a C^m diffeotopy Φ of the target fixing every point outside a compact set, for 1 ≤ m and m + 1 ≤ n: Φ (t, f₀ x) = F (σ t, x) for x ∈ A, where σ t = Real.smoothTransition t. The source need not be compact.

theorem TauCeti.SmoothIsotopy.exists_diffeotopy_final_apply_eq {E : Type u_1} {E' : Type u_2} {H : Type u_3} {H' : Type u_4} {M : Type u_5} {N : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ 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] [J.Boundaryless] [IsManifold J (↑⊤) N] [T2Space N] [SigmaCompactSpace N] {n m : ℕ∞} [IsManifold I (↑n) M] {f₀ f₁ : ContMDiffMap I J M N ↑n} (F : SmoothIsotopy f₀ f₁) {A : Set M} (hA : IsCompact A) (hm : 1 ≤ m) (hmn : m + 1 ≤ n) : ∃ (Φ : Diffeotopy J (↑m) N) (K : Set N), IsCompact K ∧ (∀ (t : ↑unitInterval), ∀ y ∉ K, (fun (p : ↑unitInterval × N) => (Φ.toDiffeomorph p).2) (t, y) = y) ∧ ∀ x ∈ A, Φ.final (f₀ x) = f₁ x

Isotopy extension on a compact subset, final form. The final diffeomorphism of a compactly supported C^m diffeotopy carries the initial embedding f₀ of a C^n isotopy to the final one f₁ on any compact subset of the source, for 1 ≤ m and m + 1 ≤ n.

theorem TauCeti.SmoothIsotopic.smoothAmbientIsotopic {E : Type u_1} {E' : Type u_2} {H : Type u_3} {H' : Type u_4} {M : Type u_5} {N : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ 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] [J.Boundaryless] [IsManifold J (↑⊤) N] [T2Space N] [SigmaCompactSpace N] [CompactSpace M] [IsManifold I (↑⊤) M] {f₀ f₁ : ContMDiffMap I J M N ↑⊤} (h : SmoothIsotopic f₀ f₁) : SmoothAmbientIsotopic f₀ f₁

Smooth isotopy implies smooth ambient isotopy for a compact source. Smoothly isotopic smooth maps of a compact boundaryless manifold into a finite-dimensional boundaryless manifold are smoothly ambient isotopic.

theorem TauCeti.smoothAmbientIsotopic_iff_smoothIsotopic {E : Type u_1} {E' : Type u_2} {H : Type u_3} {H' : Type u_4} {M : Type u_5} {N : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ 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] [J.Boundaryless] [IsManifold J (↑⊤) N] [T2Space N] [SigmaCompactSpace N] [CompactSpace M] [IsManifold I (↑⊤) M] {f₀ f₁ : ContMDiffMap I J M N ↑⊤} (hf₀ : Manifold.IsSmoothEmbedding I J ↑⊤ ⇑f₀) : SmoothAmbientIsotopic f₀ f₁ ↔ SmoothIsotopic f₀ f₁

Smooth ambient isotopy is smooth isotopy for a compact source. A smooth embedding f₀ of a compact boundaryless manifold into a finite-dimensional boundaryless manifold is smoothly ambient isotopic to a smooth map f₁ exactly when it is smoothly isotopic to it.