Smooth tracks and their split differentials

The time-preserving track (t, x) ↦ (t, F(t, x)) of a smooth isotopy is jointly smooth. Its differential admits a continuous linear left inverse whenever the isotopy has positive differentiability order. For compact sources and Hausdorff targets, the track is also a closed topological embedding.

These results supply the space-time image and its split tangent directions used when extending the velocity of an isotopy to an ambient vector field. They apply to manifolds with corners and infinite-dimensional models. A split differential is not asserted to provide an immersion normal form at boundary points. For boundaryless manifolds and a finite-dimensional target model, ContMDiff.isSmoothEmbedding_fst_prod shows that a real-time motion through smooth embeddings has a smoothly embedded track.

Reference: M. Hirsch, Differential Topology, Chapter 8, §1, the proof of the isotopy extension theorem. The differential calculation uses Mathlib's product chain rule and Manifold.IsImmersion.isDiffImmersionAt.

def TauCeti.SmoothIsotopy.track {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'] [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₀ f₁ : ContMDiffMap I J M N n} (F : SmoothIsotopy f₀ f₁) : ContMDiffMap ((modelWithCornersEuclideanHalfSpace 1).prod I) ((modelWithCornersEuclideanHalfSpace 1).prod J) (↑unitInterval × M) (↑unitInterval × N) n

The smooth time-preserving track of an isotopy through smooth embeddings.

@[simp]

theorem TauCeti.SmoothIsotopy.track_apply {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'] [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₀ f₁ : ContMDiffMap I J M N n} (F : SmoothIsotopy f₀ f₁) (p : ↑unitInterval × M) : F.track p = (p.1, F p)

The smooth track records time and the moving point.

@[simp]

theorem TauCeti.SmoothIsotopy.toContinuousMap_track {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'] [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₀ f₁ : ContMDiffMap I J M N n} (F : SmoothIsotopy f₀ f₁) : ↑F.track = F.toIsotopy.track

Forgetting smoothness preserves the track.

theorem TauCeti.SmoothIsotopy.isClosedEmbedding_track {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'] [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₀ f₁ : ContMDiffMap I J M N n} [CompactSpace M] [T2Space N] (F : SmoothIsotopy f₀ f₁) : Topology.IsClosedEmbedding ⇑F.track

The smooth track of a compact-source isotopy into a Hausdorff manifold is a closed topological embedding.

theorem TauCeti.SmoothIsotopy.hasLeftInverse_mfderiv_track {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'] [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₀ f₁ : ContMDiffMap I J M N n} (F : SmoothIsotopy f₀ f₁) (hn : n ≠ 0) (p : ↑unitInterval × M) : (mfderiv% ⇑F.track p).HasLeftInverse

At positive differentiability order, every differential of the track has a continuous linear left inverse. No compactness or finite-dimensionality is required.

theorem ContMDiff.isSmoothEmbedding_fst_prod {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] {n : WithTop ℕ∞} [I.Boundaryless] [J.Boundaryless] [IsManifold I n M] [IsManifold J n N] [CompactSpace M] [T2Space N] {G : ℝ × M → N} (hG : ContMDiff ((modelWithCornersSelf ℝ ℝ).prod I) J n G) (hslice : ∀ (t : ℝ), Topology.IsEmbedding fun (x : M) => G (t, x)) (hdiff : ∀ (t : ℝ) (x : M), IsDiffImmersionAt I J (fun (x : M) => G (t, x)) x) (hn : 1 ≤ n) : Manifold.IsSmoothEmbedding ((modelWithCornersSelf ℝ ℝ).prod I) ((modelWithCornersSelf ℝ ℝ).prod J) n fun (q : ℝ × M) => (q.1, G q)

The time-preserving track of a jointly smooth motion through topological embeddings with split injective slice differentials, from a compact boundaryless source into a finite-dimensional Hausdorff boundaryless target is a smooth embedding. The source model need not be assumed finite-dimensional or complete.