mathlib documentation

algebra.homology.homotopy_category

The homotopy category #

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

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

Equations
Instances for homotopic
def homotopy_category {ι : Type u_1} (V : Type u) [category_theory.category V] [category_theory.preadditive V] (c : complex_shape ι) :
Type (max u u_1 v)

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

Equations
Instances for homotopy_category

The quotient functor from complexes to the homotopy category.

Equations

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

Equations

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

Equations

Homotopy equivalent complexes become isomorphic in the homotopy category.

Equations

An additive functor induces a functor between homotopy categories.

Equations