Paths between points of an object of TopCat

This file introduces a structure TopCat.Path for paths between two points of an object X : TopCat. The data is defined using a morphism I ⟶ X in the category TopCat.

structure TopCat.Path (X : TopCat) (x y : ↑X) : Type u

Given two points x and y of X : TopCat, this is the type of paths from x to y, defined using a morphism I ⟶ X. Set TopCat.pathEquiv for the relation with _root_.Path x y.

• hom : I ⟶ X

  a morphism from the unit interval

• hom₀ : (CategoryTheory.ConcreteCategory.hom self.hom) 0 = x
• hom₁ : (CategoryTheory.ConcreteCategory.hom self.hom) 1 = y

theorem TopCat.Path.ext {X : TopCat} {x y : ↑X} {x✝ y✝ : X.Path x y} (hom : x✝.hom = y✝.hom) : x✝ = y✝

theorem TopCat.Path.ext_iff {X : TopCat} {x y : ↑X} {x✝ y✝ : X.Path x y} : x✝ = y✝ ↔ x✝.hom = y✝.hom

def TopCat.pathEquiv {X : TopCat} {x y : ↑X} : X.Path x y ≃ Path x y

The bijection between TopCat.Path X x y and _root_.Path x y.

Equations

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

@[simp]

theorem TopCat.pathEquiv_symm_apply_hom_hom_apply {X : TopCat} {x y : ↑X} (p : Path x y) (a✝ : ULift.{u, 0} ↑unitInterval) : (Hom.hom (pathEquiv.symm p).hom) a✝ = p (I.homeomorph a✝)

@[simp]

theorem TopCat.pathEquiv_apply_apply {X : TopCat} {x y : ↑X} (p : X.Path x y) (a✝ : ↑unitInterval) : (pathEquiv p) a✝ = (Hom.hom p.hom) (I.homeomorph.symm a✝)