Concatenation under the comparison with the unit interval

The comparison Path.toMoorePath of TauCeti.Topology.PathSpace.Moore.Comparison.Basic does not take the concatenation p.trans q of two paths on the unit interval to the concatenation of their Moore paths: the first runs through both paths at double speed in length one, the second runs through them at unit speed in length two. The two differ by a reparametrization, and this file records that they are homotopic through a homotopy that is continuous in the pair of paths and preserves the end points: p.toMoorePath.trans q.toMoorePath is (p.trans q).toMoorePath.rescale 2 (Path.transMoorePath_eq_rescale), and MoorePath.rescale from length 1 to length 2 is the homotopy (Path.transMoorePathHomotopy). This is the compatibility of the comparison with the concatenation actions of the loop spaces on the path spaces.

For loops, this says that Path.toMooreLoop : Path x x → MooreLoopSpace X x is a monoid homomorphism up to homotopy (Path.transMooreLoopHomotopy), and, through the homotopy equivalence, so is MooreLoopSpace.toPath in the other direction (MooreLoopSpace.mulToPathHomotopy): the homotopy equivalence MooreLoopSpace.homotopyEquivPath is multiplicative up to homotopy in both directions.

Main results

• Path.transMoorePath_eq_rescale: p.toMoorePath.trans q.toMoorePath is (p.trans q).toMoorePath reparametrized to length two.
• Path.transMoorePathHomotopy: the homotopy from (p.trans q).toMoorePath to p.toMoorePath.trans q.toMoorePath, continuous in (p, q), through paths from x to z (transMoorePathHomotopy_source, transMoorePathHomotopy_target).
• Path.transMooreLoopHomotopy: Path.toMooreLoop is multiplicative up to homotopy.
• TauCeti.MooreLoopSpace.mulToPathHomotopy: MooreLoopSpace.toPath is multiplicative up to homotopy.

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 concatenation of two Moore paths of length one

theorem Path.transMoorePath_eq_rescale {X : Type u_1} [TopologicalSpace X] {x y z : X} (p : Path x y) (q : Path y z) : p.toMoorePath.trans q.toMoorePath ⋯ = (p.trans q).toMoorePath.rescale 2

The concatenation of the Moore paths of p and q is the Moore path of p.trans q, reparametrized from length one to length two.

noncomputable def Path.moorePathTrans {X : Type u_1} [TopologicalSpace X] (x y z : X) : C(Path x y × Path y z, TauCeti.MoorePath X)

The Moore path of the concatenation of two paths on the unit interval, as a continuous map of the pair.

@[simp]

theorem Path.moorePathTrans_apply {X : Type u_1} [TopologicalSpace X] {x y z : X} (pq : Path x y × Path y z) : (moorePathTrans x y z) pq = (pq.1.trans pq.2).toMoorePath

noncomputable def Path.transMoorePath {X : Type u_1} [TopologicalSpace X] (x y z : X) : C(Path x y × Path y z, TauCeti.MoorePath X)

The concatenation of the Moore paths of two paths on the unit interval, as a continuous map of the pair.

@[simp]

theorem Path.transMoorePath_apply {X : Type u_1} [TopologicalSpace X] {x y z : X} (pq : Path x y × Path y z) : (transMoorePath x y z) pq = pq.1.toMoorePath.trans pq.2.toMoorePath ⋯

noncomputable def Path.transMoorePathHomotopy {X : Type u_1} [TopologicalSpace X] (x y z : X) : (moorePathTrans x y z).Homotopy (transMoorePath x y z)

The comparison with the unit interval is compatible with concatenation up to homotopy: the homotopy from (p.trans q).toMoorePath to p.toMoorePath.trans q.toMoorePath, continuous in the pair (p, q), which reparametrizes the Moore path of p.trans q from length 1 to length 2.

theorem Path.transMoorePathHomotopy_apply {X : Type u_1} [TopologicalSpace X] {x y z : X} (s : ↑unitInterval) (pq : Path x y × Path y z) : (transMoorePathHomotopy x y z) (s, pq) = (pq.1.trans pq.2).toMoorePath.rescale (1 + unitInterval.toNNReal s)

@[simp]

theorem Path.transMoorePathHomotopy_source {X : Type u_1} [TopologicalSpace X] {x y z : X} (s : ↑unitInterval) (pq : Path x y × Path y z) : ((transMoorePathHomotopy x y z) (s, pq)).source = x

@[simp]

theorem Path.transMoorePathHomotopy_target {X : Type u_1} [TopologicalSpace X] {x y z : X} (s : ↑unitInterval) (pq : Path x y × Path y z) : ((transMoorePathHomotopy x y z) (s, pq)).target = z

Loops

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

The Moore loop of the concatenation of two loops on the unit interval.

@[simp]

theorem Path.mooreLoopTrans_apply {X : Type u_1} [TopologicalSpace X] {x : X} (pq : Path x x × Path x x) : (mooreLoopTrans x) pq = (pq.1.trans pq.2).toMooreLoop

theorem Path.toMoorePath_mul_toMooreLoop {X : Type u_1} [TopologicalSpace X] {x : X} (p q : Path x x) : (p.toMooreLoop * q.toMooreLoop).toMoorePath = p.toMoorePath.trans q.toMoorePath ⋯

The underlying Moore path of a product of Moore loops of two loops on the unit interval.

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

The product of the Moore loops of two loops on the unit interval.

@[simp]

theorem Path.mulMooreLoop_apply {X : Type u_1} [TopologicalSpace X] {x : X} (pq : Path x x × Path x x) : (mulMooreLoop x) pq = pq.1.toMooreLoop * pq.2.toMooreLoop

noncomputable def Path.transMooreLoopHomotopy {X : Type u_1} [TopologicalSpace X] (x : X) : (mooreLoopTrans x).Homotopy (mulMooreLoop x)

Path.toMooreLoop is multiplicative up to homotopy: the homotopy from (p.trans q).toMooreLoop to p.toMooreLoop * q.toMooreLoop, continuous in (p, q).

@[simp]

theorem Path.toMoorePath_transMooreLoopHomotopy {X : Type u_1} [TopologicalSpace X] {x : X} (s : ↑unitInterval) (pq : Path x x × Path x x) : ((transMooreLoopHomotopy x) (s, pq)).toMoorePath = (transMoorePathHomotopy x x x) (s, pq)

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

The concatenation of the loops on the unit interval of two Moore loops.

@[simp]

theorem TauCeti.MooreLoopSpace.transToPath_apply {X : Type u_1} [TopologicalSpace X] {x : X} (γδ : MooreLoopSpace X x × MooreLoopSpace X x) : (transToPath x) γδ = γδ.1.toPath.trans γδ.2.toPath

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

The loop on the unit interval of the product of two Moore loops.

@[simp]

theorem TauCeti.MooreLoopSpace.mulToPath_apply {X : Type u_1} [TopologicalSpace X] {x : X} (γδ : MooreLoopSpace X x × MooreLoopSpace X x) : (mulToPath x) γδ = (γδ.1 * γδ.2).toPath

noncomputable def TauCeti.MooreLoopSpace.mulToPathHomotopy {X : Type u_1} [TopologicalSpace X] (x : X) : (transToPath x).Homotopy (mulToPath x)

MooreLoopSpace.toPath is multiplicative up to homotopy: the homotopy from γ.toPath.trans δ.toPath to (γ * δ).toPath, continuous in (γ, δ). Together with Path.transMooreLoopHomotopy, the homotopy equivalence homotopyEquivPath between the Moore loops and Mathlib's loops is multiplicative up to homotopy in both directions.