Tube neighborhoods in path space

A tube in the space of paths in X is determined by a partition 0 = t₀ ≤ ⋯ ≤ tₙ = 1 of the unit interval, open sets Uᵢ for the segments [tᵢ, tᵢ₊₁], and open path-connected sets Vⱼ for the vertices tⱼ, each contained in the adjacent segment sets. A path lies in the tube if it maps each segment into Uᵢ and each vertex into Vⱼ. Tubes are open in the compact-open topology. When each Uᵢ is path-homotopy-trivial (IsPathHomotopyTrivial), two paths with the same endpoints in a common tube are homotopic: connect corresponding vertices by paths in Vⱼ, use homotopy triviality of Uᵢ on each rectangle, and paste (Path.Homotopic.trans_of_subpath_trans).

Main definitions

• Path.Tube X n: the segment sets Uᵢ and vertex sets Vⱼ of a tube, with their properties.
• Path.IsInTube f part T: the predicate that f : I → X lies in the tube.

Main statements

• Path.exists_isInTube: in a locally path-connected space, a path lies in a tube if each point on it has an open, path-homotopy-trivial neighborhood.
• unitInterval.Partition.isOpen_setOf_mapsTo_Icc_and_mem: the maps sending the segments and vertices of a partition into given open sets form an open set in the compact-open topology.
• Path.Tube.isOpen_setOf_isInTube: hence tubes are open.
• Path.IsInTube.exists_trans_homotopic: two paths with the same source in a common tube become homotopic after appending to the first a path in the last vertex set.
• Path.IsInTube.homotopic: two paths with the same endpoints in a common tube are homotopic.

The application to semilocally simply connected spaces (path-homotopy classes are open, so Path.Homotopic.Quotient is discrete) is in TauCeti/AlgebraicTopology/SemilocallySimplyConnected/On.lean.

structure Path.Tube (X : Type u_2) [TopologicalSpace X] (n : ℕ) : Type u_2

The data of a tube with n segments: open path-homotopy-trivial sets U i for the segments, and open path-connected sets V j for the vertices, with V j contained in the U i of the adjacent segments.

• U : Fin n → Set X

  The segment sets.

• V : Fin (n + 1) → Set X

  The vertex sets.

• isOpen_U (i : Fin n) : IsOpen (self.U i)

  Each segment set is open.

• isPathHomotopyTrivial_U (i : Fin n) : IsPathHomotopyTrivial (self.U i)

  Each segment set is path-homotopy-trivial.

• isOpen_V (j : Fin (n + 1)) : IsOpen (self.V j)

  Each vertex set is open.

• isPathConnected_V (j : Fin (n + 1)) : IsPathConnected (self.V j)

  Each vertex set is path-connected.

• V_castSucc_subset (i : Fin n) : self.V i.castSucc ⊆ self.U i

  The vertex set at the start of a segment lies in that segment's set.

• V_succ_subset (i : Fin n) : self.V i.succ ⊆ self.U i

  The vertex set at the end of a segment lies in that segment's set.

structure Path.IsInTube {X : Type u_1} [TopologicalSpace X] {n : ℕ} (f : ↑unitInterval → X) (part : unitInterval.Partition n) (T : Tube X n) : Prop

f : I → X lies in the tube determined by part and T if it maps each segment [tᵢ, tᵢ₊₁] into U i and each vertex tⱼ into V j.

• mapsTo (i : Fin n) : Set.MapsTo f (Set.Icc (part.t i.castSucc) (part.t i.succ)) (T.U i)

  Each segment is mapped into its segment set.

• mem_V (j : Fin (n + 1)) : f (part.t j) ∈ T.V j

  Each vertex is mapped into its vertex set.

@[simp]

theorem Path.isInTube_iff {X : Type u_1} [TopologicalSpace X] {n : ℕ} {part : unitInterval.Partition n} {T : Tube X n} {f : ↑unitInterval → X} : IsInTube f part T ↔ (∀ (i : Fin n), Set.MapsTo f (Set.Icc (part.t i.castSucc) (part.t i.succ)) (T.U i)) ∧ ∀ (j : Fin (n + 1)), f (part.t j) ∈ T.V j

Unbundled form of Path.IsInTube.

theorem Path.IsInTube.range_subpath_subset {X : Type u_1} [TopologicalSpace X] {n : ℕ} {part : unitInterval.Partition n} {T : Tube X n} {x y : X} {γ : Path x y} (hγ : IsInTube (⇑γ) part T) (i : Fin n) : Set.range ⇑(γ.subpath (part.t i.castSucc) (part.t i.succ)) ⊆ T.U i

A path in a tube has each of its segment subpaths inside the corresponding segment set.

Openness of tubes

theorem unitInterval.Partition.isOpen_setOf_mapsTo_Icc_and_mem {X : Type u_1} [TopologicalSpace X] {n : ℕ} (part : Partition n) {U : Fin n → Set X} {V : Fin (n + 1) → Set X} (hU : ∀ (i : Fin n), IsOpen (U i)) (hV : ∀ (j : Fin (n + 1)), IsOpen (V j)) : IsOpen {f : C(↑unitInterval, X) | (∀ (i : Fin n), Set.MapsTo (⇑f) (Set.Icc (part.t i.castSucc) (part.t i.succ)) (U i)) ∧ ∀ (j : Fin (n + 1)), f (part.t j) ∈ V j}

The maps f : C(I, X) sending each segment [tᵢ, tᵢ₊₁] of a partition into an open set U i and each vertex tⱼ into an open set V j form an open set in the compact-open topology.

theorem Path.Tube.isOpen_setOf_isInTube {X : Type u_1} [TopologicalSpace X] {n : ℕ} (part : unitInterval.Partition n) (T : Tube X n) : IsOpen {f : C(↑unitInterval, X) | IsInTube (⇑f) part T}

A tube is open in the compact-open topology on C(I, X).

theorem Path.Tube.isOpen_setOf_isInTube_path {X : Type u_1} [TopologicalSpace X] {n : ℕ} (part : unitInterval.Partition n) (T : Tube X n) (x y : X) : IsOpen {γ : Path x y | IsInTube (⇑γ) part T}

A tube is open in the path space Path x y.

Existence of tubes

theorem Path.exists_isInTube {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] {x y : X} (γ : Path x y) (h : ∀ z ∈ Set.range ⇑γ, ∃ (U : Set X), IsOpen U ∧ z ∈ U ∧ IsPathHomotopyTrivial U) : ∃ (n : ℕ) (part : unitInterval.Partition n) (T : Tube X n), IsInTube (⇑γ) part T

If every point on a path has an open, path-homotopy-trivial neighborhood, then the path lies in a tube.

Paths in a common tube are homotopic

theorem Path.IsInTube.exists_trans_homotopic {X : Type u_1} [TopologicalSpace X] {n : ℕ} {part : unitInterval.Partition n} {T : Tube X n} {x y y' : X} {γ : Path x y} {γ' : Path x y'} (hγ : IsInTube (⇑γ) part T) (hγ' : IsInTube (⇑γ') part T) : ∃ (ρ : Path y y'), Set.range ⇑ρ ⊆ T.V (Fin.last n) ∧ (γ.trans ρ).Homotopic γ'

Two paths with the same source in a common tube are homotopic after appending to the first a path in the last vertex set of the tube.

theorem Path.IsInTube.homotopic {X : Type u_1} [TopologicalSpace X] {n : ℕ} {part : unitInterval.Partition n} {T : Tube X n} {x y : X} {γ γ' : Path x y} (hγ : IsInTube (⇑γ) part T) (hγ' : IsInTube (⇑γ') part T) : γ.Homotopic γ'

Two paths with the same endpoints in a common tube are homotopic.