Diffeotopies generated by complete vector fields

A complete C^n vector field, 1 ≤ n, generates a diffeotopy on a possibly noncompact finite-dimensional boundaryless manifold. The motion at time t ∈ [0,1] is the field's flow at time a * t, for an arbitrary real duration a. Its inverse uses time -(a * t). Every zero of the field is fixed throughout. In particular, a field vanishing outside a compact set generates a motion supported in the same set.

A time-dependent C^n vector field X whose suspension is complete generates a diffeotopy too (TauCeti.timeDependentFlowDiffeotopy): the motion at time t ∈ [0,1] is its time-dependent flow from time 0 to time t, with inverse the flow from t back to 0. This holds in particular when X vanishes outside a fixed compact set at all times (TauCeti.isCompleteVectorField_timeDependentSuspensionField). Points at which X vanishes at all times are fixed throughout.

This converts cut-off local vector fields into ambient motions with controlled support. The isotopy extension theorem runs the time-dependent diffeotopy of the ambient velocity field of an isotopy through embeddings.

Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorems 9.12, 9.16 and 9.48.

noncomputable def TauCeti.globalFlowDiffeotopy {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [BoundarylessManifold I M] {n : ℕ∞} [IsManifold I (↑n) M] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} (hn : 1 ≤ n) (hv : ContMDiff I I.tangent ↑n fun (y : M) => ⟨y, v y⟩) (hcomplete : IsCompleteVectorField v) (a : ℝ) : Diffeotopy I (↑n) M

Run a complete C^n vector field for duration a, starting at the identity. The ambient manifold need not be compact, and negative durations are allowed.

@[simp]

theorem TauCeti.globalFlowDiffeotopy_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [BoundarylessManifold I M] {n : ℕ∞} [IsManifold I (↑n) M] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} (hn : 1 ≤ n) (hv : ContMDiff I I.tangent ↑n fun (y : M) => ⟨y, v y⟩) (hcomplete : IsCompleteVectorField v) (a : ℝ) (p : ↑unitInterval × M) : (fun (p : ↑unitInterval × M) => ((globalFlowDiffeotopy hn hv hcomplete a).toDiffeomorph p).2) p = maximalIntegralCurve v p.2 (a * ↑p.1)

The motion is the maximal integral curve of the field at the rescaled time.

@[simp]

theorem TauCeti.globalFlowDiffeotopy_toDiffeomorph_symm_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [BoundarylessManifold I M] {n : ℕ∞} [IsManifold I (↑n) M] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} (hn : 1 ≤ n) (hv : ContMDiff I I.tangent ↑n fun (y : M) => ⟨y, v y⟩) (hcomplete : IsCompleteVectorField v) (a : ℝ) (p : ↑unitInterval × M) : (globalFlowDiffeotopy hn hv hcomplete a).toDiffeomorph.symm p = (p.1, maximalIntegralCurve v p.2 (-(a * ↑p.1)))

The inverse motion runs the same field for the opposite duration.

theorem TauCeti.globalFlowDiffeotopy_apply_of_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [BoundarylessManifold I M] {n : ℕ∞} [IsManifold I (↑n) M] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} (hn : 1 ≤ n) (hv : ContMDiff I I.tangent ↑n fun (y : M) => ⟨y, v y⟩) (hcomplete : IsCompleteVectorField v) (a : ℝ) {x : M} (hx : v x = 0) (t : ↑unitInterval) : (fun (p : ↑unitInterval × M) => ((globalFlowDiffeotopy hn hv hcomplete a).toDiffeomorph p).2) (t, x) = x

Every zero of the generating field is fixed throughout the diffeotopy.

noncomputable def TauCeti.compactlySupportedFlowDiffeotopy {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [BoundarylessManifold I M] {n : ℕ∞} [IsManifold I (↑n) M] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} {K : Set M} (hn : 1 ≤ n) (hv : ContMDiff I I.tangent ↑n fun (y : M) => ⟨y, v y⟩) (hK : IsCompact K) (hzero : ∀ y ∉ K, v y = 0) (a : ℝ) : Diffeotopy I (↑n) M

Run a compactly supported C^n vector field for duration a, starting at the identity. The ambient manifold need not be compact, and negative durations are allowed.

@[simp]

theorem TauCeti.compactlySupportedFlowDiffeotopy_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [BoundarylessManifold I M] {n : ℕ∞} [IsManifold I (↑n) M] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} {K : Set M} (hn : 1 ≤ n) (hv : ContMDiff I I.tangent ↑n fun (y : M) => ⟨y, v y⟩) (hK : IsCompact K) (hzero : ∀ y ∉ K, v y = 0) (a : ℝ) (p : ↑unitInterval × M) : (fun (p : ↑unitInterval × M) => ((compactlySupportedFlowDiffeotopy hn hv hK hzero a).toDiffeomorph p).2) p = maximalIntegralCurve v p.2 (a * ↑p.1)

The compactly supported motion is the maximal integral curve at the rescaled time.

@[simp]

theorem TauCeti.compactlySupportedFlowDiffeotopy_toDiffeomorph_symm_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [BoundarylessManifold I M] {n : ℕ∞} [IsManifold I (↑n) M] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} {K : Set M} (hn : 1 ≤ n) (hv : ContMDiff I I.tangent ↑n fun (y : M) => ⟨y, v y⟩) (hK : IsCompact K) (hzero : ∀ y ∉ K, v y = 0) (a : ℝ) (p : ↑unitInterval × M) : (compactlySupportedFlowDiffeotopy hn hv hK hzero a).toDiffeomorph.symm p = (p.1, maximalIntegralCurve v p.2 (-(a * ↑p.1)))

The inverse compactly supported motion runs the field for the opposite duration.

theorem TauCeti.compactlySupportedFlowDiffeotopy_apply_of_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [BoundarylessManifold I M] {n : ℕ∞} [IsManifold I (↑n) M] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} {K : Set M} (hn : 1 ≤ n) (hv : ContMDiff I I.tangent ↑n fun (y : M) => ⟨y, v y⟩) (hK : IsCompact K) (hzero : ∀ y ∉ K, v y = 0) (a : ℝ) {x : M} (hx : v x = 0) (t : ↑unitInterval) : (fun (p : ↑unitInterval × M) => ((compactlySupportedFlowDiffeotopy hn hv hK hzero a).toDiffeomorph p).2) (t, x) = x

Every zero of a compactly supported generating field is fixed throughout the motion.

theorem TauCeti.compactlySupportedFlowDiffeotopy_eqOn_compl {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [BoundarylessManifold I M] {n : ℕ∞} [IsManifold I (↑n) M] [IsManifold I 1 M] {v : (x : M) → TangentSpace I x} {K : Set M} (hn : 1 ≤ n) (hv : ContMDiff I I.tangent ↑n fun (y : M) => ⟨y, v y⟩) (hK : IsCompact K) (hzero : ∀ y ∉ K, v y = 0) (a : ℝ) (t : ↑unitInterval) : Set.EqOn (fun (x : M) => (fun (p : ↑unitInterval × M) => ((compactlySupportedFlowDiffeotopy hn hv hK hzero a).toDiffeomorph p).2) (t, x)) id Kᶜ

The entire motion fixes the complement of the prescribed compact support set.

Time-dependent vector fields

noncomputable def TauCeti.timeDependentFlowDiffeotopy {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [BoundarylessManifold I M] {n : ℕ∞} [IsManifold I (↑n) M] [IsManifold I 1 M] {X : ℝ → (x : M) → TangentSpace I x} (hn : 1 ≤ n) (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent ↑n fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) (hcomplete : IsCompleteVectorField (timeDependentSuspensionField X)) : Diffeotopy I (↑n) M

Run a time-dependent C^n vector field with complete suspension, 1 ≤ n, from time 0: the motion at time t ∈ [0, 1] is the time-dependent flow of X from time 0 to time t.

@[simp]

theorem TauCeti.timeDependentFlowDiffeotopy_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [BoundarylessManifold I M] {n : ℕ∞} [IsManifold I (↑n) M] [IsManifold I 1 M] {X : ℝ → (x : M) → TangentSpace I x} (hn : 1 ≤ n) (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent ↑n fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) (hcomplete : IsCompleteVectorField (timeDependentSuspensionField X)) (p : ↑unitInterval × M) : (fun (p : ↑unitInterval × M) => ((timeDependentFlowDiffeotopy hn hX hcomplete).toDiffeomorph p).2) p = timeDependentFlowOf X 0 (↑p.1) p.2

The time-dependent motion at time t is the time-dependent flow from 0 to t.

@[simp]

theorem TauCeti.timeDependentFlowDiffeotopy_toDiffeomorph_symm_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [BoundarylessManifold I M] {n : ℕ∞} [IsManifold I (↑n) M] [IsManifold I 1 M] {X : ℝ → (x : M) → TangentSpace I x} (hn : 1 ≤ n) (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent ↑n fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) (hcomplete : IsCompleteVectorField (timeDependentSuspensionField X)) (p : ↑unitInterval × M) : (timeDependentFlowDiffeotopy hn hX hcomplete).toDiffeomorph.symm p = (p.1, timeDependentFlowOf X (↑p.1) 0 p.2)

The inverse time-dependent motion at time t is the time-dependent flow from t back to 0.

theorem TauCeti.timeDependentFlowDiffeotopy_apply_of_forall_eq_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [BoundarylessManifold I M] {n : ℕ∞} [IsManifold I (↑n) M] [IsManifold I 1 M] {X : ℝ → (x : M) → TangentSpace I x} (hn : 1 ≤ n) (hX : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) I.tangent ↑n fun (p : ℝ × M) => ⟨p.2, X p.1 p.2⟩) (hcomplete : IsCompleteVectorField (timeDependentSuspensionField X)) {x : M} (hx : ∀ (u : ℝ), X u x = 0) (t : ↑unitInterval) : (fun (p : ↑unitInterval × M) => ((timeDependentFlowDiffeotopy hn hX hcomplete).toDiffeomorph p).2) (t, x) = x

A point at which the field vanishes at all times is fixed throughout the time-dependent motion.