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.

Equations
Instances For
    def HomotopyCategory {ι : Type u_2} (V : Type u) [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (c : ComplexShape ι) :
    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

      The quotient functor from complexes to the homotopy category.

      Equations
      Instances For

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

        Equations
        Instances For

          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

            Homotopy equivalent complexes become isomorphic in the homotopy category.

            Equations
            Instances For

              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
                @[irreducible]

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

                Equations
                Instances For
                  @[irreducible]

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

                  Equations
                  Instances For
                    @[simp]
                    theorem CategoryTheory.Functor.mapHomotopyCategory_obj {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_3} [CategoryTheory.Category.{u_4, u_3} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] (c : ComplexShape ι) (a : CategoryTheory.Quotient (homotopic V c)) :
                    (F.mapHomotopyCategory c).obj a = (HomotopyCategory.quotient W c).obj ((F.mapHomologicalComplex c).obj a.as)

                    An additive functor induces a functor between homotopy categories.

                    Equations
                    Instances For
                      @[simp]
                      theorem CategoryTheory.Functor.mapHomotopyCategory_map {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_3} [CategoryTheory.Category.{u_4, u_3} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] {c : ComplexShape ι} {K : HomologicalComplex V c} {L : HomologicalComplex V c} (f : K L) :
                      (F.mapHomotopyCategory c).map ((HomotopyCategory.quotient V c).map f) = (HomotopyCategory.quotient W c).map ((F.mapHomologicalComplex c).map f)

                      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
                        def CategoryTheory.NatTrans.mapHomotopyCategory {ι : Type u_2} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {W : Type u_3} [CategoryTheory.Category.{u_4, u_3} W] [CategoryTheory.Preadditive W] {F : CategoryTheory.Functor V W} {G : CategoryTheory.Functor V W} [F.Additive] [G.Additive] (α : F G) (c : ComplexShape ι) :
                        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