Theorems · Definition · category theory

HomologicalComplex.cylinder.mapHomologicalComplexObjIso

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (F : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              {D : Type u_3} →
                [inst_3 : CategoryTheory.Category.{v_2, u_3} D] →
                  [inst_4 : CategoryTheory.Preadditive D] →
                    (H : CategoryTheory.Functor C D) →
                      [inst_5 : H.Additive] →
                        [inst_6 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (F.X i) (F.X i)] →
                          [inst_7 :
                              HomologicalComplex.HasHomotopyCofiber
                                (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id F)
                                  (-CategoryTheory.CategoryStruct.id F))] →
                            [inst_8 :
                                ∀ (i : ι),
                                  CategoryTheory.Limits.HasBinaryBiproduct (((H.mapHomologicalComplex c).obj F).X i)
                                    (((H.mapHomologicalComplex c).obj F).X i)] →
                              [inst_9 :
                                  HomologicalComplex.HasHomotopyCofiber
                                    (CategoryTheory.Limits.biprod.lift
                                      (CategoryTheory.CategoryStruct.id ((H.mapHomologicalComplex c).obj F))
                                      (-CategoryTheory.CategoryStruct.id ((H.mapHomologicalComplex c).obj F)))] →
                                [HomologicalComplex.HasHomotopyCofiber
                                      ((H.mapHomologicalComplex c).map
                                        (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id F)
                                          (-CategoryTheory.CategoryStruct.id F)))] →
                                  (∀ (j : ι), ∃ i, c.Rel i j) →
                                    ((H.mapHomologicalComplex c).obj F.cylinder ≅
                                      ((H.mapHomologicalComplex c).obj F).cylinder)

The isomorphism expressing the commutation between taking the cylinder of a homological complex and applying an additive functor.

Defined in

Mathlib.Algebra.Homology.HomotopyCofiber

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveDecidableRelCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.Functor.AdditiveCategoryTheory.Limits.HasBinaryBiproductHomologicalComplex.HasHomotopyCofiberCategoryTheory.Limits.HasBinaryBiproductHomologicalComplex.HasHomotopyCofiberHomologicalComplex.HasHomotopyCofiber