Collared tracks

A concordance between two embeddings f g : M → N is an embedding of M × [0, 1] into N × [0, 1] restricting to f and g on the two ends. To avoid manifolds with boundary, Tau Ceti records a concordance in collared form: as a map F : M × ℝ → N × ℝ which is the product f × id for all times t ≤ ε and the product g × id for all times t ≥ 1 - ε, for some positive collar width ε, and which maps the open slab M × (0, 1) into the open slab N × (0, 1). Two such tracks with a common middle embedding can be run one after the other, and the uniform collars are what make the seam invisible: on a whole open slab around it both tracks are the same product g × id.

This file isolates these end conditions on the bare map, TauCeti.IsCollaredTrack f g F, and develops everything about a concordance that does not depend on the regularity asked of its track — smooth, locally flat or merely topological. That is: the end conditions imply that the track is the appropriate product for all t ≤ 0 and all t ≥ 1 and that it moves no time level across 0 or 1; the product f × id is a track from f to f; a track can be pushed forward along a map of the target or pulled back along a map of the source, and followed by an injective map of N × ℝ fixing everything outside a compact subset of the open slab; time can be reflected (TauCeti.reverseTime), giving a track from g to f; and two tracks can be stacked (TauCeti.stack), the first run at triple speed on [0, 1/3] and the second at triple speed on [2/3, 1], giving a track from f to h. The stacked track is glued from two open slabs, and it is an embedding as soon as the two tracks are, because the pieces are embeddings and the seam lies in the product region.

Main definitions

• TauCeti.IsCollaredTrack f g F: the end conditions of a collared track from f to g.
• TauCeti.conjTime F a b: the conjugate of F by the affine change of time t ↦ a * t + b.
• TauCeti.reverseTime F: the track run backwards, time being reflected in 1 / 2.
• TauCeti.stack F G: the first track at triple speed until time 1 / 2, then the second.

Main results

• TauCeti.IsCollaredTrack.snd_apply_lt_iff, TauCeti.IsCollaredTrack.lt_snd_apply_iff and TauCeti.IsCollaredTrack.snd_apply_mem_Ioo_iff: a collared track preserves the comparison of the time coordinate with any level outside (0, 1).
• TauCeti.isCollaredTrack_prodMap_id, TauCeti.IsCollaredTrack.reverseTime and TauCeti.IsCollaredTrack.stack: the constant, reversed and stacked tracks are collared tracks.
• TauCeti.IsCollaredTrack.comp_of_isCompact: a collared track followed by an injective map of N × ℝ which fixes everything outside a compact subset of the open slab is a collared track between the same maps.
• TauCeti.IsCollaredTrack.isEmbedding_stack: the stack of two collared tracks which are topological embeddings is a topological embedding.
• TauCeti.IsCollaredTrack.isClosedEmbedding: a continuous injective collared track with compact source and Hausdorff target is a closed embedding.
• TauCeti.IsCollaredTrack.snd_apply_mem_Icc_iff: a collared track meets the closed slab N × [0, 1] exactly over M × [0, 1].
• TauCeti.IsCollaredTrack.exists_pos_range_inter_snd_le and TauCeti.IsCollaredTrack.exists_pos_range_inter_le_snd: over a compact source, the image of a continuous collared track is the cylinder over the image of f at all heights at most some ε > 0, and the cylinder over the image of g at all heights at least 1 - ε.

References

• J. F. P. Hudson, Concordance, isotopy, and diffeotopy, Ann. of Math. 91 (1970), 425–448.

structure TauCeti.IsCollaredTrack {M : Type u_1} {N : Type u_3} (f g : M → N) (F : M × ℝ → N × ℝ) : Prop

A map F : M × ℝ → N × ℝ is a collared track from f to g when it is the product f × id for all times t ≤ ε and the product g × id for all times t ≥ 1 - ε, for some positive collar width ε, and maps the open slab M × (0, 1) into the open slab N × (0, 1). These are the end conditions of a concordance in collared form, whatever regularity is asked of the track.

• exists_pos_apply_eq_left : ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : M), ∀ t ≤ ε, F (x, t) = (f x, t)

  The track is the product of f with the identity on a collar of the initial end.

• exists_pos_apply_eq_right : ∃ (ε : ℝ), 0 < ε ∧ ∀ (x : M) (t : ℝ), 1 - ε ≤ t → F (x, t) = (g x, t)

  The track is the product of g with the identity on a collar of the final end.

• snd_apply_mem_Ioo (x : M) (t : ℝ) (ht : t ∈ Set.Ioo 0 1) : (F (x, t)).2 ∈ Set.Ioo 0 1

  The track maps the open slab M × (0, 1) into the open slab N × (0, 1).

theorem TauCeti.IsCollaredTrack.apply_of_nonpos {M : Type u_1} {N : Type u_3} {f g : M → N} {F : M × ℝ → N × ℝ} (hF : IsCollaredTrack f g F) (x : M) {t : ℝ} (ht : t ≤ 0) : F (x, t) = (f x, t)

A collared track is the product of its initial map with the identity for t ≤ 0.

theorem TauCeti.IsCollaredTrack.apply_of_one_le {M : Type u_1} {N : Type u_3} {f g : M → N} {F : M × ℝ → N × ℝ} (hF : IsCollaredTrack f g F) (x : M) {t : ℝ} (ht : 1 ≤ t) : F (x, t) = (g x, t)

A collared track is the product of its final map with the identity for 1 ≤ t.

theorem TauCeti.IsCollaredTrack.apply_zero {M : Type u_1} {N : Type u_3} {f g : M → N} {F : M × ℝ → N × ℝ} (hF : IsCollaredTrack f g F) (x : M) : F (x, 0) = (f x, 0)

At time 0 a collared track is its initial map.

theorem TauCeti.IsCollaredTrack.apply_one {M : Type u_1} {N : Type u_3} {f g : M → N} {F : M × ℝ → N × ℝ} (hF : IsCollaredTrack f g F) (x : M) : F (x, 1) = (g x, 1)

At time 1 a collared track is its final map.

theorem TauCeti.IsCollaredTrack.exists_pos_apply_eq_line {M : Type u_1} {N : Type u_3} {f g : M → N} {F : M × ℝ → N × ℝ} (hF : IsCollaredTrack f g F) {z₀ : M} (hz₀ : g z₀ = f z₀) : ∃ ε₀ > 0, ∃ ε₁ > 0, ∀ (t : ℝ), t ≤ ε₀ ∨ 1 - ε₁ ≤ t → F (z₀, t) = (f z₀, t)

Near both of its ends the arc t ↦ F (z₀, t) of a collared track from f to g, with g z₀ = f z₀, is the straight line t ↦ (f z₀, t).

theorem TauCeti.IsCollaredTrack.snd_apply_lt_iff {M : Type u_1} {N : Type u_3} {f g : M → N} {F : M × ℝ → N × ℝ} (hF : IsCollaredTrack f g F) (x : M) {t c : ℝ} (hc : c ∉ Set.Ioo 0 1) : (F (x, t)).2 < c ↔ t < c

A collared track moves no time outside the open interval (0, 1) and keeps times inside it, so it preserves the comparison of time with any level c ∉ (0, 1).

theorem TauCeti.IsCollaredTrack.lt_snd_apply_iff {M : Type u_1} {N : Type u_3} {f g : M → N} {F : M × ℝ → N × ℝ} (hF : IsCollaredTrack f g F) (x : M) {t c : ℝ} (hc : c ∉ Set.Ioo 0 1) : c < (F (x, t)).2 ↔ c < t

A collared track preserves the comparison of time with any level c ∉ (0, 1) from below.

theorem TauCeti.IsCollaredTrack.snd_apply_mem_Ioo_iff {M : Type u_1} {N : Type u_3} {f g : M → N} {F : M × ℝ → N × ℝ} (hF : IsCollaredTrack f g F) (x : M) {t : ℝ} : (F (x, t)).2 ∈ Set.Ioo 0 1 ↔ t ∈ Set.Ioo 0 1

A collared track maps M × (0, 1) into N × (0, 1) and nothing else there.

theorem TauCeti.IsCollaredTrack.snd_apply_mem_Icc_iff {M : Type u_1} {N : Type u_3} {f g : M → N} {F : M × ℝ → N × ℝ} (hF : IsCollaredTrack f g F) (x : M) {t : ℝ} : (F (x, t)).2 ∈ Set.Icc 0 1 ↔ t ∈ Set.Icc 0 1

A collared track meets the closed slab N × [0, 1] exactly over M × [0, 1].

theorem TauCeti.IsCollaredTrack.prodMap_id_comp {M : Type u_1} {N : Type u_3} {P : Type u_4} {f g : M → N} {F : M × ℝ → N × ℝ} (hF : IsCollaredTrack f g F) (e : N → P) : IsCollaredTrack (e ∘ f) (e ∘ g) (Prod.map e id ∘ F)

Pushing a collared track from f to g forward along a map e of the target gives a collared track from e ∘ f to e ∘ g.

theorem TauCeti.IsCollaredTrack.comp_prodMap_id {M : Type u_1} {M' : Type u_2} {N : Type u_3} {f g : M → N} {F : M × ℝ → N × ℝ} (hF : IsCollaredTrack f g F) (e : M' → M) : IsCollaredTrack (f ∘ e) (g ∘ e) (F ∘ Prod.map e id)

Pulling a collared track from f to g back along a map e of the source gives a collared track from f ∘ e to g ∘ e.

theorem TauCeti.IsCollaredTrack.comp_of_isCompact {M : Type u_1} {N : Type u_3} {f g : M → N} {F : M × ℝ → N × ℝ} [TopologicalSpace N] (hF : IsCollaredTrack f g F) {ψ : N × ℝ → N × ℝ} (hψ : Function.Injective ψ) {C : Set (N × ℝ)} (hC : IsCompact C) (hCslab : ∀ q ∈ C, q.2 ∈ Set.Ioo 0 1) (hψC : ∀ q ∉ C, ψ q = q) : IsCollaredTrack f g (ψ ∘ F)

Following a collared track from f to g by an injective map ψ of N × ℝ which fixes every point outside a compact subset C of the open slab N × (0, 1) gives a collared track from f to g: compactness keeps C away from the two ends of the slab, where the track is untouched.

theorem TauCeti.isCollaredTrack_prodMap_id {M : Type u_1} {N : Type u_3} (f : M → N) : IsCollaredTrack f f (Prod.map f id)

The product f × id is a collared track from f to itself.

Affine changes of time

noncomputable def TauCeti.conjTime {M : Type u_1} {N : Type u_3} (F : M × ℝ → N × ℝ) (a b : ℝ) (p : M × ℝ) : N × ℝ

The conjugate of a map F : M × ℝ → N × ℝ by the affine change of time t ↦ a * t + b: run F at the time a * t + b and read the resulting time back through the inverse change.

@[simp]

theorem TauCeti.conjTime_apply {M : Type u_1} {N : Type u_3} (F : M × ℝ → N × ℝ) (a b : ℝ) (x : M) (t : ℝ) : conjTime F a b (x, t) = ((F (x, a * t + b)).1, ((F (x, a * t + b)).2 - b) / a)

theorem TauCeti.conjTime_eq_comp {M : Type u_1} {N : Type u_3} [TopologicalSpace M] [TopologicalSpace N] (F : M × ℝ → N × ℝ) {a : ℝ} (b : ℝ) (ha : a ≠ 0) : conjTime F a b = ⇑((Homeomorph.refl N).prodCongr (affineHomeomorph a b ha).symm) ∘ F ∘ ⇑((Homeomorph.refl M).prodCongr (affineHomeomorph a b ha))

For a ≠ 0 the affine change of time is a homeomorphism of the line, and the conjugate track is the conjugate of F by the corresponding self-homeomorphisms of M × ℝ and N × ℝ.

noncomputable def TauCeti.reverseTime {M : Type u_1} {N : Type u_3} (F : M × ℝ → N × ℝ) : M × ℝ → N × ℝ

Reversing a track: reflect time in 1 / 2, so that the track is run backwards.

theorem TauCeti.reverseTime_def {M : Type u_1} {N : Type u_3} (F : M × ℝ → N × ℝ) : reverseTime F = conjTime F (-1) 1

Reversing time is conjugation by the reflection t ↦ -t + 1.

@[simp]

theorem TauCeti.reverseTime_apply {M : Type u_1} {N : Type u_3} (F : M × ℝ → N × ℝ) (x : M) (t : ℝ) : reverseTime F (x, t) = ((F (x, 1 - t)).1, 1 - (F (x, 1 - t)).2)

@[simp]

theorem TauCeti.reverseTime_reverseTime {M : Type u_1} {N : Type u_3} (F : M × ℝ → N × ℝ) : reverseTime (reverseTime F) = F

Reversing a track twice gives it back.

theorem TauCeti.IsCollaredTrack.reverseTime {M : Type u_1} {N : Type u_3} {f g : M → N} {F : M × ℝ → N × ℝ} (hF : IsCollaredTrack f g F) : IsCollaredTrack g f (TauCeti.reverseTime F)

The reversed track of a collared track from f to g is a collared track from g to f.

Stacking tracks

noncomputable def TauCeti.stack {M : Type u_1} {N : Type u_3} (F G : M × ℝ → N × ℝ) (p : M × ℝ) : N × ℝ

The stack of two tracks: the first track run at triple speed until time 1 / 2, the second track run at triple speed afterwards. For collared tracks with a common middle map g both are the product g × id on the slab [1/3, 2/3], so the seam at 1 / 2 is invisible.

theorem TauCeti.stack_apply_of_le {M : Type u_1} {N : Type u_3} (F G : M × ℝ → N × ℝ) (x : M) {t : ℝ} (ht : t ≤ 1 / 2) : stack F G (x, t) = ((F (x, 3 * t)).1, (F (x, 3 * t)).2 / 3)

Until time 1 / 2 the stacked track runs the first track at triple speed.

theorem TauCeti.stack_apply_of_lt {M : Type u_1} {N : Type u_3} (F G : M × ℝ → N × ℝ) (x : M) {t : ℝ} (ht : 1 / 2 < t) : stack F G (x, t) = ((G (x, 3 * t - 2)).1, ((G (x, 3 * t - 2)).2 + 2) / 3)

After time 1 / 2 the stacked track runs the second track at triple speed.

theorem TauCeti.IsCollaredTrack.stack_eqOn_lower {M : Type u_1} {N : Type u_3} {f g h : M → N} {F G : M × ℝ → N × ℝ} (hF : IsCollaredTrack f g F) (hG : IsCollaredTrack g h G) : Set.EqOn (TauCeti.stack F G) (conjTime F 3 0) {p : M × ℝ | p.2 < 2 / 3}

Before time 2 / 3 the stack of two collared tracks is the first track at triple speed.

theorem TauCeti.IsCollaredTrack.stack_eqOn_upper {M : Type u_1} {N : Type u_3} {f g h : M → N} {F G : M × ℝ → N × ℝ} (hF : IsCollaredTrack f g F) (hG : IsCollaredTrack g h G) : Set.EqOn (TauCeti.stack F G) (conjTime G 3 (-2)) {p : M × ℝ | 1 / 3 < p.2}

After time 1 / 3 the stack of two collared tracks is the second track at triple speed.

theorem TauCeti.IsCollaredTrack.snd_stack_lt_iff {M : Type u_1} {N : Type u_3} {f g h : M → N} {F G : M × ℝ → N × ℝ} (hF : IsCollaredTrack f g F) (hG : IsCollaredTrack g h G) (p : M × ℝ) : (TauCeti.stack F G p).2 < 2 / 3 ↔ p.2 < 2 / 3

The stacked track preserves the comparison of time with the level 2 / 3.

theorem TauCeti.IsCollaredTrack.lt_snd_stack_iff {M : Type u_1} {N : Type u_3} {f g h : M → N} {F G : M × ℝ → N × ℝ} (hF : IsCollaredTrack f g F) (hG : IsCollaredTrack g h G) (p : M × ℝ) : 1 / 3 < (TauCeti.stack F G p).2 ↔ 1 / 3 < p.2

The stacked track preserves the comparison of time with the level 1 / 3.

theorem TauCeti.IsCollaredTrack.stack {M : Type u_1} {N : Type u_3} {f g h : M → N} {F G : M × ℝ → N × ℝ} (hF : IsCollaredTrack f g F) (hG : IsCollaredTrack g h G) : IsCollaredTrack f h (TauCeti.stack F G)

The stack of a collared track from f to g and one from g to h is a collared track from f to h.

theorem TauCeti.IsCollaredTrack.isEmbedding_stack {M : Type u_1} {N : Type u_3} {f g h : M → N} {F G : M × ℝ → N × ℝ} [TopologicalSpace M] [TopologicalSpace N] (hF : IsCollaredTrack f g F) (hG : IsCollaredTrack g h G) (hF' : Topology.IsEmbedding F) (hG' : Topology.IsEmbedding G) : Topology.IsEmbedding (TauCeti.stack F G)

The stack of two collared tracks which are topological embeddings is a topological embedding.

theorem TauCeti.IsCollaredTrack.isClosedEmbedding {M : Type u_1} {N : Type u_3} {f g : M → N} {F : M × ℝ → N × ℝ} [TopologicalSpace M] [TopologicalSpace N] [CompactSpace M] [T2Space N] (hF : IsCollaredTrack f g F) (hc : Continuous F) (hinj : Function.Injective F) : Topology.IsClosedEmbedding F

A continuous injective collared track with compact source M and Hausdorff target N is a closed embedding.

theorem TauCeti.IsCollaredTrack.exists_pos_range_inter_snd_le {M : Type u_1} {N : Type u_3} {f g : M → N} {F : M × ℝ → N × ℝ} [TopologicalSpace M] [TopologicalSpace N] [CompactSpace M] (hF : IsCollaredTrack f g F) (hc : Continuous F) : ∃ ε > 0, Set.range F ∩ {p : N × ℝ | p.2 ≤ ε} = Set.range f ×ˢ Set.Iic ε

Over a compact source, the image of a continuous collared track from f is the cylinder over the image of f up to some positive height ε: its points of height at most ε are exactly the points of range f ×ˢ Iic ε. The collar width of the track alone does not give this, since points of the middle of the track may come down to low heights; compactness keeps them above a positive height.

theorem TauCeti.IsCollaredTrack.exists_pos_range_inter_le_snd {M : Type u_1} {N : Type u_3} {f g : M → N} {F : M × ℝ → N × ℝ} [TopologicalSpace M] [TopologicalSpace N] [CompactSpace M] (hF : IsCollaredTrack f g F) (hc : Continuous F) : ∃ ε > 0, Set.range F ∩ {p : N × ℝ | 1 - ε ≤ p.2} = Set.range g ×ˢ Set.Ici (1 - ε)

Over a compact source, the image of a continuous collared track to g is the cylinder over the image of g from some height 1 - ε, ε > 0, on: its points of height at least 1 - ε are exactly the points of range g ×ˢ Ici (1 - ε).