# 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_2} (V : Type u) (c : ) :

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

Equations
Instances For
instance homotopy_congruence {ι : Type u_2} (V : Type u) (c : ) :
Equations
• =
def HomotopyCategory {ι : Type u_2} (V : Type u) (c : ) :
Type (max (max u u_2) v)

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

Equations
Instances For
instance instCategoryHomotopyCategory {ι : Type u_2} (V : Type u) (c : ) :
Equations
• = id inferInstance
instance HomotopyCategory.instPreadditive {ι : Type u_2} (V : Type u) (c : ) :
Equations
def HomotopyCategory.quotient {ι : Type u_2} (V : Type u) (c : ) :

The quotient functor from complexes to the homotopy category.

Equations
Instances For
instance HomotopyCategory.instFullHomologicalComplexQuotient {ι : Type u_2} (V : Type u) (c : ) :
.Full
Equations
• =
instance HomotopyCategory.instEssSurjHomologicalComplexQuotient {ι : Type u_2} (V : Type u) (c : ) :
.EssSurj
Equations
• =
instance HomotopyCategory.instAdditiveHomologicalComplexQuotient {ι : Type u_2} (V : Type u) (c : ) :
Equations
• =
Equations
• = inferInstance
Equations
• =
instance HomotopyCategory.instLinear {R : Type u_1} [] {ι : Type u_2} (V : Type u) (c : ) [] :
Equations
instance HomotopyCategory.instLinearHomologicalComplexQuotient {R : Type u_1} [] {ι : Type u_2} (V : Type u) (c : ) [] :
Equations
• =
instance HomotopyCategory.instInhabitedOfHasZeroObject {ι : Type u_2} (V : Type u) (c : ) :
Equations
• = { default := .obj 0 }
instance HomotopyCategory.instHasZeroObject {ι : Type u_2} (V : Type u) (c : ) :
Equations
• =
instance HomotopyCategory.instFullFunctorHomologicalComplexObjWhiskeringLeftQuotient {ι : Type u_2} (V : Type u) (c : ) {D : Type u_3} [] :
(().obj ).Full
Equations
• =
instance HomotopyCategory.instFaithfulFunctorHomologicalComplexObjWhiskeringLeftQuotient {ι : Type u_2} (V : Type u) (c : ) {D : Type u_3} [] :
(().obj ).Faithful
Equations
• =
theorem HomotopyCategory.quotient_obj_as {ι : Type u_2} {V : Type u} {c : } (C : ) :
(.obj C).as = C
@[simp]
theorem HomotopyCategory.quotient_map_out {ι : Type u_2} {V : Type u} {c : } {C : } {D : } (f : C D) :
.map () = f
theorem HomotopyCategory.quot_mk_eq_quotient_map {ι : Type u_2} {V : Type u} {c : } {C : } {D : } (f : C D) :
= .map f
theorem HomotopyCategory.eq_of_homotopy {ι : Type u_2} {V : Type u} {c : } {C : } {D : } (f : C D) (g : C D) (h : Homotopy f g) :
.map f = .map g
def HomotopyCategory.homotopyOfEq {ι : Type u_2} {V : Type u} {c : } {C : } {D : } (f : C D) (g : C D) (w : .map f = .map g) :

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

Equations
Instances For
def HomotopyCategory.homotopyOutMap {ι : Type u_2} {V : Type u} {c : } {C : } {D : } (f : C D) :
Homotopy (Quot.out (.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.

Equations
Instances For
@[simp]
theorem HomotopyCategory.quotient_map_out_comp_out {ι : Type u_2} {V : Type u} {c : } {C : } {D : } {E : } (f : C D) (g : D E) :
@[simp]
theorem HomotopyCategory.isoOfHomotopyEquiv_hom {ι : Type u_2} {V : Type u} {c : } {C : } {D : } (f : ) :
= .map f.hom
@[simp]
theorem HomotopyCategory.isoOfHomotopyEquiv_inv {ι : Type u_2} {V : Type u} {c : } {C : } {D : } (f : ) :
= .map f.inv
def HomotopyCategory.isoOfHomotopyEquiv {ι : Type u_2} {V : Type u} {c : } {C : } {D : } (f : ) :
.obj C .obj D

Homotopy equivalent complexes become isomorphic in the homotopy category.

Equations
• = { hom := .map f.hom, inv := .map f.inv, hom_inv_id := , inv_hom_id := }
Instances For
def HomotopyCategory.homotopyEquivOfIso {ι : Type u_2} {V : Type u} {c : } {C : } {D : } (i : .obj C .obj D) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem HomotopyCategory.quotient_inverts_homotopyEquivalences {ι : Type u_2} (V : Type u) (c : ) :
.IsInvertedBy
theorem HomotopyCategory.isZero_quotient_obj_iff {ι : Type u_2} {V : Type u} {c : } (C : ) :
@[irreducible]
noncomputable def HomotopyCategory.homologyFunctor {ι : Type u_2} (V : Type u) (c : ) (i : ι) :

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

Equations
Instances For
@[irreducible]
noncomputable def HomotopyCategory.homologyFunctorFactors {ι : Type u_2} (V : Type u) (c : ) (i : ι) :
.comp ()

The homology functor on the homotopy category is induced by the homology functor on homological complexes.

Equations
Instances For
instance HomotopyCategory.instAdditiveHomologyFunctor {ι : Type u_2} (V : Type u) (c : ) (i : ι) :
Equations
• =
@[simp]
theorem CategoryTheory.Functor.mapHomotopyCategory_obj {ι : Type u_2} {V : Type u} {W : Type u_3} [] (F : ) [F.Additive] (c : ) (a : ) :
(F.mapHomotopyCategory c).obj a = .obj ((F.mapHomologicalComplex c).obj a.as)
def CategoryTheory.Functor.mapHomotopyCategory {ι : Type u_2} {V : Type u} {W : Type u_3} [] (F : ) [F.Additive] (c : ) :

An additive functor induces a functor between homotopy categories.

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.mapHomotopyCategory_map {ι : Type u_2} {V : Type u} {W : Type u_3} [] (F : ) [F.Additive] {c : } {K : } {L : } (f : K L) :
(F.mapHomotopyCategory c).map (.map f) = .map ((F.mapHomologicalComplex c).map f)
def CategoryTheory.Functor.mapHomotopyCategoryFactors {ι : Type u_2} {V : Type u} {W : Type u_3} [] (F : ) [F.Additive] (c : ) :
.comp (F.mapHomotopyCategory c) (F.mapHomologicalComplex c).comp

The obvious isomorphism between HomotopyCategory.quotient V c ⋙ F.mapHomotopyCategory c and F.mapHomologicalComplex c ⋙ HomotopyCategory.quotient W c when F : V ⥤ W is an additive functor.

Equations
Instances For
@[simp]
theorem CategoryTheory.NatTrans.mapHomotopyCategory_app {ι : Type u_2} {V : Type u} {W : Type u_3} [] {F : } {G : } [F.Additive] [G.Additive] (α : F G) (c : ) (C : ) :
C = .map ( C.as)
def CategoryTheory.NatTrans.mapHomotopyCategory {ι : Type u_2} {V : Type u} {W : Type u_3} [] {F : } {G : } [F.Additive] [G.Additive] (α : F G) (c : ) :
F.mapHomotopyCategory c G.mapHomotopyCategory c

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.NatTrans.mapHomotopyCategory_id {ι : Type u_2} {V : Type u} {W : Type u_3} [] (c : ) (F : ) [F.Additive] :
= CategoryTheory.CategoryStruct.id (F.mapHomotopyCategory c)
@[simp]
theorem CategoryTheory.NatTrans.mapHomotopyCategory_comp {ι : Type u_2} {V : Type u} {W : Type u_3} [] (c : ) {F : } {G : } {H : } [F.Additive] [G.Additive] [H.Additive] (α : F G) (β : G H) :