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
@[reducible, inline]
abbrev TopCat.Homotopy {X Y : TopCat} (f g : X ⟶ Y) :
Type u

A homotopy between morphisms in TopCat is a homotopy between the corresponding continuous maps.

Equations
Instances For
    source
    def TopCat.Homotopy.h {X Y : TopCat} {f₀ f₁ : X ⟶ Y} (H : Homotopy f₀ f₁) :
    CategoryTheory.MonoidalCategoryStruct.tensorObj X I ⟶ Y

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

    Equations
    Instances For
      source
      @[simp]
      theorem TopCat.Homotopy.h_hom_apply {X Y : TopCat} {f₀ f₁ : X ⟶ Y} (F : Homotopy f₀ f₁) (p : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj X I)) :
      (CategoryTheory.ConcreteCategory.hom F.h) p = F (I.homeomorph p.2, p.1)
      source
      @[simp]
      theorem TopCat.Homotopy.ι₀_h {X Y : TopCat} {f₀ f₁ : X ⟶ Y} (F : Homotopy f₀ f₁) :
      CategoryTheory.CategoryStruct.comp ι₀ F.h = f₀
      source
      @[simp]
      theorem TopCat.Homotopy.ι₀_h_assoc {X Y : TopCat} {f₀ f₁ : X ⟶ Y} (F : Homotopy f₀ f₁) {Z : TopCat} (h : Y ⟶ Z) :
      CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.CategoryStruct.comp F.h h) = CategoryTheory.CategoryStruct.comp f₀ h
      source
      @[simp]
      theorem TopCat.Homotopy.ι₁_h {X Y : TopCat} {f₀ f₁ : X ⟶ Y} (F : Homotopy f₀ f₁) :
      CategoryTheory.CategoryStruct.comp ι₁ F.h = f₁
      source
      @[simp]
      theorem TopCat.Homotopy.ι₁_h_assoc {X Y : TopCat} {f₀ f₁ : X ⟶ Y} (F : Homotopy f₀ f₁) {Z : TopCat} (h : Y ⟶ Z) :
      CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.CategoryStruct.comp F.h h) = CategoryTheory.CategoryStruct.comp f₁ h
      source
      @[reducible, inline]
      abbrev TopCat.Homotopy.refl {X Y : TopCat} (f : X ⟶ Y) :
      (Hom.hom f).Homotopy (Hom.hom f)

      The identity homotopy of a morphism f : X ⟶ Y in TopCat.

      Equations
      Instances For
        source
        @[simp]
        theorem TopCat.Homotopy.refl_apply {X Y : TopCat} (f : X ⟶ Y) (x : ↑unitInterval × ↑X) :
        (refl f) x = (Hom.hom f) x.2
        source
        @[simp]
        theorem TopCat.Homotopy.h_refl {X Y : TopCat} {f₀ : X ⟶ Y} :
        h (refl f₀) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X I) f₀
        source
        @[reducible, inline]
        abbrev TopCat.Homotopy.symm {X Y : TopCat} {f₀ f₁ : X ⟶ Y} (F : Homotopy f₀ f₁) :
        (Hom.hom f₁).Homotopy (Hom.hom f₀)

        The reverse of a homotopy F in TopCat.

        Equations
        Instances For
          source
          @[simp]
          theorem TopCat.Homotopy.symm_apply {X Y : TopCat} {f₀ f₁ : X ⟶ Y} (F : Homotopy f₀ f₁) (x : ↑unitInterval × ↑X) :
          F.symm x = F (unitInterval.symm x.1, x.2)
          source
          @[simp]
          theorem TopCat.Homotopy.h_symm {X Y : TopCat} {f₀ f₁ : X ⟶ Y} (F : Homotopy f₀ f₁) :
          h F.symm = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X I.symm) F.h
          source
          @[reducible, inline]
          noncomputable abbrev TopCat.Homotopy.trans {X Y : TopCat} {f₀ f₁ f₂ : X ⟶ Y} (F : Homotopy f₀ f₁) (G : Homotopy f₁ f₂) :
          (Hom.hom f₀).Homotopy (Hom.hom f₂)

          The compositions of homotopies in TopCat.

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev TopCat.Homotopy.comp {X Y Z : TopCat} {f₀ f₁ : X ⟶ Y} {g₀ g₁ : Y ⟶ Z} (G : Homotopy g₀ g₁) (F : Homotopy f₀ f₁) :
            Homotopy (CategoryTheory.CategoryStruct.comp f₀ g₀) (CategoryTheory.CategoryStruct.comp f₁ g₁)

            The homotopy between compositions of morphisms in TopCat.

            Equations
            Instances For
              source
              @[simp]
              theorem TopCat.Homotopy.comp_apply {X Y Z : TopCat} {f₀ f₁ : X ⟶ Y} {g₀ g₁ : Y ⟶ Z} (G : Homotopy g₀ g₁) (F : Homotopy f₀ f₁) (x : ↑unitInterval × ↑X) :
              (G.comp F) x = G (x.1, F x)
              source
              @[simp]
              theorem TopCat.Homotopy.h_comp {X Y Z : TopCat} {f₀ f₁ : X ⟶ Y} {g₀ g₁ : Y ⟶ Z} (G : Homotopy g₀ g₁) (F : Homotopy f₀ f₁) :
              (G.comp F).h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id I) (CategoryTheory.CategoryStruct.id I))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X I I).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight F.h I) G.h))