Prepending a path to the paths of the unit interval

For a fixed path α from x to y, concatenation γ ↦ α.trans γ is a continuous map Path.prepend α z from the compact-open space of paths from y to z to that of paths from x to z. Up to homotopy of maps between path spaces, prepending is associative, unital and depends only on the path-homotopy class of α, each homotopy being continuous in the path γ. Consequently prepending α is a homotopy equivalence Path.prependHomotopyEquiv, with homotopy inverse prepending the reversed path α.symm. Taking z = y identifies the loop space Ω X y with the space of paths from x to y, after choosing α. No such identification is canonical: it depends on the chosen path.

This is the unit-interval counterpart of TauCeti.MoorePathBetween.prependHomotopyEquiv for Moore paths. Unlike the Moore model, concatenation on the unit interval is associative and unital only up to reparametrization, so the homotopies here are reparametrizations (Path.reparamHomotopy) and Serre's delay homotopy Path.delayReflLeft.

Main definitions

• Path.prepend α z: the continuous map γ ↦ α.trans γ.
• Path.reparamHomotopy: the straight-line homotopy from the identity of a path space to a reparametrization.
• Path.Homotopic.cast_map_reparam: reparametrizing every loop of a loop of loops does not change its homotopy class.
• Path.Homotopic.Quotient.cast_map_trans_prod_refl and Path.Homotopic.Quotient.cast_map_trans_refl_prod: concatenating every loop of a loop of loops with the constant loop does not change its class.
• Path.prependHomotopyEquiv α z: Path y z ≃ₕ Path x z, with inverse prepending α.symm.

References

• G. W. Whitehead, Elements of Homotopy Theory, GTM 61, Springer, 1978, Chapter III.

theorem Path.delayReflLeft_continuous_family {X : Type u_1} [TopologicalSpace X] {A : Type u_2} [TopologicalSpace A] {a b : A → X} (γ : (q : A) → Path (a q) (b q)) (hγ : Continuous ↿γ) (s : C(A, ↑unitInterval)) : Continuous ↿fun (q : A) => delayReflLeft (s q) (γ q)

Serre's left delay is continuous for a family of paths with varying endpoints.

Reparametrizing the paths of a path space

theorem Path.continuous_reparam {X : Type u_1} [TopologicalSpace X] {x y : X} {f : ↑unitInterval → ↑unitInterval} (hf : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : Continuous fun (γ : Path x y) => γ.reparam f hf hf₀ hf₁

Reparametrizing by a fixed endpoint-preserving map f : I → I is continuous on the compact-open space of paths.

def Path.reparamHomotopy {X : Type u_1} [TopologicalSpace X] {x y : X} (f : ↑unitInterval → ↑unitInterval) (hf : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : (ContinuousMap.id (Path x y)).Homotopy { toFun := fun (γ : Path x y) => γ.reparam f hf hf₀ hf₁, continuous_toFun := ⋯ }

The straight-line homotopy from the identity of the path space to reparametrization by f, evaluating Path.Homotopy.reparam γ f at each time. It is continuous in the path.

@[simp]

theorem Path.reparamHomotopy_apply {X : Type u_1} [TopologicalSpace X] {x y : X} (f : ↑unitInterval → ↑unitInterval) (hf : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) (s : ↑unitInterval) (γ : Path x y) : (reparamHomotopy f hf hf₀ hf₁) (s, γ) = (Homotopy.reparam γ f hf hf₀ hf₁).eval s

theorem Path.Homotopic.cast_map_reparam {X : Type u_1} [TopologicalSpace X] {x : X} (L : Path (Path.refl x) (Path.refl x)) {f : ↑unitInterval → ↑unitInterval} (hf : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : ((L.map ⋯).cast ⋯ ⋯).Homotopic L

Reparametrizing every loop of a loop L at the constant loop in Ω X x by the same map f does not change the homotopy class of L: reparamHomotopy acts on all loops at once and fixes the constant loop.

@[simp]

theorem Path.Homotopic.Quotient.cast_map_trans_prod_refl {X : Type u_1} [TopologicalSpace X] {x : X} (L : Homotopic.Quotient (Path.refl x) (Path.refl x)) : ((prod L (refl (Path.refl x))).map { toFun := fun (ρ : Path x x × Path x x) => ρ.1.trans ρ.2, continuous_toFun := ⋯ }).cast ⋯ ⋯ = L

Concatenating every loop of a loop of loops L at the constant loop with the constant loop does not change its homotopy class.

@[simp]

theorem Path.Homotopic.Quotient.cast_map_trans_refl_prod {X : Type u_1} [TopologicalSpace X] {x : X} (L : Homotopic.Quotient (Path.refl x) (Path.refl x)) : ((prod (refl (Path.refl x)) L).map { toFun := fun (ρ : Path x x × Path x x) => ρ.1.trans ρ.2, continuous_toFun := ⋯ }).cast ⋯ ⋯ = L

Concatenating the constant loop with every loop of a loop of loops L at the constant loop does not change its homotopy class.

Prepending a path

noncomputable def Path.prepend {X : Type u_1} [TopologicalSpace X] {x y : X} (α : Path x y) (z : X) : C(Path y z, Path x z)

Prepending a fixed path α from x to y, as a continuous map from the paths from y to z to the paths from x to z.

@[simp]

theorem Path.prepend_apply {X : Type u_1} [TopologicalSpace X] {x y z : X} (α : Path x y) (γ : Path y z) : (α.prepend z) γ = α.trans γ

theorem Path.homotopic_prepend_comp_prepend {X : Type u_1} [TopologicalSpace X] {w x y : X} (p : Path w x) (q : Path x y) (z : X) : ((p.prepend z).comp (q.prepend z)).Homotopic ((p.trans q).prepend z)

Prepending q and then p is homotopic to prepending p.trans q.

theorem Path.Homotopic.prepend {X : Type u_1} [TopologicalSpace X] {x y : X} {p p' : Path x y} (h : p.Homotopic p') (z : X) : (p.prepend z).Homotopic (p'.prepend z)

Prepending depends only on the path-homotopy class of the prepended path.

theorem Path.homotopic_prepend_refl {X : Type u_1} [TopologicalSpace X] (x z : X) : ((refl x).prepend z).Homotopic (ContinuousMap.id (Path x z))

Prepending a constant path is homotopic to the identity, by Serre's delay homotopy.

noncomputable def Path.prependHomotopyEquiv {X : Type u_1} [TopologicalSpace X] {x y : X} (α : Path x y) (z : X) : ContinuousMap.HomotopyEquiv (Path y z) (Path x z)

Prepending a path is a homotopy equivalence, with homotopy inverse prepending its reversal.

@[simp]

theorem Path.prependHomotopyEquiv_apply {X : Type u_1} [TopologicalSpace X] {x y z : X} (α : Path x y) (γ : Path y z) : (α.prependHomotopyEquiv z).toFun γ = α.trans γ

@[simp]

theorem Path.prependHomotopyEquiv_symm_apply {X : Type u_1} [TopologicalSpace X] {x y z : X} (α : Path x y) (γ : Path x z) : (α.prependHomotopyEquiv z).symm.toFun γ = α.symm.trans γ