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.

source
def CategoryTheory.ShortComplex.isLimitOfIsLimitπ {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] {F : Functor J (ShortComplex C)} (c : Limits.Cone F) (h₁ : Limits.IsLimit (π₁.mapCone c)) (h₂ : Limits.IsLimit (π₂.mapCone c)) (h₃ : Limits.IsLimit (π₃.mapCone c)) :
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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasLimit (F.comp π₁)] [Limits.HasLimit (F.comp π₂)] [Limits.HasLimit (F.comp π₃)] :
    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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasLimit (F.comp π₁)] [Limits.HasLimit (F.comp π₂)] [Limits.HasLimit (F.comp π₃)] :
      Limits.IsLimit (π₁.mapCone (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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasLimit (F.comp π₁)] [Limits.HasLimit (F.comp π₂)] [Limits.HasLimit (F.comp π₃)] :
        Limits.IsLimit (π₂.mapCone (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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasLimit (F.comp π₁)] [Limits.HasLimit (F.comp π₂)] [Limits.HasLimit (F.comp π₃)] :
          Limits.IsLimit (π₃.mapCone (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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasLimit (F.comp π₁)] [Limits.HasLimit (F.comp π₂)] [Limits.HasLimit (F.comp π₃)] :
            Limits.IsLimit (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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasLimit (F.comp π₁)] [Limits.HasLimit (F.comp π₂)] [Limits.HasLimit (F.comp π₃)] :
              Limits.HasLimit F
              source
              instance CategoryTheory.ShortComplex.instPreservesLimitπ₁ {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasLimit (F.comp π₁)] [Limits.HasLimit (F.comp π₂)] [Limits.HasLimit (F.comp π₃)] :
              Limits.PreservesLimit F π₁
              source
              instance CategoryTheory.ShortComplex.instPreservesLimitπ₂ {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasLimit (F.comp π₁)] [Limits.HasLimit (F.comp π₂)] [Limits.HasLimit (F.comp π₃)] :
              Limits.PreservesLimit F π₂
              source
              instance CategoryTheory.ShortComplex.instPreservesLimitπ₃ {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasLimit (F.comp π₁)] [Limits.HasLimit (F.comp π₂)] [Limits.HasLimit (F.comp π₃)] :
              Limits.PreservesLimit F π₃
              source
              instance CategoryTheory.ShortComplex.hasLimitsOfShape {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasLimitsOfShape J C] :
              Limits.HasLimitsOfShape J (ShortComplex C)
              source
              instance CategoryTheory.ShortComplex.instPreservesLimitsOfShapeπ₁ {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasLimitsOfShape J C] :
              Limits.PreservesLimitsOfShape J π₁
              source
              instance CategoryTheory.ShortComplex.instPreservesLimitsOfShapeπ₂ {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasLimitsOfShape J C] :
              Limits.PreservesLimitsOfShape J π₂
              source
              instance CategoryTheory.ShortComplex.instPreservesLimitsOfShapeπ₃ {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasLimitsOfShape J C] :
              Limits.PreservesLimitsOfShape J π₃
              source
              instance CategoryTheory.ShortComplex.hasFiniteLimits {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteLimits C] :
              Limits.HasFiniteLimits (ShortComplex C)
              source
              instance CategoryTheory.ShortComplex.instPreservesFiniteLimitsπ₁ {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteLimits C] :
              Limits.PreservesFiniteLimits π₁
              source
              instance CategoryTheory.ShortComplex.instPreservesFiniteLimitsπ₂ {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteLimits C] :
              Limits.PreservesFiniteLimits π₂
              source
              instance CategoryTheory.ShortComplex.instPreservesFiniteLimitsπ₃ {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteLimits C] :
              Limits.PreservesFiniteLimits π₃
              source
              instance CategoryTheory.ShortComplex.preservesMonomorphisms_π₁ {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasLimitsOfShape Limits.WalkingCospan C] :
              π₁.PreservesMonomorphisms
              source
              instance CategoryTheory.ShortComplex.preservesMonomorphisms_π₂ {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasLimitsOfShape Limits.WalkingCospan C] :
              π₂.PreservesMonomorphisms
              source
              instance CategoryTheory.ShortComplex.preservesMonomorphisms_π₃ {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasLimitsOfShape Limits.WalkingCospan C] :
              π₃.PreservesMonomorphisms
              source
              def CategoryTheory.ShortComplex.isColimitOfIsColimitπ {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] {F : Functor J (ShortComplex C)} (c : Limits.Cocone F) (h₁ : Limits.IsColimit (π₁.mapCocone c)) (h₂ : Limits.IsColimit (π₂.mapCocone c)) (h₃ : Limits.IsColimit (π₃.mapCocone c)) :
              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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasColimit (F.comp π₁)] [Limits.HasColimit (F.comp π₂)] [Limits.HasColimit (F.comp π₃)] :
                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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasColimit (F.comp π₁)] [Limits.HasColimit (F.comp π₂)] [Limits.HasColimit (F.comp π₃)] :
                  Limits.IsColimit (π₁.mapCocone (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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasColimit (F.comp π₁)] [Limits.HasColimit (F.comp π₂)] [Limits.HasColimit (F.comp π₃)] :
                    Limits.IsColimit (π₂.mapCocone (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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasColimit (F.comp π₁)] [Limits.HasColimit (F.comp π₂)] [Limits.HasColimit (F.comp π₃)] :
                      Limits.IsColimit (π₃.mapCocone (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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasColimit (F.comp π₁)] [Limits.HasColimit (F.comp π₂)] [Limits.HasColimit (F.comp π₃)] :
                        Limits.IsColimit (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} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasColimit (F.comp π₁)] [Limits.HasColimit (F.comp π₂)] [Limits.HasColimit (F.comp π₃)] :
                          Limits.HasColimit F
                          source
                          instance CategoryTheory.ShortComplex.instPreservesColimitπ₁ {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasColimit (F.comp π₁)] [Limits.HasColimit (F.comp π₂)] [Limits.HasColimit (F.comp π₃)] :
                          Limits.PreservesColimit F π₁
                          source
                          instance CategoryTheory.ShortComplex.instPreservesColimitπ₂ {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasColimit (F.comp π₁)] [Limits.HasColimit (F.comp π₂)] [Limits.HasColimit (F.comp π₃)] :
                          Limits.PreservesColimit F π₂
                          source
                          instance CategoryTheory.ShortComplex.instPreservesColimitπ₃ {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] (F : Functor J (ShortComplex C)) [Limits.HasColimit (F.comp π₁)] [Limits.HasColimit (F.comp π₂)] [Limits.HasColimit (F.comp π₃)] :
                          Limits.PreservesColimit F π₃
                          source
                          instance CategoryTheory.ShortComplex.hasColimitsOfShape {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasColimitsOfShape J C] :
                          Limits.HasColimitsOfShape J (ShortComplex C)
                          source
                          instance CategoryTheory.ShortComplex.instPreservesColimitsOfShapeπ₁ {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasColimitsOfShape J C] :
                          Limits.PreservesColimitsOfShape J π₁
                          source
                          instance CategoryTheory.ShortComplex.instPreservesColimitsOfShapeπ₂ {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasColimitsOfShape J C] :
                          Limits.PreservesColimitsOfShape J π₂
                          source
                          instance CategoryTheory.ShortComplex.instPreservesColimitsOfShapeπ₃ {J : Type u_1} {C : Type u_2} [Category.{u_3, u_1} J] [Category.{u_4, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasColimitsOfShape J C] :
                          Limits.PreservesColimitsOfShape J π₃
                          source
                          instance CategoryTheory.ShortComplex.hasFiniteColimits {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteColimits C] :
                          Limits.HasFiniteColimits (ShortComplex C)
                          source
                          instance CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₁ {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteColimits C] :
                          Limits.PreservesFiniteColimits π₁
                          source
                          instance CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₂ {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteColimits C] :
                          Limits.PreservesFiniteColimits π₂
                          source
                          instance CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₃ {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteColimits C] :
                          Limits.PreservesFiniteColimits π₃
                          source
                          instance CategoryTheory.ShortComplex.preservesEpimorphisms_π₁ {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasColimitsOfShape Limits.WalkingSpan C] :
                          π₁.PreservesEpimorphisms
                          source
                          instance CategoryTheory.ShortComplex.preservesEpimorphisms_π₂ {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasColimitsOfShape Limits.WalkingSpan C] :
                          π₂.PreservesEpimorphisms
                          source
                          instance CategoryTheory.ShortComplex.preservesEpimorphisms_π₃ {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasZeroMorphisms C] [Limits.HasColimitsOfShape Limits.WalkingSpan C] :
                          π₃.PreservesEpimorphisms