Based paths

For a topological space X and a basepoint x₀ : X, this file introduces the space BasedPath x₀ of continuous maps γ : C(I, X) with γ 0 = x₀, topologized as a subspace of C(I, X) with the compact-open topology. Its quotient by endpoint-preserving homotopy is the model TauCeti.UniversalCover x₀ used to construct the universal cover. When X is locally path-connected and semilocally simply connected, that quotient is simply connected and its endpoint projection is a covering map whose range is the path component of x₀ (TauCeti/AlgebraicTopology/UniversalCover/Covering.lean); it is then a universal cover of that path component, and of X when X is path-connected. This file is adapted from #38292 by Kim Morrison.

The main results concern the path components of endpoint ⁻¹' U. For sufficiently small open sets U, their images in the universal cover are the sheets over U.

Main definitions

• BasedPath x₀: the space of based paths out of x₀.
• BasedPath.deformTerminal: modify a based path near its endpoint by a short path, without moving far in the compact-open topology.
• BasedPath.initialSegmentFamily: the family t ↦ γ|_[0, t] of initial segments.

Main statements

• BasedPath.isOpenMap_endpoint: the endpoint map BasedPath x₀ → X is open when X is locally path-connected.
• BasedPath.joinedIn_preimage_of_append: appending a path inside U stays in the same path component of endpoint ⁻¹' U.
• BasedPath.isOpen_pathComponent_preimage: in a semilocally simply connected, locally path-connected space, path components of endpoint ⁻¹' U are open for open U.
• BasedPath.toPath_homotopic_of_joinedIn_pathHomotopyTrivial: based paths with the same endpoint in a common path component of endpoint ⁻¹' U, for U path-homotopy-trivial, are homotopic.
• BasedPath.pathComponentIn_ofPath_eq_of_homotopic: path components of endpoint ⁻¹' U are invariant under endpoint-preserving homotopy.

def BasedPath {X : Type u_1} [TopologicalSpace X] (x₀ : X) : Type u_1

The compact-open based-path space out of x₀.

Equations

• BasedPath x₀ = { γ : C(↑unitInterval, X) // γ 0 = x₀ }

@[instance_reducible]

instance BasedPath.instTopologicalSpace {X : Type u_1} [TopologicalSpace X] {x₀ : X} : TopologicalSpace (BasedPath x₀)

Equations

• BasedPath.instTopologicalSpace = { IsOpen := BasedPath.instTopologicalSpace._aux_1, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

@[instance_reducible]

instance BasedPath.instFunLikeElemRealUnitInterval {X : Type u_1} [TopologicalSpace X] {x₀ : X} : FunLike (BasedPath x₀) (↑unitInterval) X

Equations

• BasedPath.instFunLikeElemRealUnitInterval = { coe := fun (γ : BasedPath x₀) => ⇑↑γ, coe_injective := ⋯ }

instance BasedPath.instContinuousEvalElemRealUnitInterval {X : Type u_1} [TopologicalSpace X] {x₀ : X} : ContinuousEval (BasedPath x₀) (↑unitInterval) X

Evaluation BasedPath x₀ × I → X is jointly continuous.

@[simp]

theorem BasedPath.mk_apply {X : Type u_1} [TopologicalSpace X] {x₀ : X} (γ : C(↑unitInterval, X)) (h : γ 0 = x₀) (t : ↑unitInterval) : (have this := ⟨γ, h⟩; this) t = γ t

@[simp]

theorem BasedPath.val_apply {X : Type u_1} [TopologicalSpace X] {x₀ : X} (γ : BasedPath x₀) (t : ↑unitInterval) : ↑γ t = γ t

theorem BasedPath.continuous_iff {X : Type u_1} [TopologicalSpace X] {x₀ : X} {Y : Type u_2} [TopologicalSpace Y] {f : Y → BasedPath x₀} : Continuous f ↔ Continuous fun (p : Y × ↑unitInterval) => (f p.1) p.2

A map into BasedPath x₀ is continuous iff its uncurried form is.

@[simp]

theorem BasedPath.source {X : Type u_1} [TopologicalSpace X] {x₀ : X} (γ : BasedPath x₀) : γ 0 = x₀

def BasedPath.endpoint {X : Type u_1} [TopologicalSpace X] {x₀ : X} (γ : BasedPath x₀) : X

The endpoint of a based path.

Equations

• γ.endpoint = γ 1

theorem BasedPath.continuous_endpoint {X : Type u_1} [TopologicalSpace X] {x₀ : X} : Continuous endpoint

The endpoint map from based paths to their terminal point is continuous.

def BasedPath.toPath {X : Type u_1} [TopologicalSpace X] {x₀ : X} (γ : BasedPath x₀) : Path x₀ γ.endpoint

View a based path as a path to its endpoint.

Equations

• γ.toPath = { toContinuousMap := ↑γ, source' := ⋯, target' := ⋯ }

theorem BasedPath.endpoint_def {X : Type u_1} [TopologicalSpace X] {x₀ : X} (γ : BasedPath x₀) : γ.endpoint = γ 1

Definitional unfolding of endpoint. Not a global simp lemma: it overlaps with endpoint_refl (and other endpoint_… lemmas) on the simp normal form, so we instead include it explicitly at each site that wants to pass from the named endpoint γ to the evaluation γ 1.

@[simp]

theorem BasedPath.toPath_apply {X : Type u_1} [TopologicalSpace X] {x₀ : X} (γ : BasedPath x₀) (t : ↑unitInterval) : γ.toPath t = γ t

theorem BasedPath.toPath_source {X : Type u_1} [TopologicalSpace X] {x₀ : X} (γ : BasedPath x₀) : γ.toPath 0 = x₀

theorem BasedPath.toPath_target {X : Type u_1} [TopologicalSpace X] {x₀ : X} (γ : BasedPath x₀) : γ.toPath 1 = γ.endpoint

theorem BasedPath.ext {X : Type u_1} [TopologicalSpace X] {x₀ : X} {γ γ' : BasedPath x₀} (h : ∀ (t : ↑unitInterval), γ t = γ' t) : γ = γ'

theorem BasedPath.ext_iff {X : Type u_1} [TopologicalSpace X] {x₀ : X} {γ γ' : BasedPath x₀} : γ = γ' ↔ ∀ (t : ↑unitInterval), γ t = γ' t

def BasedPath.ofPath {X : Type u_1} [TopologicalSpace X] {x₀ y : X} (γ : Path x₀ y) : BasedPath x₀

The canonical inclusion Path x₀ y → BasedPath x₀: package an ordinary path out of x₀ as a based path, forgetting y at the type level. The endpoint is recovered as endpoint (ofPath γ) = y via endpoint_ofPath. The map toPath is a partial inverse: ofPath γ.toPath = γ (ofPath_toPath_self), and conversely (ofPath γ).toPath is γ with its right endpoint cast to endpoint (ofPath γ) (toPath_ofPath).

Equations

• BasedPath.ofPath γ = ⟨γ.toContinuousMap, ⋯⟩

@[simp]

theorem BasedPath.ofPath_apply {X : Type u_1} [TopologicalSpace X] {x₀ y : X} (γ : Path x₀ y) (t : ↑unitInterval) : (ofPath γ) t = γ t

@[simp]

theorem BasedPath.toPath_ofPath {X : Type u_1} [TopologicalSpace X] {x₀ y : X} (γ : Path x₀ y) : (ofPath γ).toPath = γ.cast ⋯ ⋯

@[simp]

theorem BasedPath.endpoint_ofPath {X : Type u_1} [TopologicalSpace X] {x₀ y : X} (γ : Path x₀ y) : (ofPath γ).endpoint = y

@[simp]

theorem BasedPath.ofPath_toPath_self {X : Type u_1} [TopologicalSpace X] {x₀ : X} (γ : BasedPath x₀) : ofPath γ.toPath = γ

The round-trip ofPath ∘ toPath is the identity on BasedPath x₀.

@[simp]

theorem BasedPath.ofPath_cast {X : Type u_1} [TopologicalSpace X] {x₀ y y' : X} (γ : Path x₀ y) (h : y' = y) : ofPath (γ.cast ⋯ h) = ofPath γ

ofPath is invariant under reindexing the right endpoint via Path.cast.

def BasedPath.refl {X : Type u_1} [TopologicalSpace X] (x₀ : X) : BasedPath x₀

The constant based path at x₀.

Equations

• BasedPath.refl x₀ = BasedPath.ofPath (Path.refl x₀)

@[simp]

theorem BasedPath.endpoint_refl {X : Type u_1} [TopologicalSpace X] (x₀ : X) : (refl x₀).endpoint = x₀

@[simp]

theorem BasedPath.toPath_refl {X : Type u_1} [TopologicalSpace X] (x₀ : X) : (refl x₀).toPath = Path.refl x₀

@[simp]

theorem BasedPath.ofPath_refl {X : Type u_1} [TopologicalSpace X] (x₀ : X) : ofPath (Path.refl x₀) = refl x₀

noncomputable def BasedPath.append {X : Type u_1} [TopologicalSpace X] {x₀ y : X} (γ : BasedPath x₀) (δ : Path γ.endpoint y) : BasedPath x₀

Append a path δ at the endpoint of a based path γ, defined as ofPath (γ.toPath.trans δ): the half s ∈ [0, ½] traverses γ at double speed and the half s ∈ [½, 1] traverses δ at double speed (Path.trans_apply). The new endpoint is the endpoint of δ (endpoint_append). This is the move used by joinedIn_preimage_of_append to slide a based path within a path component of endpoint ⁻¹' U.

Equations

• γ.append δ = BasedPath.ofPath (γ.toPath.trans δ)

@[simp]

theorem BasedPath.toPath_append {X : Type u_1} [TopologicalSpace X] {x₀ y : X} (γ : BasedPath x₀) (δ : Path γ.endpoint y) : (γ.append δ).toPath = (γ.toPath.trans δ).cast ⋯ ⋯

@[simp]

theorem BasedPath.endpoint_append {X : Type u_1} [TopologicalSpace X] {x₀ y : X} (γ : BasedPath x₀) (δ : Path γ.endpoint y) : (γ.append δ).endpoint = y

Deforming the end of a based path

noncomputable def BasedPath.deformTerminal {X : Type u_1} [TopologicalSpace X] {x₀ v : X} (γ : BasedPath x₀) (δ : Path γ.endpoint v) {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : b < 1) : BasedPath x₀

Replace the end of a based path γ by a path δ out of its endpoint: the result agrees with γ on [0, a], traverses γ|_[a, 1] on [a, b], and traverses δ on [b, 1]. When a is close to 1 and the range of δ lies in a small neighborhood of the endpoint, this stays in a prescribed compact-open neighborhood of γ.

Equations

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

theorem BasedPath.deformTerminal_apply_of_le {X : Type u_1} [TopologicalSpace X] {x₀ v : X} (γ : BasedPath x₀) (δ : Path γ.endpoint v) {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : b < 1) {t : ↑unitInterval} (ht : ↑t ≤ a) : (γ.deformTerminal δ ha hab hb) t = γ t

theorem BasedPath.deformTerminal_apply_of_lt_of_le {X : Type u_1} [TopologicalSpace X] {x₀ v : X} (γ : BasedPath x₀) (δ : Path γ.endpoint v) {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : b < 1) {t : ↑unitInterval} (hat : a < ↑t) (htb : ↑t ≤ b) : (γ.deformTerminal δ ha hab hb) t = γ.toPath.extend (a + (↑t - a) / (b - a) * (1 - a))

theorem BasedPath.deformTerminal_apply_of_lt {X : Type u_1} [TopologicalSpace X] {x₀ v : X} (γ : BasedPath x₀) (δ : Path γ.endpoint v) {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : b < 1) {t : ↑unitInterval} (hbt : b < ↑t) : (γ.deformTerminal δ ha hab hb) t = δ.extend ((↑t - b) / (1 - b))

@[simp]

theorem BasedPath.endpoint_deformTerminal {X : Type u_1} [TopologicalSpace X] {x₀ v : X} (γ : BasedPath x₀) (δ : Path γ.endpoint v) {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : b < 1) : (γ.deformTerminal δ ha hab hb).endpoint = v

theorem BasedPath.deformTerminal_apply_mem_of_lt {X : Type u_1} [TopologicalSpace X] {x₀ v : X} (γ : BasedPath x₀) (δ : Path γ.endpoint v) {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) (hb : b < 1) {t : ↑unitInterval} {W : Set X} (hγW : Set.MapsTo (⇑γ.toPath.extend) (Set.Icc a 1) W) (hδW : Set.range ⇑δ ⊆ W) (hat : a < ↑t) : (γ.deformTerminal δ ha hab hb) t ∈ W

Past time a, the deformed path stays in any set containing γ [a, 1] and the range of δ.

The endpoint map is open

theorem BasedPath.isOpenMap_endpoint {X : Type u_1} [TopologicalSpace X] [LocallyPathConnectedSpace X] (x₀ : X) : IsOpenMap endpoint

The endpoint map BasedPath x₀ → X is an open map when X is locally path-connected.

Initial segments

noncomputable def BasedPath.initialSegmentFamily {X : Type u_1} [TopologicalSpace X] {x₀ : X} (γ : BasedPath x₀) (t : ↑unitInterval) : BasedPath x₀

The family t ↦ γ|_[0, t] of initial segments of a based path.

Equations

• γ.initialSegmentFamily t = BasedPath.ofPath (γ.toPath.initialSegmentFamily t)

@[simp]

theorem BasedPath.initialSegmentFamily_apply {X : Type u_1} [TopologicalSpace X] {x₀ : X} (γ : BasedPath x₀) (t s : ↑unitInterval) : (γ.initialSegmentFamily t) s = γ.toPath.extend (min ↑s ↑t)

@[simp]

theorem BasedPath.endpoint_initialSegmentFamily {X : Type u_1} [TopologicalSpace X] {x₀ : X} (γ : BasedPath x₀) (t : ↑unitInterval) : (γ.initialSegmentFamily t).endpoint = γ t

@[simp]

theorem BasedPath.initialSegmentFamily_zero {X : Type u_1} [TopologicalSpace X] {x₀ : X} (γ : BasedPath x₀) : γ.initialSegmentFamily 0 = refl x₀

@[simp]

theorem BasedPath.initialSegmentFamily_one {X : Type u_1} [TopologicalSpace X] {x₀ : X} (γ : BasedPath x₀) : γ.initialSegmentFamily 1 = γ

theorem BasedPath.continuous_initialSegmentFamily {X : Type u_1} [TopologicalSpace X] {x₀ : X} (γ : BasedPath x₀) : Continuous γ.initialSegmentFamily

theorem BasedPath.continuous_append_initialSegmentFamily {X : Type u_1} [TopologicalSpace X] {x₀ z : X} (γ : BasedPath x₀) (δ : Path γ.endpoint z) : Continuous fun (t : ↑unitInterval) => γ.append (δ.initialSegmentFamily t)

Appending the initial segments of a path δ to a based path is continuous in the parameter.

Path components of endpoint ⁻¹' U

theorem BasedPath.joinedIn_endpoint_preimage_of_homotopic {X : Type u_1} [TopologicalSpace X] {x₀ y : X} {U : Set X} (hy : y ∈ U) {p q : Path x₀ y} (h : p.Homotopic q) : JoinedIn (endpoint ⁻¹' U) (ofPath p) (ofPath q)

Endpoint-preserving homotopic paths to a point y ∈ U give joined based paths inside the endpoint preimage of U.

theorem BasedPath.joinedIn_preimage_of_append {X : Type u_1} [TopologicalSpace X] {x₀ : X} {U : Set X} {z : X} (γ : BasedPath x₀) (δ : Path γ.endpoint z) (hδ : Set.range ⇑δ ⊆ U) : JoinedIn (endpoint ⁻¹' U) γ (γ.append δ)

Appending a path that stays inside U moves a based path within the same path component of the endpoint preimage of U.

theorem BasedPath.exists_open_nhds_pathComponent_preimage {X : Type u_1} [TopologicalSpace X] {x₀ : X} [LocallyPathConnectedSpace X] {U : Set X} (hU : IsOpen U) (α : BasedPath x₀) (hslsc : SemilocallySimplyConnectedOn (Set.range ⇑α.toPath)) (hα : α.endpoint ∈ U) : ∃ (N : Set (BasedPath x₀)), IsOpen N ∧ α ∈ N ∧ ∀ β ∈ N, JoinedIn (endpoint ⁻¹' U) α β

Variable-endpoint tube/component theorem.

In a locally path-connected space, if semilocal simple connectivity holds along α.toPath and α : BasedPath x₀ has endpoint in an open set U, then α has an open neighborhood N in BasedPath x₀ all of whose members lie in the same path component of endpoint ⁻¹' U as α.

theorem BasedPath.isOpen_pathComponent_preimage {X : Type u_1} [TopologicalSpace X] {x₀ : X} [TauCeti.SemilocallySimplyConnectedSpace X] [LocallyPathConnectedSpace X] {U : Set X} (hU : IsOpen U) (α : BasedPath x₀) : IsOpen (pathComponentIn (endpoint ⁻¹' U) α)

For an open neighborhood U, path components of endpoint ⁻¹' U are open.

theorem BasedPath.toPath_homotopic_of_joinedIn_pathHomotopyTrivial {X : Type u_1} [TopologicalSpace X] {x₀ : X} {U : Set X} (hU : IsPathHomotopyTrivial U) {α β : BasedPath x₀} (heq : α.endpoint = β.endpoint) (hαβ : JoinedIn (endpoint ⁻¹' U) α β) : (α.toPath.cast ⋯ ⋯).Homotopic β.toPath

If α and β are based paths with the same endpoint, joined inside endpoint ⁻¹' U for a path-homotopy-trivial set U, then α.toPath and β.toPath are homotopic (after casting to a common endpoint). A path in BasedPath x₀ from α to β is a free homotopy from α to β whose endpoint trace is a loop in U, and that loop is nullhomotopic.

theorem BasedPath.pathComponentIn_ofPath_eq_of_homotopic {X : Type u_1} [TopologicalSpace X] {x₀ : X} {U : Set X} {y : X} (hy : y ∈ U) {p q : Path x₀ y} (h : p.Homotopic q) : pathComponentIn (endpoint ⁻¹' U) (ofPath p) = pathComponentIn (endpoint ⁻¹' U) (ofPath q)

Path components of endpoint ⁻¹' U are invariant under endpoint-preserving homotopy: if p ≃ q are homotopic paths from x₀ to y ∈ U, then the based paths ofPath p and ofPath q lie in the same path component of endpoint ⁻¹' U.