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

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

Equations

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

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

• 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_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)

@[simp]

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

@[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

@[simp]

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

@[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

@[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

• TopCat.Homotopy.refl f = ContinuousMap.Homotopy.refl (TopCat.Hom.hom f)

@[simp]

theorem TopCat.Homotopy.h_refl {X Y : TopCat} {f₀ : X ⟶ Y} : h (refl f₀) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst X I) f₀

@[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

• F.symm = ContinuousMap.Homotopy.symm F

@[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

@[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

• F.trans G = ContinuousMap.Homotopy.trans F G

@[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

• G.comp F = ContinuousMap.Homotopy.comp G F

@[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)

@[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))