Tracks of isotopies with compact source

The track of an isotopy retains time as its first coordinate. For a compact source and Hausdorff target it is a closed embedding, so points of the moving image have continuous source coordinates. Compactness matters here: slice-wise embeddings alone do not guarantee that the track of a noncompact isotopy is an embedding.

Reference: M. Hirsch, Differential Topology, Chapter 8, §1, the track construction in the proof of the isotopy extension theorem.

def TauCeti.Isotopy.track {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (F : Isotopy f₀ f₁) : C(↑unitInterval × X, ↑unitInterval × Y)

The time-preserving track of an isotopy.

@[simp]

theorem TauCeti.Isotopy.track_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (F : Isotopy f₀ f₁) (p : ↑unitInterval × X) : F.track p = (p.1, F p)

The track records both time and the moving point.

theorem TauCeti.Isotopy.track_injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (F : Isotopy f₀ f₁) : Function.Injective ⇑F.track

Distinct points of the space-time source have distinct track images.

theorem TauCeti.Isotopy.isClosedEmbedding_track {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} [CompactSpace X] [T2Space Y] (F : Isotopy f₀ f₁) : Topology.IsClosedEmbedding ⇑F.track

The track of a compact-source isotopy into a Hausdorff space is a closed embedding.

theorem TauCeti.Isotopy.mem_range_track {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f₀ f₁ : C(X, Y)} (F : Isotopy f₀ f₁) (q : ↑unitInterval × Y) : q ∈ Set.range ⇑F.track ↔ q.2 ∈ Set.range fun (x : X) => F (q.1, x)

A space-time point lies on the track exactly when its spatial coordinate lies on the image of the corresponding time slice. This is an explicit rewrite lemma, since Set.mem_range already expands its left-hand side in the simplifier.