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.

def homotopic {ι : Type u_1} (V : Type u) [category_theory.category V] [category_theory.preadditive V] (c : complex_shape ι) :

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

Equations
Instances for homotopic
@[protected, instance]
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
@[simp]
noncomputable def homotopy_category.homotopy_of_eq {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (f g : C D) (w : (homotopy_category.quotient V c).map f = (homotopy_category.quotient V c).map g) :

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

Equations
noncomputable def homotopy_category.homotopy_out_map {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D : homological_complex V c} (f : C D) :

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

Equations
@[simp]
theorem homotopy_category.quotient_map_out_comp_out {ι : Type u_1} {V : Type u} [category_theory.category V] [category_theory.preadditive V] {c : complex_shape ι} {C D E : homotopy_category V c} (f : C D) (g : D E) :

Homotopy equivalent complexes become isomorphic in the homotopy category.

Equations

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

Equations

An additive functor induces a functor between homotopy categories.

Equations

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

Equations