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.

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

Instances For
    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.

    Instances For

      The quotient functor from complexes to the homotopy category.

      Instances For

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

        Instances For

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

          Instances For

            Homotopy equivalent complexes become isomorphic in the homotopy category.

            Instances For

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

              Instances For