Theorems · Definition · category theory

CochainComplex.mappingCone.mapTrianglehIso

{C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Limits.HasBinaryBiproducts C] →
            [inst_4 : CategoryTheory.Preadditive D] →
              [inst_5 : CategoryTheory.Limits.HasBinaryBiproducts D] →
                {K L : CochainComplex C ℤ} →
                  (φ : K ⟶ L) →
                    (G : CategoryTheory.Functor C D) →
                      [inst_6 : G.Additive] →
                        (G.mapHomotopyCategory (ComplexShape.up ℤ)).mapTriangle.obj
                            (CochainComplex.mappingCone.triangleh φ) ≅
                          CochainComplex.mappingCone.triangleh ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)

If φ : K ⟶ L is a morphism of cochain complexes in C and G : C ⥤ D is an additive functor, then the image by G of the triangle triangleh φ identifies to the triangle associated to the image of φ by G.

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Cited by

0 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.Limits.HasBinaryBiproductsCategoryTheory.PreadditiveCategoryTheory.Limits.HasBinaryBiproductsCategoryTheory.Functor.Additive