Documentation

Mathlib.Algebra.Homology.ShortComplex.Limits

Limits and colimits in the category of short complexes #

In this file, it is shown if a category C with zero morphisms has limits of a certain shape J, then it is also the case of the category ShortComplex C.

TODO (@rioujoel): Do the same for colimits.

source
def CategoryTheory.ShortComplex.isLimitOfIsLimitπ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} (c : CategoryTheory.Limits.Cone F) (h₁ : CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.π₁.mapCone c)) (h₂ : CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.π₂.mapCone c)) (h₃ : CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.π₃.mapCone c)) :
CategoryTheory.Limits.IsLimit c

If a cone with values in ShortComplex C is such that it becomes limit when we apply the three projections ShortComplex C ⥤ C, then it is limit.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def CategoryTheory.ShortComplex.limitCone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
    CategoryTheory.Limits.Cone F

    Construction of a limit cone for a functor J ⥤ ShortComplex C using the limits of the three components J ⥤ C.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def CategoryTheory.ShortComplex.isLimitπ₁MapConeLimitCone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
      CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.π₁.mapCone (CategoryTheory.ShortComplex.limitCone F))

      limitCone F becomes limit after the application of π₁ : ShortComplex C ⥤ C.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def CategoryTheory.ShortComplex.isLimitπ₂MapConeLimitCone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
        CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.π₂.mapCone (CategoryTheory.ShortComplex.limitCone F))

        limitCone F becomes limit after the application of π₂ : ShortComplex C ⥤ C.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def CategoryTheory.ShortComplex.isLimitπ₃MapConeLimitCone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
          CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.π₃.mapCone (CategoryTheory.ShortComplex.limitCone F))

          limitCone F becomes limit after the application of π₃ : ShortComplex C ⥤ C.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def CategoryTheory.ShortComplex.isLimitLimitCone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
            CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.limitCone F)

            limitCone F is limit.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              instance CategoryTheory.ShortComplex.hasLimit_of_hasLimitπ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
              CategoryTheory.Limits.HasLimit F
              Equations
              source
              noncomputable instance CategoryTheory.ShortComplex.instPreservesLimitShortComplexInstCategoryShortComplexπ₁ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
              CategoryTheory.Limits.PreservesLimit F CategoryTheory.ShortComplex.π₁
              Equations
              • One or more equations did not get rendered due to their size.
              source
              noncomputable instance CategoryTheory.ShortComplex.instPreservesLimitShortComplexInstCategoryShortComplexπ₂ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
              CategoryTheory.Limits.PreservesLimit F CategoryTheory.ShortComplex.π₂
              Equations
              • One or more equations did not get rendered due to their size.
              source
              noncomputable instance CategoryTheory.ShortComplex.instPreservesLimitShortComplexInstCategoryShortComplexπ₃ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
              CategoryTheory.Limits.PreservesLimit F CategoryTheory.ShortComplex.π₃
              Equations
              • One or more equations did not get rendered due to their size.
              source
              instance CategoryTheory.ShortComplex.hasLimitsOfShape {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape J C] :
              CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.ShortComplex C)
              Equations
              source
              noncomputable instance CategoryTheory.ShortComplex.instPreservesLimitsOfShapeShortComplexInstCategoryShortComplexπ₁ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape J C] :
              CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.ShortComplex.π₁
              Equations
              • CategoryTheory.ShortComplex.instPreservesLimitsOfShapeShortComplexInstCategoryShortComplexπ₁ = CategoryTheory.Limits.PreservesLimitsOfShape.mk
              source
              noncomputable instance CategoryTheory.ShortComplex.instPreservesLimitsOfShapeShortComplexInstCategoryShortComplexπ₂ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape J C] :
              CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.ShortComplex.π₂
              Equations
              • CategoryTheory.ShortComplex.instPreservesLimitsOfShapeShortComplexInstCategoryShortComplexπ₂ = CategoryTheory.Limits.PreservesLimitsOfShape.mk
              source
              noncomputable instance CategoryTheory.ShortComplex.instPreservesLimitsOfShapeShortComplexInstCategoryShortComplexπ₃ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape J C] :
              CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.ShortComplex.π₃
              Equations
              • CategoryTheory.ShortComplex.instPreservesLimitsOfShapeShortComplexInstCategoryShortComplexπ₃ = CategoryTheory.Limits.PreservesLimitsOfShape.mk
              source
              instance CategoryTheory.ShortComplex.hasFiniteLimits {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] :
              CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.ShortComplex C)
              Equations
              source
              noncomputable instance CategoryTheory.ShortComplex.instPreservesFiniteLimitsShortComplexInstCategoryShortComplexπ₁ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] :
              CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.ShortComplex.π₁
              Equations
              • CategoryTheory.ShortComplex.instPreservesFiniteLimitsShortComplexInstCategoryShortComplexπ₁ = CategoryTheory.Limits.PreservesFiniteLimits.mk
              source
              noncomputable instance CategoryTheory.ShortComplex.instPreservesFiniteLimitsShortComplexInstCategoryShortComplexπ₂ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] :
              CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.ShortComplex.π₂
              Equations
              • CategoryTheory.ShortComplex.instPreservesFiniteLimitsShortComplexInstCategoryShortComplexπ₂ = CategoryTheory.Limits.PreservesFiniteLimits.mk
              source
              noncomputable instance CategoryTheory.ShortComplex.instPreservesFiniteLimitsShortComplexInstCategoryShortComplexπ₃ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteLimits C] :
              CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.ShortComplex.π₃
              Equations
              • CategoryTheory.ShortComplex.instPreservesFiniteLimitsShortComplexInstCategoryShortComplexπ₃ = CategoryTheory.Limits.PreservesFiniteLimits.mk
              source
              instance CategoryTheory.ShortComplex.preservesMonomorphisms_π₁ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingCospan C] :
              CategoryTheory.Functor.PreservesMonomorphisms CategoryTheory.ShortComplex.π₁
              Equations
              source
              instance CategoryTheory.ShortComplex.preservesMonomorphisms_π₂ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingCospan C] :
              CategoryTheory.Functor.PreservesMonomorphisms CategoryTheory.ShortComplex.π₂
              Equations
              source
              instance CategoryTheory.ShortComplex.preservesMonomorphisms_π₃ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingCospan C] :
              CategoryTheory.Functor.PreservesMonomorphisms CategoryTheory.ShortComplex.π₃
              Equations
              source
              def CategoryTheory.ShortComplex.isColimitOfIsColimitπ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} (c : CategoryTheory.Limits.Cocone F) (h₁ : CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₁.mapCocone c)) (h₂ : CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₂.mapCocone c)) (h₃ : CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₃.mapCocone c)) :
              CategoryTheory.Limits.IsColimit c

              If a cocone with values in ShortComplex C is such that it becomes colimit when we apply the three projections ShortComplex C ⥤ C, then it is colimit.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def CategoryTheory.ShortComplex.colimitCocone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
                CategoryTheory.Limits.Cocone F

                Construction of a colimit cocone for a functor J ⥤ ShortComplex C using the colimits of the three components J ⥤ C.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def CategoryTheory.ShortComplex.isColimitπ₁MapCoconeColimitCocone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
                  CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₁.mapCocone (CategoryTheory.ShortComplex.colimitCocone F))

                  colimitCocone F becomes colimit after the application of π₁ : ShortComplex C ⥤ C.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    noncomputable def CategoryTheory.ShortComplex.isColimitπ₂MapCoconeColimitCocone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
                    CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₂.mapCocone (CategoryTheory.ShortComplex.colimitCocone F))

                    colimitCocone F becomes colimit after the application of π₂ : ShortComplex C ⥤ C.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      noncomputable def CategoryTheory.ShortComplex.isColimitπ₃MapCoconeColimitCocone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
                      CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₃.mapCocone (CategoryTheory.ShortComplex.colimitCocone F))

                      colimitCocone F becomes colimit after the application of π₃ : ShortComplex C ⥤ C.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        noncomputable def CategoryTheory.ShortComplex.isColimitColimitCocone {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
                        CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.colimitCocone F)

                        colimitCocone F is colimit.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          instance CategoryTheory.ShortComplex.hasColimit_of_hasColimitπ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
                          CategoryTheory.Limits.HasColimit F
                          Equations
                          source
                          noncomputable instance CategoryTheory.ShortComplex.instPreservesColimitShortComplexInstCategoryShortComplexπ₁ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
                          CategoryTheory.Limits.PreservesColimit F CategoryTheory.ShortComplex.π₁
                          Equations
                          • One or more equations did not get rendered due to their size.
                          source
                          noncomputable instance CategoryTheory.ShortComplex.instPreservesColimitShortComplexInstCategoryShortComplexπ₂ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
                          CategoryTheory.Limits.PreservesColimit F CategoryTheory.ShortComplex.π₂
                          Equations
                          • One or more equations did not get rendered due to their size.
                          source
                          noncomputable instance CategoryTheory.ShortComplex.instPreservesColimitShortComplexInstCategoryShortComplexπ₃ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.comp F CategoryTheory.ShortComplex.π₃)] :
                          CategoryTheory.Limits.PreservesColimit F CategoryTheory.ShortComplex.π₃
                          Equations
                          • One or more equations did not get rendered due to their size.
                          source
                          instance CategoryTheory.ShortComplex.hasColimitsOfShape {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape J C] :
                          CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.ShortComplex C)
                          Equations
                          source
                          noncomputable instance CategoryTheory.ShortComplex.instPreservesColimitsOfShapeShortComplexInstCategoryShortComplexπ₁ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape J C] :
                          CategoryTheory.Limits.PreservesColimitsOfShape J CategoryTheory.ShortComplex.π₁
                          Equations
                          • CategoryTheory.ShortComplex.instPreservesColimitsOfShapeShortComplexInstCategoryShortComplexπ₁ = CategoryTheory.Limits.PreservesColimitsOfShape.mk
                          source
                          noncomputable instance CategoryTheory.ShortComplex.instPreservesColimitsOfShapeShortComplexInstCategoryShortComplexπ₂ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape J C] :
                          CategoryTheory.Limits.PreservesColimitsOfShape J CategoryTheory.ShortComplex.π₂
                          Equations
                          • CategoryTheory.ShortComplex.instPreservesColimitsOfShapeShortComplexInstCategoryShortComplexπ₂ = CategoryTheory.Limits.PreservesColimitsOfShape.mk
                          source
                          noncomputable instance CategoryTheory.ShortComplex.instPreservesColimitsOfShapeShortComplexInstCategoryShortComplexπ₃ {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape J C] :
                          CategoryTheory.Limits.PreservesColimitsOfShape J CategoryTheory.ShortComplex.π₃
                          Equations
                          • CategoryTheory.ShortComplex.instPreservesColimitsOfShapeShortComplexInstCategoryShortComplexπ₃ = CategoryTheory.Limits.PreservesColimitsOfShape.mk
                          source
                          instance CategoryTheory.ShortComplex.hasFiniteColimits {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] :
                          CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.ShortComplex C)
                          Equations
                          source
                          noncomputable instance CategoryTheory.ShortComplex.instPreservesFiniteColimitsShortComplexInstCategoryShortComplexπ₁ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] :
                          CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex.π₁
                          Equations
                          • CategoryTheory.ShortComplex.instPreservesFiniteColimitsShortComplexInstCategoryShortComplexπ₁ = CategoryTheory.Limits.PreservesFiniteColimits.mk
                          source
                          noncomputable instance CategoryTheory.ShortComplex.instPreservesFiniteColimitsShortComplexInstCategoryShortComplexπ₂ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] :
                          CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex.π₂
                          Equations
                          • CategoryTheory.ShortComplex.instPreservesFiniteColimitsShortComplexInstCategoryShortComplexπ₂ = CategoryTheory.Limits.PreservesFiniteColimits.mk
                          source
                          noncomputable instance CategoryTheory.ShortComplex.instPreservesFiniteColimitsShortComplexInstCategoryShortComplexπ₃ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] :
                          CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex.π₃
                          Equations
                          • CategoryTheory.ShortComplex.instPreservesFiniteColimitsShortComplexInstCategoryShortComplexπ₃ = CategoryTheory.Limits.PreservesFiniteColimits.mk
                          source
                          instance CategoryTheory.ShortComplex.preservesEpimorphisms_π₁ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingSpan C] :
                          CategoryTheory.Functor.PreservesEpimorphisms CategoryTheory.ShortComplex.π₁
                          Equations
                          source
                          instance CategoryTheory.ShortComplex.preservesEpimorphisms_π₂ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingSpan C] :
                          CategoryTheory.Functor.PreservesEpimorphisms CategoryTheory.ShortComplex.π₂
                          Equations
                          source
                          instance CategoryTheory.ShortComplex.preservesEpimorphisms_π₃ {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingSpan C] :
                          CategoryTheory.Functor.PreservesEpimorphisms CategoryTheory.ShortComplex.π₃
                          Equations