Concatenation equivalences of Moore path spaces

Prepending a chosen Moore path from a to b gives a homotopy equivalence from the paths from b to c to the paths from a to c. Its inverse prepends the reversed path. The inverse homotopies shrink a path followed by its reversal by truncating the outward leg. Both concatenation maps and the inverse homotopies commute strictly with the right action of loops at c.

In particular, the space of paths from a to b is right-equivariantly homotopy equivalent to the Moore loops at b, after choosing a path from a to b. This is the topological input for the chain bimodules used to change basepoints in DG local systems. No concatenation with a reversed path is asserted to equal a constant path: its duration is generally nonzero.

References

• G. W. Whitehead, Elements of Homotopy Theory, Chapter III.
• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Morse homology with differential graded coefficients, Progress in Mathematics 360, Birkhäuser, 2025, §7.1.

noncomputable def TauCeti.MoorePathBetween.prepend {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePathBetween X a b) (c : X) : C(MoorePathBetween X b c, MoorePathBetween X a c)

Prepend a chosen Moore path.

@[simp]

theorem TauCeti.MoorePathBetween.prepend_apply {X : Type u_1} [TopologicalSpace X] {a b c : X} (γ : MoorePathBetween X a b) (δ : MoorePathBetween X b c) : (γ.prepend c) δ = γ.trans δ

theorem TauCeti.MoorePathBetween.prepend_op_smul {X : Type u_1} [TopologicalSpace X] {a b c : X} (γ : MoorePathBetween X a b) (δ : MoorePathBetween X b c) (ω : MooreLoopSpace X c) : (γ.prepend c) (MulOpposite.op ω • δ) = MulOpposite.op ω • (γ.prepend c) δ

Prepending commutes strictly with the right action at the final endpoint.

noncomputable def TauCeti.MoorePathBetween.retrace {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePathBetween X a b) (s : NNReal) : MooreLoopSpace X a

A retracing loop, obtained by truncating the outward leg before returning along it.

@[simp]

theorem TauCeti.MoorePathBetween.toMoorePath_retrace {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePathBetween X a b) (s : NNReal) : (γ.retrace s).toMoorePath = (γ.toMoorePath.truncate s).trans (γ.toMoorePath.truncate s).symm ⋯

The underlying path of the retracing loop.

@[simp]

theorem TauCeti.MoorePathBetween.retrace_zero {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePathBetween X a b) : γ.retrace 0 = 1

theorem TauCeti.MoorePathBetween.continuous_retrace {X : Type u_1} [TopologicalSpace X] {a b : X} : Continuous fun (p : MoorePathBetween X a b × NNReal) => p.1.retrace p.2

Retracing is jointly continuous in the path and the truncation time.

noncomputable def TauCeti.MoorePathBetween.prependSymmHomotopy {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePathBetween X a b) (c : X) : (ContinuousMap.id (MoorePathBetween X a c)).Homotopy ((γ.prepend c).comp (γ.symm.prepend c))

Grow a retracing prefix from duration zero to the full path and its reversal.

@[simp]

theorem TauCeti.MoorePathBetween.prependSymmHomotopy_apply {X : Type u_1} [TopologicalSpace X] {a b c : X} (γ : MoorePathBetween X a b) (s : ↑unitInterval) (δ : MoorePathBetween X a c) : (γ.prependSymmHomotopy c) (s, δ) = leftAct (γ.retrace (unitInterval.toNNReal s * γ.toMoorePath.length)) δ

The inverse homotopy is given by a retracing prefix acting on the path.

theorem TauCeti.MoorePathBetween.prependSymmHomotopy_op_smul {X : Type u_1} [TopologicalSpace X] {a b c : X} (γ : MoorePathBetween X a b) (s : ↑unitInterval) (δ : MoorePathBetween X a c) (ω : MooreLoopSpace X c) : (γ.prependSymmHomotopy c) (s, MulOpposite.op ω • δ) = MulOpposite.op ω • (γ.prependSymmHomotopy c) (s, δ)

Every intermediate map of the inverse homotopy commutes with the right loop action.

noncomputable def TauCeti.MoorePathBetween.prependHomotopyEquiv {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePathBetween X a b) (c : X) : ContinuousMap.HomotopyEquiv (MoorePathBetween X b c) (MoorePathBetween X a c)

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

@[simp]

theorem TauCeti.MoorePathBetween.prependHomotopyEquiv_apply {X : Type u_1} [TopologicalSpace X] {a b c : X} (γ : MoorePathBetween X a b) (δ : MoorePathBetween X b c) : (γ.prependHomotopyEquiv c).toFun δ = γ.trans δ

@[simp]

theorem TauCeti.MoorePathBetween.prependHomotopyEquiv_symm_apply {X : Type u_1} [TopologicalSpace X] {a b c : X} (γ : MoorePathBetween X a b) (δ : MoorePathBetween X a c) : (γ.prependHomotopyEquiv c).symm.toFun δ = γ.symm.trans δ

noncomputable def TauCeti.MoorePathBetween.loopPrependHomotopyEquiv {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePathBetween X a b) : ContinuousMap.HomotopyEquiv (MooreLoopSpace X b) (MoorePathBetween X a b)

Prepending a chosen path identifies loops at its target with paths between its endpoints, up to homotopy.

@[simp]

theorem TauCeti.MoorePathBetween.loopPrependHomotopyEquiv_apply {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePathBetween X a b) (ω : MooreLoopSpace X b) : γ.loopPrependHomotopyEquiv.toFun ω = γ.rightAct ω

@[simp]

theorem TauCeti.MoorePathBetween.toMoorePath_loopPrependHomotopyEquiv_symm {X : Type u_1} [TopologicalSpace X] {a b : X} (γ δ : MoorePathBetween X a b) : (γ.loopPrependHomotopyEquiv.symm.toFun δ).toMoorePath = γ.toMoorePath.symm.trans δ.toMoorePath ⋯

The inverse first prepends the reversed path, then regards the result as a loop.

theorem TauCeti.MoorePathBetween.loopPrependHomotopyEquiv_op_smul {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePathBetween X a b) (ω η : MooreLoopSpace X b) : γ.loopPrependHomotopyEquiv.toFun (MulOpposite.op η • ω) = MulOpposite.op η • γ.loopPrependHomotopyEquiv.toFun ω

The loop-to-path equivalence commutes strictly with right multiplication by loops.