Moore paths and paths on the unit interval

Moore paths compare with the fixed-interval model C(I, X) of paths parametrized by the unit interval I = [0, 1]. A path f : C(I, X) becomes the Moore path MoorePath.ofUnitPath f of length one, stopped at time one; a Moore path γ of length L becomes the path MoorePath.toUnitPath γ : s ↦ γ (L s) on the unit interval. Going from C(I, X) to the Moore paths and back is the identity (toUnitPath_ofUnitPath); going from the Moore paths to C(I, X) and back changes the length to one and reparametrizes, and the result is homotopic to the original path through Moore paths with the same end points (MoorePath.unitHomotopy). So the two path spaces are homotopy equivalent over X × X (MoorePath.homotopyEquivUnitPath), and the based version follows: the Moore loops MooreLoopSpace X x are homotopy equivalent to Mathlib's loops Path x x (MooreLoopSpace.homotopyEquivPath). Away from length zero there is no need to pass through length one: the Moore loops of positive length are homeomorphic to (0, ∞) × Path x x (MooreLoopSpace.posLengthHomeomorph). The Moore loop of length zero is the unit alone, while there are as many loops of each positive length as there are fixed-interval loops.

The homotopy is assembled from three pieces, each one a homotopy through maps that preserve the two end points, so that their composite is one as well (MoorePath.PreservesEndpoints, ContinuousMap.HomotopyWith):

• appending a constant path of length s ∈ [0, 1] at the target, which only changes the length;
• rescaling (MoorePath.rescale) the path of length L + 1 down to length one, which divides by lengths at least one;
• the image of the first homotopy under ofUnitPath ∘ toUnitPath.

The detour through length L + 1 avoids dividing by a length that could be zero.

Main definitions

• TauCeti.MoorePath.ofUnitPath, TauCeti.MoorePath.toUnitPath: the comparison maps between C(I, X) and MoorePath X.
• TauCeti.MoorePath.ofUnitPath_toUnitPath: going to the unit interval and back is MoorePath.rescale γ 1, the reparametrization to length one.
• Path.toMoorePath, TauCeti.MoorePath.toPath, Path.toMooreLoop, TauCeti.MooreLoopSpace.toPath: the based comparison maps.
• TauCeti.MoorePath.unitHomotopy: the homotopy from ofUnitPath ∘ toUnitPath to the identity through end-point preserving maps.
• TauCeti.MooreLoopSpace.unitHomotopy: its restriction to the Moore loops at x.
• TauCeti.MoorePath.homotopyEquivUnitPath: the homotopy equivalence MoorePath X ≃ₕ C(I, X).
• TauCeti.MooreLoopSpace.homotopyEquivPath: the homotopy equivalence MooreLoopSpace X x ≃ₕ Path x x with Mathlib's loop space.
• TauCeti.MooreLoopSpace.posLengthHomeomorph: the Moore loops of positive length are homeomorphic to (0, ∞) × Path x x, by the length and toPath.

Main results

• TauCeti.MoorePath.toUnitPath_ofUnitPath, Path.toPath_toMoorePath, Path.toPath_toMooreLoop: one composite is the identity on the nose.
• TauCeti.MoorePath.unitHomotopy_source, TauCeti.MoorePath.unitHomotopy_target: the homotopy for the other composite preserves the end points.

References

• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Floer homology with DG coefficients. Applications to cotangent bundles, arXiv:2404.07953, §7.1.
• G. W. Whitehead, Elements of Homotopy Theory, GTM 61, Springer, 1978, Chapter III.

The comparison maps

noncomputable def TauCeti.MoorePath.ofUnitPath {X : Type u_1} [TopologicalSpace X] (f : C(↑unitInterval, X)) : MoorePath X

A path on the unit interval, as a Moore path of length one, stopped at time one.

@[simp]

theorem TauCeti.MoorePath.ofUnitPath_apply {X : Type u_1} [TopologicalSpace X] (f : C(↑unitInterval, X)) (t : NNReal) : (ofUnitPath f).toContinuousMap t = f (Set.projIcc 0 1 ⋯ ↑t)

@[simp]

theorem TauCeti.MoorePath.length_ofUnitPath {X : Type u_1} [TopologicalSpace X] (f : C(↑unitInterval, X)) : (ofUnitPath f).length = 1

@[simp]

theorem TauCeti.MoorePath.source_ofUnitPath {X : Type u_1} [TopologicalSpace X] (f : C(↑unitInterval, X)) : (ofUnitPath f).source = f 0

@[simp]

theorem TauCeti.MoorePath.target_ofUnitPath {X : Type u_1} [TopologicalSpace X] (f : C(↑unitInterval, X)) : (ofUnitPath f).target = f 1

theorem TauCeti.MoorePath.continuous_ofUnitPath {X : Type u_1} [TopologicalSpace X] : Continuous ofUnitPath

def TauCeti.MoorePath.toUnitPath {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : C(↑unitInterval, X)

A Moore path of length L, reparametrized to the unit interval: s ↦ γ (L s).

@[simp]

theorem TauCeti.MoorePath.toUnitPath_apply {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (s : ↑unitInterval) : γ.toUnitPath s = γ.toContinuousMap (γ.length * unitInterval.toNNReal s)

theorem TauCeti.MoorePath.toUnitPath_zero {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : γ.toUnitPath 0 = γ.source

theorem TauCeti.MoorePath.toUnitPath_one {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : γ.toUnitPath 1 = γ.target

theorem TauCeti.MoorePath.continuous_toUnitPath {X : Type u_1} [TopologicalSpace X] : Continuous toUnitPath

@[simp]

theorem TauCeti.MoorePath.toUnitPath_ofUnitPath {X : Type u_1} [TopologicalSpace X] (f : C(↑unitInterval, X)) : (ofUnitPath f).toUnitPath = f

A path on the unit interval, sent to the Moore paths and back, is unchanged.

@[simp]

theorem TauCeti.MoorePath.toUnitPath_refl {X : Type u_1} [TopologicalSpace X] (x : X) : (refl x).toUnitPath = ContinuousMap.const (↑unitInterval) x

@[simp]

theorem TauCeti.MoorePath.toUnitPath_constOfLength {X : Type u_1} [TopologicalSpace X] (x : X) (L : NNReal) : (constOfLength x L).toUnitPath = ContinuousMap.const (↑unitInterval) x

@[simp]

theorem TauCeti.MoorePath.ofUnitPath_const {X : Type u_1} [TopologicalSpace X] (x : X) : ofUnitPath (ContinuousMap.const (↑unitInterval) x) = constOfLength x 1

theorem TauCeti.MoorePath.ofUnitPath_toUnitPath_apply {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (t : NNReal) : (ofUnitPath γ.toUnitPath).toContinuousMap t = γ.toContinuousMap (γ.length * min t 1)

A Moore path sent to the unit interval and back: the path t ↦ γ (L · min t 1) of length one.

theorem TauCeti.MoorePath.ofUnitPath_toUnitPath {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : ofUnitPath γ.toUnitPath = γ.rescale 1

Sending a Moore path to the unit interval and back reparametrizes it to length one.

The homotopy from ofUnitPath ∘ toUnitPath to the identity

def TauCeti.MoorePath.PreservesEndpoints {X : Type u_1} [TopologicalSpace X] (f : C(MoorePath X, MoorePath X)) : Prop

A self-map of the Moore paths preserves the end points. The homotopies below are through such maps, so they are homotopies over X × X.

noncomputable def TauCeti.MoorePath.toLengthOne {X : Type u_1} [TopologicalSpace X] : C(MoorePath X, MoorePath X)

The composite ofUnitPath ∘ toUnitPath, bundled: a Moore path, reparametrized to length one (ofUnitPath_toUnitPath_apply).

@[simp]

theorem TauCeti.MoorePath.toLengthOne_apply {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : toLengthOne γ = ofUnitPath γ.toUnitPath

theorem TauCeti.MoorePath.toLengthOne_eq_rescale_one {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : toLengthOne γ = γ.rescale 1

noncomputable def TauCeti.MoorePath.unitHomotopy {X : Type u_1} [TopologicalSpace X] : toLengthOne.HomotopyWith (ContinuousMap.id (MoorePath X)) PreservesEndpoints

The homotopy from ofUnitPath ∘ toUnitPath to the identity of the Moore paths, through maps preserving the end points: a Moore path is homotopic, through Moore paths with the same end points, to its reparametrization to length one.

theorem TauCeti.MoorePath.unitHomotopy_apply_zero {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : unitHomotopy (0, γ) = ofUnitPath γ.toUnitPath

theorem TauCeti.MoorePath.unitHomotopy_apply_one {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : unitHomotopy (1, γ) = γ

theorem TauCeti.MoorePath.unitHomotopy_source {X : Type u_1} [TopologicalSpace X] (s : ↑unitInterval) (γ : MoorePath X) : (unitHomotopy (s, γ)).source = γ.source

theorem TauCeti.MoorePath.unitHomotopy_target {X : Type u_1} [TopologicalSpace X] (s : ↑unitInterval) (γ : MoorePath X) : (unitHomotopy (s, γ)).target = γ.target

noncomputable def TauCeti.MoorePath.homotopyEquivUnitPath {X : Type u_1} [TopologicalSpace X] : ContinuousMap.HomotopyEquiv (MoorePath X) C(↑unitInterval, X)

Moore paths and paths on the unit interval are homotopy equivalent, by toUnitPath and ofUnitPath; the homotopy unitHomotopy preserves the end points, so this is a homotopy equivalence over X × X.

@[simp]

theorem TauCeti.MoorePath.homotopyEquivUnitPath_apply {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : homotopyEquivUnitPath.toFun γ = γ.toUnitPath

@[simp]

theorem TauCeti.MoorePath.homotopyEquivUnitPath_symm_apply {X : Type u_1} [TopologicalSpace X] (f : C(↑unitInterval, X)) : homotopyEquivUnitPath.symm.toFun f = ofUnitPath f

The based comparison

noncomputable def Path.toMoorePath {X : Type u_1} [TopologicalSpace X] {x y : X} (p : Path x y) : TauCeti.MoorePath X

A path on the unit interval from x to y, as a Moore path of length one.

@[simp]

theorem Path.toMoorePath_apply {X : Type u_1} [TopologicalSpace X] {x y : X} (p : Path x y) (t : NNReal) : p.toMoorePath.toContinuousMap t = p.extend ↑t

@[simp]

theorem Path.length_toMoorePath {X : Type u_1} [TopologicalSpace X] {x y : X} (p : Path x y) : p.toMoorePath.length = 1

@[simp]

theorem Path.source_toMoorePath {X : Type u_1} [TopologicalSpace X] {x y : X} (p : Path x y) : p.toMoorePath.source = x

@[simp]

theorem Path.target_toMoorePath {X : Type u_1} [TopologicalSpace X] {x y : X} (p : Path x y) : p.toMoorePath.target = y

theorem Path.continuous_toMoorePath {X : Type u_1} [TopologicalSpace X] {x y : X} : Continuous toMoorePath

def TauCeti.MoorePath.toPath {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : Path γ.source γ.target

A Moore path, as a path on the unit interval between its end points.

@[simp]

theorem TauCeti.MoorePath.toPath_apply {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (s : ↑unitInterval) : γ.toPath s = γ.toContinuousMap (γ.length * unitInterval.toNNReal s)

@[simp]

theorem Path.toPath_toMoorePath {X : Type u_1} [TopologicalSpace X] {x y : X} (p : Path x y) : p.toMoorePath.toPath = p.cast ⋯ ⋯

A path on the unit interval, sent to the Moore paths and back, is unchanged, up to the identification of its end points.

def TauCeti.MooreLoopSpace.toPath {X : Type u_1} [TopologicalSpace X] {x : X} (γ : MooreLoopSpace X x) : Path x x

A Moore loop at x, as a loop on the unit interval.

@[simp]

theorem TauCeti.MooreLoopSpace.toPath_apply {X : Type u_1} [TopologicalSpace X] {x : X} (γ : MooreLoopSpace X x) (s : ↑unitInterval) : γ.toPath s = γ.toMoorePath.toContinuousMap (γ.toMoorePath.length * unitInterval.toNNReal s)

theorem TauCeti.MooreLoopSpace.continuous_toPath {X : Type u_1} [TopologicalSpace X] {x : X} : Continuous toPath

@[simp]

theorem TauCeti.MooreLoopSpace.toPath_one {X : Type u_1} [TopologicalSpace X] {x : X} : toPath 1 = Path.refl x

Normalizing the Moore unit gives the constant fixed-interval loop.

noncomputable def Path.toMooreLoop {X : Type u_1} [TopologicalSpace X] {x : X} (p : Path x x) : TauCeti.MooreLoopSpace X x

A loop on the unit interval at x, as a Moore loop of length one.

@[simp]

theorem Path.toMoorePath_toMooreLoop {X : Type u_1} [TopologicalSpace X] {x : X} (p : Path x x) : p.toMooreLoop.toMoorePath = p.toMoorePath

theorem Path.continuous_toMooreLoop {X : Type u_1} [TopologicalSpace X] {x : X} : Continuous toMooreLoop

@[simp]

theorem Path.toPath_toMooreLoop {X : Type u_1} [TopologicalSpace X] {x : X} (p : Path x x) : p.toMooreLoop.toPath = p

A loop on the unit interval, sent to the Moore loops and back, is unchanged.

noncomputable def TauCeti.MooreLoopSpace.toLengthOne {X : Type u_1} [TopologicalSpace X] {x : X} : C(MooreLoopSpace X x, MooreLoopSpace X x)

The composite Path.toMooreLoop ∘ toPath, bundled: a Moore loop reparametrized to length one.

@[simp]

theorem TauCeti.MooreLoopSpace.toLengthOne_apply {X : Type u_1} [TopologicalSpace X] {x : X} (γ : MooreLoopSpace X x) : toLengthOne γ = γ.toPath.toMooreLoop

theorem TauCeti.MooreLoopSpace.toMoorePath_toLengthOne {X : Type u_1} [TopologicalSpace X] {x : X} (γ : MooreLoopSpace X x) : (toLengthOne γ).toMoorePath = MoorePath.toLengthOne γ.toMoorePath

theorem TauCeti.MooreLoopSpace.toMoorePath_toPath {X : Type u_1} [TopologicalSpace X] {x : X} (γ : MooreLoopSpace X x) : γ.toPath.toMoorePath = γ.toMoorePath.rescale 1

A Moore loop reparametrized to the unit interval, as a Moore path, is its rescaling to length one.

noncomputable def TauCeti.MooreLoopSpace.unitHomotopy {X : Type u_1} [TopologicalSpace X] {x : X} : toLengthOne.Homotopy (ContinuousMap.id (MooreLoopSpace X x))

The homotopy from toLengthOne to the identity of the Moore loops at x: the restriction of MoorePath.unitHomotopy, which preserves the end points, to the loops.

@[simp]

theorem TauCeti.MooreLoopSpace.toMoorePath_unitHomotopy {X : Type u_1} [TopologicalSpace X] {x : X} (s : ↑unitInterval) (γ : MooreLoopSpace X x) : (unitHomotopy (s, γ)).toMoorePath = MoorePath.unitHomotopy (s, γ.toMoorePath)

theorem TauCeti.MooreLoopSpace.unitHomotopy_apply_zero {X : Type u_1} [TopologicalSpace X] {x : X} (γ : MooreLoopSpace X x) : unitHomotopy (0, γ) = γ.toPath.toMooreLoop

theorem TauCeti.MooreLoopSpace.unitHomotopy_apply_one {X : Type u_1} [TopologicalSpace X] {x : X} (γ : MooreLoopSpace X x) : unitHomotopy (1, γ) = γ

noncomputable def TauCeti.MooreLoopSpace.homotopyEquivPath {X : Type u_1} [TopologicalSpace X] (x : X) : ContinuousMap.HomotopyEquiv (MooreLoopSpace X x) (Path x x)

The Moore loop space is homotopy equivalent to Mathlib's loop space Path x x of loops parametrized by the unit interval, by toPath and Path.toMooreLoop.

@[simp]

theorem TauCeti.MooreLoopSpace.homotopyEquivPath_apply {X : Type u_1} [TopologicalSpace X] {x : X} (γ : MooreLoopSpace X x) : (homotopyEquivPath x).toFun γ = γ.toPath

@[simp]

theorem TauCeti.MooreLoopSpace.homotopyEquivPath_symm_apply {X : Type u_1} [TopologicalSpace X] {x : X} (p : Path x x) : (homotopyEquivPath x).symm.toFun p = p.toMooreLoop

Moore loops of positive length

noncomputable def TauCeti.MooreLoopSpace.posLengthHomeomorph {X : Type u_1} [TopologicalSpace X] (x : X) : ↑(length ⁻¹' Set.Ioi 0) ≃ₜ ↑(Set.Ioi 0) × Path x x

Moore loops of positive length are pairs of a positive length and a loop on the unit interval: a Moore loop is sent to its length and to its reparametrization to the unit interval, and a pair (L, c) to the loop c run in time L. In particular, over positive lengths, the length of Moore loops is a product projection, with fibre the loop space Path x x.

@[simp]

theorem TauCeti.MooreLoopSpace.posLengthHomeomorph_apply_fst {X : Type u_1} [TopologicalSpace X] {x : X} (γ : ↑(length ⁻¹' Set.Ioi 0)) : ↑((posLengthHomeomorph x) γ).1 = (↑γ).length

@[simp]

theorem TauCeti.MooreLoopSpace.posLengthHomeomorph_apply_snd {X : Type u_1} [TopologicalSpace X] {x : X} (γ : ↑(length ⁻¹' Set.Ioi 0)) : ((posLengthHomeomorph x) γ).2 = (↑γ).toPath

@[simp]

theorem TauCeti.MooreLoopSpace.toMoorePath_posLengthHomeomorph_symm_apply {X : Type u_1} [TopologicalSpace X] {x : X} (q : ↑(Set.Ioi 0) × Path x x) : (↑((posLengthHomeomorph x).symm q)).toMoorePath = q.2.toMoorePath.rescale ↑q.1

@[simp]

theorem TauCeti.MooreLoopSpace.length_posLengthHomeomorph_symm_apply {X : Type u_1} [TopologicalSpace X] {x : X} (q : ↑(Set.Ioi 0) × Path x x) : (↑((posLengthHomeomorph x).symm q)).length = ↑q.1

@[simp]

theorem TauCeti.MooreLoopSpace.toPath_posLengthHomeomorph_symm_apply {X : Type u_1} [TopologicalSpace X] {x : X} (q : ↑(Set.Ioi 0) × Path x x) : (↑((posLengthHomeomorph x).symm q)).toPath = q.2

@[simp]

theorem TauCeti.MooreLoopSpace.toPath_map {X : Type u_1} [TopologicalSpace X] {x : X} {Y : Type u_2} [TopologicalSpace Y] (f : C(X, Y)) (γ : MooreLoopSpace X x) : ((map f ⋯) γ).toPath = γ.toPath.map ⋯

Reparametrizing to the unit interval commutes with the Moore loop map of a continuous map.