The homotopy category

HomotopyCategory V c gives the category of chain complexes of shape c in V, with chain maps identified when they are homotopic.

def homotopic {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : HomRel (HomologicalComplex V c)

The congruence on HomologicalComplex V c given by the existence of a homotopy.

instance homotopy_congruence {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : CategoryTheory.Congruence (homotopic V c)

def HomotopyCategory {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : Type (max (max u u_1) v)

HomotopyCategory V c is the category of chain complexes of shape c in V, with chain maps identified when they are homotopic.

instance instCategoryHomotopyCategory (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] : {ι : Type u_2} → {v : ComplexShape ι} → CategoryTheory.Category.{max v u_2, max (max u v) u_2} (HomotopyCategory V v)

def HomotopyCategory.quotient {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) : CategoryTheory.Functor (HomologicalComplex V c) (HomotopyCategory V c)

The quotient functor from complexes to the homotopy category.

instance HomotopyCategory.instInhabitedHomotopyCategory {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.Limits.HasZeroObject V] : Inhabited (HomotopyCategory V c)

theorem HomotopyCategory.quotient_obj_as {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (C : HomologicalComplex V c) : ((HomotopyCategory.quotient V c).obj C).as = C

@[simp]

theorem HomotopyCategory.quotient_map_out {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomotopyCategory V c} {D : HomotopyCategory V c} (f : C ⟶ D) : (HomotopyCategory.quotient V c).map (Quot.out f) = f

theorem HomotopyCategory.quot_mk_eq_quotient_map {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : C ⟶ D) : Quot.mk (CategoryTheory.Quotient.CompClosure (homotopic V c)) f = (HomotopyCategory.quotient V c).map f

theorem HomotopyCategory.eq_of_homotopy {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : C ⟶ D) (g : C ⟶ D) (h : Homotopy f g) : (HomotopyCategory.quotient V c).map f = (HomotopyCategory.quotient V c).map g

def HomotopyCategory.homotopyOfEq {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : C ⟶ D) (g : C ⟶ D) (w : (HomotopyCategory.quotient V c).map f = (HomotopyCategory.quotient V c).map g) : Homotopy f g

If two chain maps become equal in the homotopy category, then they are homotopic.

def HomotopyCategory.homotopyOutMap {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : C ⟶ D) : Homotopy (Quot.out ((HomotopyCategory.quotient V c).map f)) f

An arbitrarily chosen representation of the image of a chain map in the homotopy category is homotopic to the original chain map.

@[simp]

theorem HomotopyCategory.quotient_map_out_comp_out {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomotopyCategory V c} {D : HomotopyCategory V c} {E : HomotopyCategory V c} (f : C ⟶ D) (g : D ⟶ E) : (HomotopyCategory.quotient V c).map (CategoryTheory.CategoryStruct.comp (Quot.out f) (Quot.out g)) = CategoryTheory.CategoryStruct.comp f g

@[simp]

theorem HomotopyCategory.isoOfHomotopyEquiv_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : HomotopyEquiv C D) : (HomotopyCategory.isoOfHomotopyEquiv f).hom = (HomotopyCategory.quotient V c).map f.hom

@[simp]

theorem HomotopyCategory.isoOfHomotopyEquiv_inv {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : HomotopyEquiv C D) : (HomotopyCategory.isoOfHomotopyEquiv f).inv = (HomotopyCategory.quotient V c).map f.inv

def HomotopyCategory.isoOfHomotopyEquiv {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : HomotopyEquiv C D) : (HomotopyCategory.quotient V c).obj C ≅ (HomotopyCategory.quotient V c).obj D

Homotopy equivalent complexes become isomorphic in the homotopy category.

def HomotopyCategory.homotopyEquivOfIso {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (i : (HomotopyCategory.quotient V c).obj C ≅ (HomotopyCategory.quotient V c).obj D) : HomotopyEquiv C D

If two complexes become isomorphic in the homotopy category, then they were homotopy equivalent.

def HomotopyCategory.homologyFunctor {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] [CategoryTheory.Limits.HasCokernels V] (i : ι) : CategoryTheory.Functor (HomotopyCategory V c) V

The i-th homology, as a functor from the homotopy category.

def HomotopyCategory.homologyFactors {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] [CategoryTheory.Limits.HasCokernels V] (i : ι) : CategoryTheory.Functor.comp (HomotopyCategory.quotient V c) (HomotopyCategory.homologyFunctor V c i) ≅ homologyFunctor V c i

The homology functor on the homotopy category is just the usual homology functor.

@[simp]

theorem HomotopyCategory.homologyFactors_hom_app {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] [CategoryTheory.Limits.HasCokernels V] (i : ι) (C : HomologicalComplex V c) : (HomotopyCategory.homologyFactors V c i).hom.app C = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.comp (HomotopyCategory.quotient V c) (HomotopyCategory.homologyFunctor V c i)).obj C)

@[simp]

theorem HomotopyCategory.homologyFactors_inv_app {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] [CategoryTheory.Limits.HasCokernels V] (i : ι) (C : HomologicalComplex V c) : (HomotopyCategory.homologyFactors V c i).inv.app C = CategoryTheory.CategoryStruct.id ((homologyFunctor V c i).obj C)

theorem HomotopyCategory.homologyFunctor_map_factors {ι : Type u_1} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) [CategoryTheory.Limits.HasEqualizers V] [CategoryTheory.Limits.HasImages V] [CategoryTheory.Limits.HasImageMaps V] [CategoryTheory.Limits.HasCokernels V] (i : ι) {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : C ⟶ D) : (homologyFunctor V c i).map f = (HomotopyCategory.homologyFunctor V c i).map ((HomotopyCategory.quotient V c).map f)

@[simp]

theorem CategoryTheory.Functor.mapHomotopyCategory_obj {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [CategoryTheory.Functor.Additive F] (c : ComplexShape ι) (a : CategoryTheory.Quotient (homotopic V c)) : (CategoryTheory.Functor.mapHomotopyCategory F c).obj a = (HomotopyCategory.quotient W c).obj ((CategoryTheory.Functor.mapHomologicalComplex F c).obj a.as)

def CategoryTheory.Functor.mapHomotopyCategory {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [CategoryTheory.Functor.Additive F] (c : ComplexShape ι) : CategoryTheory.Functor (HomotopyCategory V c) (HomotopyCategory W c)

An additive functor induces a functor between homotopy categories.

@[simp]

theorem CategoryTheory.Functor.mapHomotopyCategory_map {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [CategoryTheory.Functor.Additive F] {c : ComplexShape ι} {K : HomologicalComplex V c} {L : HomologicalComplex V c} (f : K ⟶ L) : (CategoryTheory.Functor.mapHomotopyCategory F c).map ((HomotopyCategory.quotient V c).map f) = (HomotopyCategory.quotient W c).map ((CategoryTheory.Functor.mapHomologicalComplex F c).map f)

@[simp]

theorem CategoryTheory.NatTrans.mapHomotopyCategory_app {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] {F : CategoryTheory.Functor V W} {G : CategoryTheory.Functor V W} [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] (α : F ⟶ G) (c : ComplexShape ι) (C : HomotopyCategory V c) : (CategoryTheory.NatTrans.mapHomotopyCategory α c).app C = (HomotopyCategory.quotient W c).map ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C.as)

def CategoryTheory.NatTrans.mapHomotopyCategory {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] {F : CategoryTheory.Functor V W} {G : CategoryTheory.Functor V W} [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] (α : F ⟶ G) (c : ComplexShape ι) : CategoryTheory.Functor.mapHomotopyCategory F c ⟶ CategoryTheory.Functor.mapHomotopyCategory G c

A natural transformation induces a natural transformation between the induced functors on the homotopy category.

@[simp]

theorem CategoryTheory.NatTrans.mapHomotopyCategory_id {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (c : ComplexShape ι) (F : CategoryTheory.Functor V W) [CategoryTheory.Functor.Additive F] : CategoryTheory.NatTrans.mapHomotopyCategory (CategoryTheory.CategoryStruct.id F) c = CategoryTheory.CategoryStruct.id (CategoryTheory.Functor.mapHomotopyCategory F c)

@[simp]

theorem CategoryTheory.NatTrans.mapHomotopyCategory_comp {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (c : ComplexShape ι) {F : CategoryTheory.Functor V W} {G : CategoryTheory.Functor V W} {H : CategoryTheory.Functor V W} [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] [CategoryTheory.Functor.Additive H] (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.NatTrans.mapHomotopyCategory (CategoryTheory.CategoryStruct.comp α β) c = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.mapHomotopyCategory α c) (CategoryTheory.NatTrans.mapHomotopyCategory β c)