Moore paths between two points

Moore paths from a to b form a space with a left action of the Moore loops at a and a right action of the Moore loops at b, both given by concatenation. The actions are continuous, strictly associative and unital, and commute. This topological bimodule is the input for the chain bimodule that transports DG local systems between basepoints.

Reversal exchanges the endpoints, and concatenation joins paths with matching endpoints. Paths with equal specified endpoints are homeomorphic to the Moore loop space.

The right action is represented by an action of the opposite monoid, following the convention for right DG modules. A Moore path retains its duration, including when its underlying map is constant.

References

• 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.

@[reducible, inline]

abbrev TauCeti.MoorePathBetween (X : Type u_2) [TopologicalSpace X] (a b : X) : Type u_2

The space of Moore paths from a to b, with the subspace topology of all Moore paths.

def TauCeti.MoorePathBetween.toMoorePath {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePathBetween X a b) : MoorePath X

The underlying Moore path.

@[simp]

theorem TauCeti.MoorePathBetween.toMoorePath_mk {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePath X) (h : γ.source = a ∧ γ.target = b) : toMoorePath ⟨γ, h⟩ = γ

theorem TauCeti.MoorePathBetween.ext {X : Type u_1} [TopologicalSpace X] {a b : X} {γ δ : MoorePathBetween X a b} (h : γ.toMoorePath = δ.toMoorePath) : γ = δ

theorem TauCeti.MoorePathBetween.ext_iff {X : Type u_1} [TopologicalSpace X] {a b : X} {γ δ : MoorePathBetween X a b} : γ = δ ↔ γ.toMoorePath = δ.toMoorePath

@[simp]

theorem TauCeti.MoorePathBetween.source {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePathBetween X a b) : γ.toMoorePath.source = a

@[simp]

theorem TauCeti.MoorePathBetween.target {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePathBetween X a b) : γ.toMoorePath.target = b

theorem TauCeti.MoorePathBetween.continuous_toMoorePath {X : Type u_1} [TopologicalSpace X] {a b : X} : Continuous toMoorePath

def TauCeti.MoorePathBetween.symm {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePathBetween X a b) : MoorePathBetween X b a

Reverse a Moore path with specified endpoints.

@[simp]

theorem TauCeti.MoorePathBetween.toMoorePath_symm {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePathBetween X a b) : γ.symm.toMoorePath = γ.toMoorePath.symm

@[simp]

theorem TauCeti.MoorePathBetween.symm_symm {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePathBetween X a b) : γ.symm.symm = γ

theorem TauCeti.MoorePathBetween.continuous_symm {X : Type u_1} [TopologicalSpace X] {a b : X} : Continuous symm

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

Concatenate Moore paths with specified endpoints.

@[simp]

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

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

Concatenation remains strictly associative on endpoint-constrained path spaces.

@[simp]

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

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

Concatenation is jointly continuous on the endpoint-constrained spaces.

def TauCeti.MoorePathBetween.loopHomeomorph {X : Type u_1} [TopologicalSpace X] (x : X) : MooreLoopSpace X x ≃ₜ MoorePathBetween X x x

Moore loops are precisely the Moore paths with equal specified endpoints.

@[simp]

theorem TauCeti.MoorePathBetween.toMoorePath_loopHomeomorph {X : Type u_1} [TopologicalSpace X] {b : X} (ω : MooreLoopSpace X b) : ((loopHomeomorph b) ω).toMoorePath = ω.toMoorePath

@[simp]

theorem TauCeti.MoorePathBetween.toMoorePath_loopHomeomorph_symm {X : Type u_1} [TopologicalSpace X] {b : X} (γ : MoorePathBetween X b b) : ((loopHomeomorph b).symm γ).toMoorePath = γ.toMoorePath

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

Concatenate a loop at a in front of a path from a to b.

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

Concatenate a loop at b after a path from a to b.

@[simp]

theorem TauCeti.MoorePathBetween.toMoorePath_leftAct {X : Type u_1} [TopologicalSpace X] {a b : X} (ω : MooreLoopSpace X a) (γ : MoorePathBetween X a b) : (leftAct ω γ).toMoorePath = ω.toMoorePath.trans γ.toMoorePath ⋯

@[simp]

theorem TauCeti.MoorePathBetween.toMoorePath_rightAct {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePathBetween X a b) (ω : MooreLoopSpace X b) : (γ.rightAct ω).toMoorePath = γ.toMoorePath.trans ω.toMoorePath ⋯

@[simp]

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

@[simp]

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

@[simp]

theorem TauCeti.MoorePathBetween.leftAct_mul {X : Type u_1} [TopologicalSpace X] {a b : X} (ω ω' : MooreLoopSpace X a) (γ : MoorePathBetween X a b) : leftAct (ω * ω') γ = leftAct ω (leftAct ω' γ)

@[simp]

theorem TauCeti.MoorePathBetween.rightAct_mul {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : MoorePathBetween X a b) (ω ω' : MooreLoopSpace X b) : γ.rightAct (ω * ω') = (γ.rightAct ω).rightAct ω'

theorem TauCeti.MoorePathBetween.leftAct_rightAct {X : Type u_1} [TopologicalSpace X] {a b : X} (ω : MooreLoopSpace X a) (γ : MoorePathBetween X a b) (η : MooreLoopSpace X b) : leftAct ω (γ.rightAct η) = (leftAct ω γ).rightAct η

Concatenating at the source commutes with concatenating at the target.

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

The left loop action is jointly continuous.

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

The right loop action is jointly continuous.

@[instance_reducible]

noncomputable instance TauCeti.MoorePathBetween.instMulActionMooreLoopSpace {X : Type u_1} [TopologicalSpace X] {a b : X} : MulAction (MooreLoopSpace X a) (MoorePathBetween X a b)

The action of loops at the starting point.

@[instance_reducible]

noncomputable instance TauCeti.MoorePathBetween.instMulActionMulOppositeMooreLoopSpace {X : Type u_1} [TopologicalSpace X] {a b : X} : MulAction (MooreLoopSpace X b)ᵐᵒᵖ (MoorePathBetween X a b)

The right action of loops at the ending point, viewed as an action of the opposite monoid.

@[simp]

theorem TauCeti.MoorePathBetween.smul_eq_leftAct {X : Type u_1} [TopologicalSpace X] {a b : X} (ω : MooreLoopSpace X a) (γ : MoorePathBetween X a b) : ω • γ = leftAct ω γ

@[simp]

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

instance TauCeti.MoorePathBetween.instSMulCommClassMooreLoopSpaceMulOpposite {X : Type u_1} [TopologicalSpace X] {a b : X} : SMulCommClass (MooreLoopSpace X a) (MooreLoopSpace X b)ᵐᵒᵖ (MoorePathBetween X a b)

The two loop actions commute.

instance TauCeti.MoorePathBetween.instContinuousSMulMooreLoopSpace {X : Type u_1} [TopologicalSpace X] {a b : X} : ContinuousSMul (MooreLoopSpace X a) (MoorePathBetween X a b)

instance TauCeti.MoorePathBetween.instContinuousSMulMulOppositeMooreLoopSpace {X : Type u_1} [TopologicalSpace X] {a b : X} : ContinuousSMul (MooreLoopSpace X b)ᵐᵒᵖ (MoorePathBetween X a b)