Subpaths

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.

The main result Path.Homotopy.subpathTransSubpath shows that subpaths concatenate nicely. In particular: 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₂.

Path.subpath is similar in behavior to Path.truncate. When t₀ ≤ t₁, they are reparameterizations of each other (not yet proven). However, Path.subpath works without assuming an order on t₀ and t₁, and is convenient for concrete manipulations (e.g., Path.Homotopy.subpathTransSubpath).

TODO

Prove that Path.truncateOfLE and Path.subpath are reparameterizations of each other.

def Path.subpathAux (t₀ t₁ s : ↑unitInterval) : ↑unitInterval

Auxillary function for defining subpaths.

Equations

• Path.subpathAux t₀ t₁ s = ⟨(1 - ↑s) * ↑t₀ + ↑s * ↑t₁, ⋯⟩

theorem Path.subpathAux_zero (t₀ t₁ : ↑unitInterval) : subpathAux t₀ t₁ 0 = t₀

theorem Path.subpathAux_one (t₀ t₁ : ↑unitInterval) : subpathAux t₀ t₁ 1 = t₁

theorem Path.subpathAux_continuous : Continuous fun (x : ↑unitInterval × ↑unitInterval × ↑unitInterval) => subpathAux x.1 x.2.1 x.2.2

subpathAux is continuous as an uncurried function I × I × I → I.

def Path.subpath {X : Type u} [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 := ⇑γ ∘ Path.subpathAux t₀ t₁, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

@[simp]

theorem Path.symm_subpath {X : Type u} [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 (subpathAux t₀ t₁) = Set.uIcc t₀ t₁

@[simp]

theorem Path.range_subpath {X : Type u} [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} [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} [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} [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} [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} [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.

def Path.Homotopy.subpathTransSubpathRefl {X : Type u} [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₂)))

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

def Path.Homotopy.subpathTransSubpath {X : Type u} [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₂))