Subpaths and concatenation of paths

This file defines Path.subpath as a restriction of a path to a subinterval, reparameterized to have domain [0, 1] and possibly with a reverse of direction. It then defines Path.concat as a way to concatenate finite sequences of paths with compatible endpoints.

The main result Path.Homotopy.concatSubpath shows that subpaths concatenate nicely. In particular: following the subpaths of γ from t i to t (i + 1) for 0 ≤ i < n is homotopic to the subpath of γ from t 0 to t n.

TODO

Prove that Path.truncateOfLE and Path.subpath are reparameterizations of each other. (Path.subpath is still a useful definition because it works without assuming an order on t₀ and t₁, and is convenient for concrete manipulations.)

Subpaths

@[deprecated Set.Icc.convexComb (since := "2026-03-20")]

def Path.subpathAux {a b : ℝ} (x y : ↑(Set.Icc a b)) (t : ↑unitInterval) : ↑(Set.Icc a b)

Alias of Set.Icc.convexComb.

Equations

• @Path.subpathAux = @Set.Icc.convexComb

@[deprecated Set.Icc.convexComb_zero (since := "2026-03-20")]

theorem Path.subpathAux_zero {a b : ℝ} (x y : ↑(Set.Icc a b)) : Set.Icc.convexComb x y 0 = x

Alias of Set.Icc.convexComb_zero.

@[deprecated Set.Icc.convexComb_one (since := "2026-03-20")]

theorem Path.subpathAux_one {a b : ℝ} (x y : ↑(Set.Icc a b)) : Set.Icc.convexComb x y 1 = y

Alias of Set.Icc.convexComb_one.

@[deprecated Set.Icc.continuous_convexComb_prod (since := "2026-03-20")]

theorem Path.subpathAux_continuous {a b : ℝ} : Continuous fun (x : ↑(Set.Icc a b) × ↑(Set.Icc a b) × ↑unitInterval) => Set.Icc.convexComb x.1 x.2.1 x.2.2

Alias of Set.Icc.continuous_convexComb_prod.

def Path.subpath {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ : ↑unitInterval) : Path (γ t₀) (γ t₁)

The subpath of γ from t₀ to t₁.

Equations

• γ.subpath t₀ t₁ = { toFun := ⇑γ ∘ Set.Icc.convexComb t₀ t₁, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

@[simp]

theorem Path.symm_subpath {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ : ↑unitInterval) : (γ.subpath t₀ t₁).symm = γ.subpath t₁ t₀

Reversing γ.subpath t₀ t₁ results in γ.subpath t₁ t₀.

theorem Path.range_subpathAux (t₀ t₁ : ↑unitInterval) : Set.range (Set.Icc.convexComb t₀ t₁) = Set.uIcc t₀ t₁

@[simp]

theorem Path.range_subpath {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ : ↑unitInterval) : Set.range ⇑(γ.subpath t₀ t₁) = ⇑γ '' Set.uIcc t₀ t₁

The range of a subpath is the image of the original path on the relevant interval.

theorem Path.range_subpath_of_le {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ : ↑unitInterval) (h : t₀ ≤ t₁) : Set.range ⇑(γ.subpath t₀ t₁) = ⇑γ '' Set.Icc t₀ t₁

theorem Path.range_subpath_of_ge {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ : ↑unitInterval) (h : t₁ ≤ t₀) : Set.range ⇑(γ.subpath t₀ t₁) = ⇑γ '' Set.Icc t₁ t₀

@[simp]

theorem Path.subpath_self {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) (t : ↑unitInterval) : γ.subpath t t = refl (γ t)

The subpath of γ from t to t is just the constant path at γ t.

@[simp]

theorem Path.subpath_zero_one {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) : γ.subpath 0 1 = γ.cast ⋯ ⋯

The subpath of γ from 0 to 1 is just γ, with a slightly different type.

theorem Path.subpath_continuous_family {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) : Continuous fun (x : ↑unitInterval × ↑unitInterval × ↑unitInterval) => (γ.subpath x.1 x.2.1) x.2.2

For a path γ, γ.subpath gives a "continuous family of paths", by which we mean the uncurried function which maps (t₀, t₁, s) to γ.subpath t₀ t₁ s is continuous.

noncomputable def Path.Homotopy.subpathTransSubpathRefl {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ t₂ : ↑unitInterval) : ((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂)).Homotopy ((γ.subpath t₀ t₂).trans (Path.refl (γ t₂)))

Auxiliary homotopy for Path.Homotopy.subpathTransSubpath which includes an unnecessary copy of Path.refl.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Path.Homotopy.subpathTransSubpath {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ t₂ : ↑unitInterval) : ((γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂)).Homotopy (γ.subpath t₀ t₂)

Following the subpath of γ from t₀ to t₁, and then that from t₁ to t₂, is in natural homotopy with following the subpath of γ from t₀ to t₂.

Equations

• Path.Homotopy.subpathTransSubpath γ t₀ t₁ t₂ = (Path.Homotopy.subpathTransSubpathRefl γ t₀ t₁ t₂).trans (Path.Homotopy.transRefl (γ.subpath t₀ t₂))

Concatenation of paths

noncomputable def Path.concat {X : Type u_1} [TopologicalSpace X] {n : ℕ} (p : Fin (n + 1) → X) (F : (k : Fin n) → Path (p k.castSucc) (p k.succ)) : Path (p 0) (p (Fin.last n))

Concatenation of a sequence of paths with compatible endpoints.

Equations

• Path.concat p F = Fin.dfoldl n (fun (i : Fin (n + 1)) => Path (p 0) (p i)) (fun (i : Fin n) (ih : Path (p 0) (p i.castSucc)) => ih.trans (F i)) (Path.refl (p 0))

@[simp]

theorem Path.concat_zero {X : Type u_1} [TopologicalSpace X] (p : Fin 1 → X) (F : (k : Fin 0) → Path (p k.castSucc) (p k.succ)) : concat p F = refl (p 0)

Concatenating zero paths yields the constant path (the identity of Path.trans).

theorem Path.concat_succ {X : Type u_1} [TopologicalSpace X] {n : ℕ} (p : Fin (n + 2) → X) (F : (k : Fin (n + 1)) → Path (p k.castSucc) (p k.succ)) : concat p F = (concat (p ∘ Fin.castSucc) fun (k : Fin n) => F k.castSucc).trans (F (Fin.last n))

Concatenating n + 1 paths corresponds to concatenating n paths and then the last path.

@[simp]

theorem Path.concat_refl {X : Type u_1} [TopologicalSpace X] (n : ℕ) (x : X) : (concat (fun (x_1 : Fin (n + 1)) => x) fun (x_1 : Fin n) => refl x) = refl x

Concatenating the constant path at x with itself just yields the constant path at x.

noncomputable def Path.Homotopy.concat {X : Type u_1} [TopologicalSpace X] {n : ℕ} (p : Fin (n + 1) → X) (F G : (k : Fin n) → Path (p k.castSucc) (p k.succ)) (H : (k : Fin n) → (F k).Homotopy (G k)) : (concat p F).Homotopy (concat p G)

Given two sequences of paths F and G, and a sequence H of homotopies between them, there is a natural homotopy between concat _ F and concat _ G.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Path.Homotopy.concatSubpath {X : Type u_1} [TopologicalSpace X] {a b : X} {n : ℕ} (γ : Path a b) (t : Fin (n + 1) → ↑unitInterval) : (concat (⇑γ ∘ t) fun (k : Fin n) => γ.subpath (t k.castSucc) (t k.succ)).Homotopy (γ.subpath (t 0) (t (Fin.last n)))

Given a path γ and a sequence t of n + 1 points in [0, 1], there is a natural homotopy between the concatenation of paths γ.subpath (t k) (t (k + 1)), and γ.subpath (t 0) (t n).

Equations

• One or more equations did not get rendered due to their size.

theorem Path.Homotopic.concat_one {X : Type u_1} [TopologicalSpace X] (p : Fin 2 → X) (F : (k : Fin 1) → Path (p k.castSucc) (p k.succ)) : (concat p F).Homotopic (F 0)

Concatenating one path F 0 is homotopic to that path.

theorem Path.Homotopic.concat_two {X : Type u_1} [TopologicalSpace X] (p : Fin 3 → X) (F : (k : Fin 2) → Path (p k.castSucc) (p k.succ)) : (concat p F).Homotopic ((F 0).trans (F 1))

Concatenating two paths F 0 and F 1 is homotopic to Path.trans (F 0) (F 1).

theorem Path.Homotopic.concat_hcomp {X : Type u_1} [TopologicalSpace X] {n : ℕ} (p : Fin (n + 1) → X) (F G : (k : Fin n) → Path (p k.castSucc) (p k.succ)) (h : ∀ (k : Fin n), (F k).Homotopic (G k)) : (concat p F).Homotopic (concat p G)

Alternative to Path.Homotopy.concatHcomp in terms of Path.Homotopic.

@[simp]

theorem Path.Homotopic.concat_subpath {X : Type u_1} [TopologicalSpace X] {a b : X} {n : ℕ} (γ : Path a b) (t : Fin (n + 1) → ↑unitInterval) : (concat (⇑γ ∘ t) fun (k : Fin n) => γ.subpath (t k.castSucc) (t k.succ)).Homotopic (γ.subpath (t 0) (t (Fin.last n)))

Alternative to Path.Homotopy.concatSubpath in terms of Path.Homotopic.

@[simp]

theorem Path.Homotopic.subpath_trans_subpath {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) (s t u : ↑unitInterval) : ((γ.subpath s t).trans (γ.subpath t u)).Homotopic (γ.subpath s u)

Two consecutive subpaths are homotopic to the subpath between their outer endpoints.

@[simp]

theorem Path.Homotopic.mk_subpath_trans_mk_subpath {X : Type u_1} [TopologicalSpace X] {a b : X} (γ : Path a b) (s t u : ↑unitInterval) : (Quotient.mk (γ.subpath s t)).trans (Quotient.mk (γ.subpath t u)) = Quotient.mk (γ.subpath s u)

Composition of consecutive subpath classes is the class of the subpath between their outer endpoints.