# Documentation

Mathlib.Algebra.Homology.HomotopyCategory

# 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) (c : ) :

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

Instances For
instance homotopy_congruence {ι : Type u_1} (V : Type u) (c : ) :
def HomotopyCategory {ι : Type u_1} (V : Type u) (c : ) :
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.

Instances For
instance instCategoryHomotopyCategory (V : Type u) :
{ι : Type u_2} → {v : } →
def HomotopyCategory.quotient {ι : Type u_1} (V : Type u) (c : ) :

The quotient functor from complexes to the homotopy category.

Instances For
theorem HomotopyCategory.quotient_obj_as {ι : Type u_1} {V : Type u} {c : } (C : ) :
(().obj C).as = C
@[simp]
theorem HomotopyCategory.quotient_map_out {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : C D) :
().map () = f
theorem HomotopyCategory.quot_mk_eq_quotient_map {ι : Type u_1} {V : Type u} {c : } {C : } {D : } (f : C D) :
= ().map f
theorem HomotopyCategory.eq_of_homotopy {ι : Type u_1} {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_1} {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.

Instances For
def HomotopyCategory.homotopyOutMap {ι : Type u_1} {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.

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

Homotopy equivalent complexes become isomorphic in the homotopy category.

Instances For
def HomotopyCategory.homotopyEquivOfIso {ι : Type u_1} {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.

Instances For
def HomotopyCategory.homologyFunctor {ι : Type u_1} (V : Type u) (c : ) (i : ι) :

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

Instances For
def HomotopyCategory.homologyFactors {ι : Type u_1} (V : Type u) (c : ) (i : ι) :

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

Instances For
@[simp]
theorem HomotopyCategory.homologyFactors_hom_app {ι : Type u_1} (V : Type u) (c : ) (i : ι) (C : ) :
().hom.app C =
@[simp]
theorem HomotopyCategory.homologyFactors_inv_app {ι : Type u_1} (V : Type u) (c : ) (i : ι) (C : ) :
().inv.app C = CategoryTheory.CategoryStruct.id (().obj C)
theorem HomotopyCategory.homologyFunctor_map_factors {ι : Type u_1} (V : Type u) (c : ) (i : ι) {C : } {D : } (f : C D) :
().map f = ().map (().map f)
@[simp]
theorem CategoryTheory.Functor.mapHomotopyCategory_obj {ι : Type u_1} {V : Type u} {W : Type u_2} [] (F : ) (c : ) (a : ) :
().obj a = ().obj (().obj a.as)
def CategoryTheory.Functor.mapHomotopyCategory {ι : Type u_1} {V : Type u} {W : Type u_2} [] (F : ) (c : ) :

An additive functor induces a functor between homotopy categories.

Instances For
@[simp]
theorem CategoryTheory.Functor.mapHomotopyCategory_map {ι : Type u_1} {V : Type u} {W : Type u_2} [] (F : ) {c : } {K : } {L : } (f : K L) :
().map (().map f) = ().map (().map f)
@[simp]
theorem CategoryTheory.NatTrans.mapHomotopyCategory_app {ι : Type u_1} {V : Type u} {W : Type u_2} [] {F : } {G : } (α : F G) (c : ) (C : ) :
().app C = ().map (().app C.as)
def CategoryTheory.NatTrans.mapHomotopyCategory {ι : Type u_1} {V : Type u} {W : Type u_2} [] {F : } {G : } (α : F G) (c : ) :

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

Instances For
@[simp]
theorem CategoryTheory.NatTrans.mapHomotopyCategory_id {ι : Type u_1} {V : Type u} {W : Type u_2} [] (c : ) (F : ) :
@[simp]
theorem CategoryTheory.NatTrans.mapHomotopyCategory_comp {ι : Type u_1} {V : Type u} {W : Type u_2} [] (c : ) {F : } {G : } {H : } (α : F G) (β : G H) :