Moore paths and the Moore loop space

A Moore path in X is a path of variable duration: a length L ≥ 0 together with a continuous map γ : [0, ∞) → X that is stopped at time L, so γ t = γ L for t ≥ L. Concatenation adds the lengths and runs the second path after the first, with no reparametrization. It is therefore strictly associative, and the paths of length zero are strict units. This is what makes the Moore loops at a point x a monoid on the nose, rather than a monoid up to homotopy as for loops parametrized by the unit interval.

Moore paths carry the topology of a subspace of [0, ∞) × C([0, ∞), X), with the compact-open topology on the second factor. Since [0, ∞) is locally compact, a family of Moore paths is continuous exactly when its lengths and its uncurried paths are (MoorePath.continuous_iff). Concatenation is continuous in this topology (Continuous.moorePath_trans), so the Moore loops at x form a topological monoid MooreLoopSpace X x, functorial in based maps.

A path does not determine its length: the constant path of any length has the same underlying map. So a Moore path is not a bundled function, and equality of Moore paths is checked on the length and on the path (MoorePath.ext).

The Moore loop space need not be homeomorphic to Mathlib's loop space Path x x of loops parametrized by the unit interval: when X is a point, the Moore loops at it form a copy of [0, ∞) (MooreLoopSpace.lengthHomeomorph).

Main definitions

• TauCeti.MoorePath X: Moore paths in X, with length, source and target.
• TauCeti.MoorePath.refl x: the constant path at x of length zero, and TauCeti.MoorePath.constOfLength x L: the constant path at x of length L.
• TauCeti.MoorePath.trans: concatenation of two Moore paths with matching endpoints.
• TauCeti.MoorePath.symm: the reversal of a Moore path.
• TauCeti.MoorePath.rescale γ ℓ: the Moore path γ reparametrized to the length ℓ.
• TauCeti.MoorePath.map: the image of a Moore path under a continuous map.
• TauCeti.MoorePath.pathsBetween A B: the Moore paths from A to B, the path space P_{A→B} X.
• TauCeti.MooreLoopSpace X x: the Moore loops at x, a monoid under concatenation with unit the constant loop of length zero.
• TauCeti.MooreLoopSpace.map: the continuous monoid homomorphism induced by a based map.
• TauCeti.MooreLoopSpace.lengthHom: the length, a continuous monoid homomorphism to [0, ∞), with the constant loops TauCeti.MooreLoopSpace.constOfLengthHom as a section.

Main results

• TauCeti.MoorePath.trans_assoc, TauCeti.MoorePath.refl_trans, TauCeti.MoorePath.trans_refl: concatenation is strictly associative and strictly unital.
• TauCeti.MoorePath.symm_symm, TauCeti.MoorePath.symm_trans: reversal is an involution that reverses concatenations.
• TauCeti.MoorePath.continuous_iff: the characterization of continuous families of Moore paths.
• Continuous.moorePath_trans: concatenation is continuous.
• TauCeti.MoorePath.isClosed_pathsBetween: the paths between closed subsets form a closed subspace.
• TauCeti.MooreLoopSpace.instContinuousMul: the Moore loop space is a topological monoid.
• TauCeti.MooreLoopSpace.lengthHomeomorph: the Moore loop space of a point is [0, ∞).

References

• J. C. Moore, Le théorème de Freudenthal, la suite exacte de James et l'invariant de Hopf généralisé, Séminaire Henri Cartan 7 (1954–1955), exposé 22.
• G. W. Whitehead, Elements of Homotopy Theory, GTM 61, Springer, 1978, 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.

structure TauCeti.MoorePath (X : Type u_1) [TopologicalSpace X] extends C(NNReal, X) : Type u_1

A Moore path in X: a continuous map [0, ∞) → X together with a length L ≥ 0, such that the path is stopped from time L on.

• toFun : NNReal → X
• continuous_toFun : Continuous self.toFun
• length : NNReal

  The length, or duration, of the Moore path.

• apply_of_length_le' (t : NNReal) : self.length ≤ t → self.toFun t = self.toFun self.length

  The path is stopped from time length on.

@[instance_reducible]

instance TauCeti.MoorePath.instCoeFunForallNNReal {X : Type u_1} [TopologicalSpace X] : CoeFun (MoorePath X) fun (x : MoorePath X) => NNReal → X

theorem TauCeti.MoorePath.ext {X : Type u_1} [TopologicalSpace X] {γ₁ γ₂ : MoorePath X} (hL : γ₁.length = γ₂.length) (h : ∀ (t : NNReal), γ₁.toContinuousMap t = γ₂.toContinuousMap t) : γ₁ = γ₂

theorem TauCeti.MoorePath.ext_iff {X : Type u_1} [TopologicalSpace X] {γ₁ γ₂ : MoorePath X} : γ₁ = γ₂ ↔ γ₁.length = γ₂.length ∧ ∀ (t : NNReal), γ₁.toContinuousMap t = γ₂.toContinuousMap t

theorem TauCeti.MoorePath.continuous {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : Continuous ⇑γ.toContinuousMap

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

The starting point of a Moore path.

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

The end point of a Moore path: its value at time length.

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

theorem TauCeti.MoorePath.target_def {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : γ.target = γ.toContinuousMap γ.length

theorem TauCeti.MoorePath.apply_of_length_le {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) {t : NNReal} (ht : γ.length ≤ t) : γ.toContinuousMap t = γ.target

A Moore path is stopped at its target from time length on.

theorem TauCeti.MoorePath.apply_min_length {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (t : NNReal) : γ.toContinuousMap (min t γ.length) = γ.toContinuousMap t

A Moore path only depends on times up to its length.

The topology of Moore paths

@[instance_reducible]

instance TauCeti.MoorePath.instTopologicalSpace {X : Type u_1} [TopologicalSpace X] : TopologicalSpace (MoorePath X)

Moore paths carry the topology induced by the length and the path, as a subspace of [0, ∞) × C([0, ∞), X) with the compact-open topology on the second factor.

theorem TauCeti.MoorePath.isEmbedding_length_toContinuousMap {X : Type u_1} [TopologicalSpace X] : Topology.IsEmbedding fun (γ : MoorePath X) => (γ.length, γ.toContinuousMap)

theorem TauCeti.MoorePath.continuous_length {X : Type u_1} [TopologicalSpace X] : Continuous length

theorem TauCeti.MoorePath.continuous_toContinuousMap {X : Type u_1} [TopologicalSpace X] : Continuous toContinuousMap

theorem TauCeti.MoorePath.continuous_eval {X : Type u_1} [TopologicalSpace X] : Continuous fun (p : MoorePath X × NNReal) => p.1.toContinuousMap p.2

Evaluation of Moore paths is jointly continuous in the path and the time.

theorem Continuous.moorePath_eval {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : Y → TauCeti.MoorePath X} {g : Y → NNReal} (hf : Continuous f) (hg : Continuous g) : Continuous fun (y : Y) => (f y).toContinuousMap (g y)

Evaluation of a continuous family of Moore paths at continuously varying times is continuous.

theorem TauCeti.MoorePath.continuous_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : Y → MoorePath X} : Continuous f ↔ (Continuous fun (y : Y) => (f y).length) ∧ Continuous fun (p : Y × NNReal) => (f p.1).toContinuousMap p.2

A family of Moore paths is continuous exactly when its lengths and its uncurried paths are continuous.

theorem TauCeti.MoorePath.continuous_source {X : Type u_1} [TopologicalSpace X] : Continuous source

theorem TauCeti.MoorePath.continuous_target {X : Type u_1} [TopologicalSpace X] : Continuous target

Constant paths

def TauCeti.MoorePath.refl {X : Type u_1} [TopologicalSpace X] (x : X) : MoorePath X

The constant Moore path at x, of length zero.

@[simp]

theorem TauCeti.MoorePath.refl_apply {X : Type u_1} [TopologicalSpace X] (x : X) (t : NNReal) : (refl x).toContinuousMap t = x

@[simp]

theorem TauCeti.MoorePath.length_refl {X : Type u_1} [TopologicalSpace X] (x : X) : (refl x).length = 0

@[simp]

theorem TauCeti.MoorePath.source_refl {X : Type u_1} [TopologicalSpace X] (x : X) : (refl x).source = x

@[simp]

theorem TauCeti.MoorePath.target_refl {X : Type u_1} [TopologicalSpace X] (x : X) : (refl x).target = x

theorem TauCeti.MoorePath.eq_refl_of_length_eq_zero {X : Type u_1} [TopologicalSpace X] {γ : MoorePath X} (h : γ.length = 0) : γ = refl γ.source

A Moore path of length zero is the constant path at its source.

theorem TauCeti.MoorePath.continuous_refl {X : Type u_1} [TopologicalSpace X] : Continuous refl

def TauCeti.MoorePath.constOfLength {X : Type u_1} [TopologicalSpace X] (x : X) (L : NNReal) : MoorePath X

The constant Moore path at x of length L.

@[simp]

theorem TauCeti.MoorePath.constOfLength_apply {X : Type u_1} [TopologicalSpace X] (x : X) (L t : NNReal) : (constOfLength x L).toContinuousMap t = x

@[simp]

theorem TauCeti.MoorePath.length_constOfLength {X : Type u_1} [TopologicalSpace X] (x : X) (L : NNReal) : (constOfLength x L).length = L

@[simp]

theorem TauCeti.MoorePath.source_constOfLength {X : Type u_1} [TopologicalSpace X] (x : X) (L : NNReal) : (constOfLength x L).source = x

@[simp]

theorem TauCeti.MoorePath.target_constOfLength {X : Type u_1} [TopologicalSpace X] (x : X) (L : NNReal) : (constOfLength x L).target = x

@[simp]

theorem TauCeti.MoorePath.constOfLength_zero {X : Type u_1} [TopologicalSpace X] (x : X) : constOfLength x 0 = refl x

theorem Continuous.moorePath_constOfLength {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : Y → X} {g : Y → NNReal} (hf : Continuous f) (hg : Continuous g) : Continuous fun (y : Y) => TauCeti.MoorePath.constOfLength (f y) (g y)

The constant paths form a continuous family in the point and the length.

Concatenation

noncomputable def TauCeti.MoorePath.trans {X : Type u_1} [TopologicalSpace X] (γ δ : MoorePath X) (h : γ.target = δ.source) : MoorePath X

The concatenation of two Moore paths with γ.target = δ.source: the lengths add, and the path runs through γ and then through δ, with no reparametrization.

theorem TauCeti.MoorePath.trans_apply {X : Type u_1} [TopologicalSpace X] (γ δ : MoorePath X) (h : γ.target = δ.source) (t : NNReal) : (γ.trans δ h).toContinuousMap t = if t ≤ γ.length then γ.toContinuousMap t else δ.toContinuousMap (t - γ.length)

@[simp]

theorem TauCeti.MoorePath.length_trans {X : Type u_1} [TopologicalSpace X] (γ δ : MoorePath X) (h : γ.target = δ.source) : (γ.trans δ h).length = γ.length + δ.length

theorem TauCeti.MoorePath.trans_apply_of_le {X : Type u_1} [TopologicalSpace X] (γ δ : MoorePath X) (h : γ.target = δ.source) {t : NNReal} (ht : t ≤ γ.length) : (γ.trans δ h).toContinuousMap t = γ.toContinuousMap t

theorem TauCeti.MoorePath.trans_apply_of_length_le {X : Type u_1} [TopologicalSpace X] (γ δ : MoorePath X) (h : γ.target = δ.source) {t : NNReal} (ht : γ.length ≤ t) : (γ.trans δ h).toContinuousMap t = δ.toContinuousMap (t - γ.length)

@[simp]

theorem TauCeti.MoorePath.trans_apply_length_add {X : Type u_1} [TopologicalSpace X] (γ δ : MoorePath X) (h : γ.target = δ.source) (t : NNReal) : (γ.trans δ h).toContinuousMap (γ.length + t) = δ.toContinuousMap t

@[simp]

theorem TauCeti.MoorePath.source_trans {X : Type u_1} [TopologicalSpace X] (γ δ : MoorePath X) (h : γ.target = δ.source) : (γ.trans δ h).source = γ.source

@[simp]

theorem TauCeti.MoorePath.target_trans {X : Type u_1} [TopologicalSpace X] (γ δ : MoorePath X) (h : γ.target = δ.source) : (γ.trans δ h).target = δ.target

theorem TauCeti.MoorePath.trans_assoc {X : Type u_1} [TopologicalSpace X] (γ δ ε : MoorePath X) (h₁ : γ.target = δ.source) (h₂ : δ.target = ε.source) : (γ.trans δ h₁).trans ε ⋯ = γ.trans (δ.trans ε h₂) ⋯

Concatenation of Moore paths is strictly associative.

@[simp]

theorem TauCeti.MoorePath.refl_trans {X : Type u_1} [TopologicalSpace X] {x : X} (γ : MoorePath X) (h : (refl x).target = γ.source) : (refl x).trans γ h = γ

The constant path of length zero is a strict left unit for concatenation.

@[simp]

theorem TauCeti.MoorePath.trans_refl {X : Type u_1} [TopologicalSpace X] {y : X} (γ : MoorePath X) (h : γ.target = (refl y).source) : γ.trans (refl y) h = γ

The constant path of length zero is a strict right unit for concatenation.

@[simp]

theorem TauCeti.MoorePath.constOfLength_trans_constOfLength {X : Type u_1} [TopologicalSpace X] (x : X) (L L' : NNReal) : (constOfLength x L).trans (constOfLength x L') ⋯ = constOfLength x (L + L')

Constant paths at a point concatenate by adding their lengths.

theorem TauCeti.MoorePath.trans_constOfLength_target_apply {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (s t : NNReal) : (γ.trans (constOfLength γ.target s) ⋯).toContinuousMap t = γ.toContinuousMap t

Appending a constant path at the target changes only the length.

Reversal

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

The reversal of a Moore path: the same length, run backwards, t ↦ γ (γ.length - t).

@[simp]

theorem TauCeti.MoorePath.symm_apply {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (t : NNReal) : γ.symm.toContinuousMap t = γ.toContinuousMap (γ.length - t)

@[simp]

theorem TauCeti.MoorePath.length_symm {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : γ.symm.length = γ.length

@[simp]

theorem TauCeti.MoorePath.source_symm {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : γ.symm.source = γ.target

@[simp]

theorem TauCeti.MoorePath.target_symm {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : γ.symm.target = γ.source

@[simp]

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

@[simp]

theorem TauCeti.MoorePath.symm_refl {X : Type u_1} [TopologicalSpace X] (x : X) : (refl x).symm = refl x

@[simp]

theorem TauCeti.MoorePath.symm_constOfLength {X : Type u_1} [TopologicalSpace X] (x : X) (L : NNReal) : (constOfLength x L).symm = constOfLength x L

@[simp]

theorem TauCeti.MoorePath.symm_trans {X : Type u_1} [TopologicalSpace X] (γ δ : MoorePath X) (h : γ.target = δ.source) : (γ.trans δ h).symm = δ.symm.trans γ.symm ⋯

Reversal exchanges the order of a concatenation.

theorem Continuous.moorePath_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : Y → TauCeti.MoorePath X} (hf : Continuous f) : Continuous fun (y : Y) => (f y).symm

Reversing a continuous family of Moore paths is continuous.

Reparametrization to a given length

noncomputable def TauCeti.MoorePath.rescale {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (ℓ : NNReal) : MoorePath X

The Moore path γ reparametrized to the length ℓ: the path t ↦ γ (γ.length * t / ℓ). For ℓ = 0 it is the constant path of length zero at the source.

@[simp]

theorem TauCeti.MoorePath.rescale_apply {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (ℓ t : NNReal) : (γ.rescale ℓ).toContinuousMap t = γ.toContinuousMap (γ.length * t / ℓ)

@[simp]

theorem TauCeti.MoorePath.length_rescale {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (ℓ : NNReal) : (γ.rescale ℓ).length = ℓ

@[simp]

theorem TauCeti.MoorePath.source_rescale {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) (ℓ : NNReal) : (γ.rescale ℓ).source = γ.source

theorem TauCeti.MoorePath.target_rescale {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) {ℓ : NNReal} (hℓ : ℓ ≠ 0) : (γ.rescale ℓ).target = γ.target

@[simp]

theorem TauCeti.MoorePath.rescale_length {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : γ.rescale γ.length = γ

Reparametrizing a Moore path to its own length changes nothing.

@[simp]

theorem TauCeti.MoorePath.rescale_rescale {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) {ℓ : NNReal} (hℓ : ℓ ≠ 0) (ℓ' : NNReal) : (γ.rescale ℓ).rescale ℓ' = γ.rescale ℓ'

Rescaling twice is rescaling once to the final length, if the intermediate length is nonzero.

@[simp]

theorem TauCeti.MoorePath.rescale_zero {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : γ.rescale 0 = refl γ.source

theorem Continuous.moorePath_rescale {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : Y → TauCeti.MoorePath X} {g : Y → NNReal} (hf : Continuous f) (hg : Continuous g) (h0 : ∀ (y : Y), g y ≠ 0) : Continuous fun (y : Y) => (f y).rescale (g y)

Rescaling is continuous in the path and in the length, for nonzero lengths.

theorem Continuous.moorePath_trans {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : Y → TauCeti.MoorePath X} (hf : Continuous f) (hg : Continuous g) (h : ∀ (y : Y), (f y).target = (g y).source) : Continuous fun (y : Y) => (f y).trans (g y) ⋯

Concatenation of Moore paths is continuous.

Images under continuous maps

def TauCeti.MoorePath.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (γ : MoorePath X) : MoorePath Y

The image of a Moore path under a continuous map, of the same length.

@[simp]

theorem TauCeti.MoorePath.map_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (γ : MoorePath X) (t : NNReal) : (map f γ).toContinuousMap t = f (γ.toContinuousMap t)

@[simp]

theorem TauCeti.MoorePath.length_map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (γ : MoorePath X) : (map f γ).length = γ.length

@[simp]

theorem TauCeti.MoorePath.source_map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (γ : MoorePath X) : (map f γ).source = f γ.source

@[simp]

theorem TauCeti.MoorePath.target_map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (γ : MoorePath X) : (map f γ).target = f γ.target

@[simp]

theorem TauCeti.MoorePath.map_refl {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (x : X) : map f (refl x) = refl (f x)

@[simp]

theorem TauCeti.MoorePath.map_trans {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (γ δ : MoorePath X) (h : γ.target = δ.source) : map f (γ.trans δ h) = (map f γ).trans (map f δ) ⋯

@[simp]

theorem TauCeti.MoorePath.map_id {X : Type u_1} [TopologicalSpace X] (γ : MoorePath X) : map (ContinuousMap.id X) γ = γ

@[simp]

theorem TauCeti.MoorePath.map_map {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (g : C(Y, Z)) (f : C(X, Y)) (γ : MoorePath X) : map g (map f γ) = map (g.comp f) γ

theorem TauCeti.MoorePath.continuous_map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : Continuous (map f)

Paths between subsets

def TauCeti.MoorePath.pathsBetween {X : Type u_1} [TopologicalSpace X] (A B : Set X) : Set (MoorePath X)

The Moore paths starting in A and ending in B: the path space P_{A→B} X.

@[simp]

theorem TauCeti.MoorePath.mem_pathsBetween {X : Type u_1} [TopologicalSpace X] {A B : Set X} {γ : MoorePath X} : γ ∈ pathsBetween A B ↔ γ.source ∈ A ∧ γ.target ∈ B

def TauCeti.MoorePath.endpointsBetween {X : Type u_1} [TopologicalSpace X] (A B : Set X) : C(↑(pathsBetween A B), ↑A × ↑B)

Endpoint evaluation on the Moore path space, taking values in A × B.

theorem TauCeti.MoorePath.endpointsBetween_apply {X : Type u_1} [TopologicalSpace X] (A B : Set X) (γ : ↑(pathsBetween A B)) : (endpointsBetween A B) γ = (⟨(↑γ).source, ⋯⟩, ⟨(↑γ).target, ⋯⟩)

theorem TauCeti.MoorePath.isClosed_pathsBetween {X : Type u_1} [TopologicalSpace X] {A B : Set X} (hA : IsClosed A) (hB : IsClosed B) : IsClosed (pathsBetween A B)

The paths between two closed subsets form a closed subspace of the Moore paths.

theorem TauCeti.MoorePath.refl_mem_pathsBetween {X : Type u_1} [TopologicalSpace X] {A B : Set X} {x : X} (hA : x ∈ A) (hB : x ∈ B) : refl x ∈ pathsBetween A B

def TauCeti.MoorePath.constantBetween {X : Type u_1} [TopologicalSpace X] (A B : Set X) : C(↑(A ∩ B), ↑(pathsBetween A B))

The constant Moore paths of duration zero, parametrized by A ∩ B.

@[simp]

theorem TauCeti.MoorePath.coe_constantBetween {X : Type u_1} [TopologicalSpace X] (A B : Set X) (x : ↑(A ∩ B)) : ↑((constantBetween A B) x) = refl ↑x

theorem TauCeti.MoorePath.trans_mem_pathsBetween {X : Type u_1} [TopologicalSpace X] {A B : Set X} {γ δ : MoorePath X} (hγ : γ.source ∈ A) (hδ : δ.target ∈ B) (h : γ.target = δ.source) : γ.trans δ h ∈ pathsBetween A B

theorem TauCeti.MoorePath.symm_mem_pathsBetween {X : Type u_1} [TopologicalSpace X] {A B : Set X} {γ : MoorePath X} : γ.symm ∈ pathsBetween B A ↔ γ ∈ pathsBetween A B

theorem TauCeti.MoorePath.map_mem_pathsBetween {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {A B : Set X} {γ : MoorePath X} (f : C(X, Y)) (hγ : γ ∈ pathsBetween A B) : map f γ ∈ pathsBetween (⇑f '' A) (⇑f '' B)

The Moore loop space

structure TauCeti.MooreLoopSpace (X : Type u_1) [TopologicalSpace X] (x : X) : Type u_1

The Moore loop space of X at x: the Moore paths from x to x. Under concatenation it is a monoid with unit the constant loop of length zero, and a topological monoid for the subspace topology.

• toMoorePath : MoorePath X

  The underlying Moore path.

• source_eq : self.toMoorePath.source = x

  The loop starts at x.

• target_eq : self.toMoorePath.target = x

  The loop ends at x.

theorem TauCeti.MooreLoopSpace.toMoorePath_injective {X : Type u_1} [TopologicalSpace X] {x : X} : Function.Injective toMoorePath

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

theorem TauCeti.MooreLoopSpace.ext_iff {X : Type u_1} [TopologicalSpace X] {x : X} {γ δ : MooreLoopSpace X x} : γ = δ ↔ γ.toMoorePath = δ.toMoorePath

@[instance_reducible]

instance TauCeti.MooreLoopSpace.instTopologicalSpace {X : Type u_1} [TopologicalSpace X] {x : X} : TopologicalSpace (MooreLoopSpace X x)

Moore loops carry the subspace topology of the Moore paths.

theorem TauCeti.MooreLoopSpace.isEmbedding_toMoorePath {X : Type u_1} [TopologicalSpace X] {x : X} : Topology.IsEmbedding toMoorePath

theorem TauCeti.MooreLoopSpace.continuous_toMoorePath {X : Type u_1} [TopologicalSpace X] {x : X} : Continuous toMoorePath

@[instance_reducible]

instance TauCeti.MooreLoopSpace.instOne {X : Type u_1} [TopologicalSpace X] {x : X} : One (MooreLoopSpace X x)

@[instance_reducible]

noncomputable instance TauCeti.MooreLoopSpace.instMul {X : Type u_1} [TopologicalSpace X] {x : X} : Mul (MooreLoopSpace X x)

@[simp]

theorem TauCeti.MooreLoopSpace.toMoorePath_one {X : Type u_1} [TopologicalSpace X] {x : X} : toMoorePath 1 = MoorePath.refl x

@[simp]

theorem TauCeti.MooreLoopSpace.toMoorePath_mul {X : Type u_1} [TopologicalSpace X] {x : X} (γ δ : MooreLoopSpace X x) : (γ * δ).toMoorePath = γ.toMoorePath.trans δ.toMoorePath ⋯

@[instance_reducible]

noncomputable instance TauCeti.MooreLoopSpace.instMonoid {X : Type u_1} [TopologicalSpace X] {x : X} : Monoid (MooreLoopSpace X x)

The Moore loops at x form a monoid under concatenation: strict associativity and strict units of Moore paths.

instance TauCeti.MooreLoopSpace.instContinuousMul {X : Type u_1} [TopologicalSpace X] {x : X} : ContinuousMul (MooreLoopSpace X x)

The Moore loop space is a topological monoid.

The length of Moore loops

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

The length of a Moore loop.

@[simp]

theorem TauCeti.MooreLoopSpace.length_toMoorePath {X : Type u_1} [TopologicalSpace X] {x : X} (γ : MooreLoopSpace X x) : γ.toMoorePath.length = γ.length

@[simp]

theorem TauCeti.MooreLoopSpace.length_one {X : Type u_1} [TopologicalSpace X] {x : X} : length 1 = 0

theorem TauCeti.MooreLoopSpace.eq_one_of_length_eq_zero {X : Type u_1} [TopologicalSpace X] {x : X} {γ : MooreLoopSpace X x} (h : γ.length = 0) : γ = 1

A Moore loop of length zero is the unit.

@[simp]

theorem TauCeti.MooreLoopSpace.length_eq_zero_iff {X : Type u_1} [TopologicalSpace X] {x : X} {γ : MooreLoopSpace X x} : γ.length = 0 ↔ γ = 1

@[simp]

theorem TauCeti.MooreLoopSpace.length_mul {X : Type u_1} [TopologicalSpace X] {x : X} (γ δ : MooreLoopSpace X x) : (γ * δ).length = γ.length + δ.length

theorem TauCeti.MooreLoopSpace.continuous_length {X : Type u_1} [TopologicalSpace X] {x : X} : Continuous length

def TauCeti.MooreLoopSpace.lengthHom {X : Type u_1} [TopologicalSpace X] (x : X) : MooreLoopSpace X x →ₜ* Multiplicative NNReal

The length of Moore loops, as a continuous monoid homomorphism to [0, ∞) written multiplicatively.

@[simp]

theorem TauCeti.MooreLoopSpace.lengthHom_apply {X : Type u_1} [TopologicalSpace X] (x : X) (γ : MooreLoopSpace X x) : (lengthHom x) γ = Multiplicative.ofAdd γ.length

def TauCeti.MooreLoopSpace.constOfLength {X : Type u_1} [TopologicalSpace X] (x : X) (L : NNReal) : MooreLoopSpace X x

The constant loop at x of length L.

@[simp]

theorem TauCeti.MooreLoopSpace.toMoorePath_constOfLength {X : Type u_1} [TopologicalSpace X] (x : X) (L : NNReal) : (constOfLength x L).toMoorePath = MoorePath.constOfLength x L

@[simp]

theorem TauCeti.MooreLoopSpace.length_constOfLength {X : Type u_1} [TopologicalSpace X] (x : X) (L : NNReal) : (constOfLength x L).length = L

@[simp]

theorem TauCeti.MooreLoopSpace.constOfLength_zero {X : Type u_1} [TopologicalSpace X] (x : X) : constOfLength x 0 = 1

theorem TauCeti.MooreLoopSpace.constOfLength_add {X : Type u_1} [TopologicalSpace X] (x : X) (L L' : NNReal) : constOfLength x (L + L') = constOfLength x L * constOfLength x L'

The constant loops at x multiply by adding their lengths.

theorem TauCeti.MooreLoopSpace.continuous_constOfLength {X : Type u_1} [TopologicalSpace X] (x : X) : Continuous (constOfLength x)

def TauCeti.MooreLoopSpace.constOfLengthHom {X : Type u_1} [TopologicalSpace X] (x : X) : Multiplicative NNReal →ₜ* MooreLoopSpace X x

The constant loops at x, as a continuous monoid homomorphism from [0, ∞) written multiplicatively; it is a section of lengthHom.

@[simp]

theorem TauCeti.MooreLoopSpace.constOfLengthHom_apply {X : Type u_1} [TopologicalSpace X] (x : X) (L : Multiplicative NNReal) : (constOfLengthHom x) L = constOfLength x (Multiplicative.toAdd L)

theorem TauCeti.MooreLoopSpace.lengthHom_comp_constOfLengthHom {X : Type u_1} [TopologicalSpace X] (x : X) : (lengthHom x).comp (constOfLengthHom x) = ContinuousMonoidHom.id (Multiplicative NNReal)

def TauCeti.MooreLoopSpace.lengthHomeomorph {X : Type u_1} [TopologicalSpace X] (x : X) [Subsingleton X] : MooreLoopSpace X x ≃ₜ NNReal

When X is a point, the length is a homeomorphism MooreLoopSpace X x ≃ₜ [0, ∞): the Moore loop space of a point is [0, ∞), not a point.

@[simp]

theorem TauCeti.MooreLoopSpace.lengthHomeomorph_apply {X : Type u_1} [TopologicalSpace X] (x : X) [Subsingleton X] (γ : MooreLoopSpace X x) : (lengthHomeomorph x) γ = γ.length

@[simp]

theorem TauCeti.MooreLoopSpace.lengthHomeomorph_symm_apply {X : Type u_1} [TopologicalSpace X] (x : X) [Subsingleton X] (L : NNReal) : (lengthHomeomorph x).symm L = constOfLength x L

def TauCeti.MooreLoopSpace.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (f : C(X, Y)) (hf : f x = y) : MooreLoopSpace X x →ₜ* MooreLoopSpace Y y

The continuous monoid homomorphism of Moore loop spaces induced by a based map.

@[simp]

theorem TauCeti.MooreLoopSpace.toMoorePath_map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (f : C(X, Y)) (hf : f x = y) (γ : MooreLoopSpace X x) : ((map f hf) γ).toMoorePath = MoorePath.map f γ.toMoorePath

@[simp]

theorem TauCeti.MooreLoopSpace.length_map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (f : C(X, Y)) (hf : f x = y) (γ : MooreLoopSpace X x) : ((map f hf) γ).length = γ.length

@[simp]

theorem TauCeti.MooreLoopSpace.map_id {X : Type u_1} [TopologicalSpace X] {x : X} : map (ContinuousMap.id X) ⋯ = ContinuousMonoidHom.id (MooreLoopSpace X x)

theorem TauCeti.MooreLoopSpace.map_comp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} {Z : Type u_3} [TopologicalSpace Z] {z : Z} (g : C(Y, Z)) (f : C(X, Y)) (hg : g y = z) (hf : f x = y) : map (g.comp f) ⋯ = (map g hg).comp (map f hf)