Homotopies between morphisms in TopCat

In this file, we define the type TopCat.Homotopy of homotopies between two morphisms in the category TopCat.

@[reducible, inline]

abbrev TopCat.Homotopy {X Y : TopCat} (f g : X ⟶ Y) : Type u

An homotopy between morphisms in TopCat is a homotopy between the corresponding continous maps.

Equations

• TopCat.Homotopy f g = (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)

def TopCat.Homotopy.h {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy f g) : CategoryTheory.MonoidalCategoryStruct.tensorObj X I ⟶ Y

The morphism X ⊗ I ⟶ Y that is part of a homotopy between two morphisms in TopCat.

Equations

• H.h = CategoryTheory.CategoryStruct.comp (β_ X TopCat.I).hom (TopCat.ofHom (H.comp ((↑TopCat.I.homeomorph).prodMap (ContinuousMap.id ↑X))))

@[simp]

theorem TopCat.Homotopy.ι₀_h {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy f g) : CategoryTheory.CategoryStruct.comp ι₀ H.h = f

@[simp]

theorem TopCat.Homotopy.ι₀_h_assoc {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy f g) {Z : TopCat} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.CategoryStruct.comp H.h h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem TopCat.Homotopy.ι₁_h {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy f g) : CategoryTheory.CategoryStruct.comp ι₁ H.h = g

@[simp]

theorem TopCat.Homotopy.ι₁_h_assoc {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy f g) {Z : TopCat} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.CategoryStruct.comp H.h h) = CategoryTheory.CategoryStruct.comp g h