Documentation

Mathlib.Topology.Homotopy.TopCat.Basic

Homotopies between morphisms in TopCat #

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

source
🔸 coverage
@[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.

Instances For
    source
    🔸 coverage
    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.

    Instances For
      source
      📐 coverage
      @[simp]
      theorem TopCat.Homotopy.ι₀_h {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy f g) :
      CategoryTheory.CategoryStruct.comp ι₀ H.h = f
      source
      📐 coverage
      @[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
      source
      📐 coverage
      @[simp]
      theorem TopCat.Homotopy.ι₁_h {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy f g) :
      CategoryTheory.CategoryStruct.comp ι₁ H.h = g
      source
      📐 coverage
      @[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