Ambient velocity on a compact part of a smooth isotopy

A smooth isotopy of a possibly noncompact boundaryless manifold has a compactly supported ambient velocity field on each compact subset of its source. Run the isotopy over the real line using Real.smoothTransition, so the resulting motion is stationary before time zero and after time one. Every point of the chosen compact subset then follows an integral curve of a single jointly smooth time-dependent vector field with support in a fixed compact set.

For an open-disc isotopy, choose a closed ball as the compact subset. This supplies the velocity field used to extend the motion of that closed disc to an ambient isotopy; no manifold structure on the closed disc, or compactness of the open source, is required.

References

• M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 8, §1, Theorems 1.3--1.4 and their proof.

theorem TauCeti.SmoothIsotopy.exists_ambientVelocityField {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) : ∃ (X : ℝ → (y : N) → TangentSpace J y) (K : Set N), IsCompact K ∧ (∀ (t : ℝ), ∀ y ∉ K, X t y = 0) ∧ (ContMDiff ((modelWithCornersSelf ℝ ℝ).prod J) J.tangent ↑m fun (p : ℝ × N) => ⟨p.2, X p.1 p.2⟩) ∧ ∀ (t : ℝ), ∀ x ∈ A, HasMFDerivAt% (fun (s : ℝ) => F (⟨s.smoothTransition, ⋯⟩, x)) t (ContinuousLinearMap.smulRight 1 (X t (F (⟨t.smoothTransition, ⋯⟩, x))))

On any compact subset of its boundaryless source, a smooth isotopy run at the time Real.smoothTransition t moves each point along a compactly supported ambient vector field. The field is jointly C^m in time and space for 1 ≤ m and m + 1 ≤ n.