Theorems · Theorem · category theory

CategoryTheory.Limits.colim.exact_mapShortComplex

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C] [CategoryTheory.HasExactColimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)},
  S.Exact →
    ∀ {c₁ : CategoryTheory.Limits.Cocone S.X₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁)
      {c₂ : CategoryTheory.Limits.Cocone S.X₂} (hc₂ : CategoryTheory.Limits.IsColimit c₂)
      {c₃ : CategoryTheory.Limits.Cocone S.X₃} (hc₃ : CategoryTheory.Limits.IsColimit c₃) (f : c₁.pt ⟶ c₂.pt)
      (g : c₂.pt ⟶ c₃.pt)
      (hf :
        ∀ (j : J),
          CategoryTheory.CategoryStruct.comp (c₁.ι.app j) f =
            CategoryTheory.CategoryStruct.comp (S.f.app j) (c₂.ι.app j))
      (hg :
        ∀ (j : J),
          CategoryTheory.CategoryStruct.comp (c₂.ι.app j) g =
            CategoryTheory.CategoryStruct.comp (S.g.app j) (c₃.ι.app j)),
      (CategoryTheory.Limits.colim.mapShortComplex S hc₁ c₂ c₃ f g hf hg).Exact

Assuming HasExactColimitsOfShape J C, this lemma rephrases the exactness of the functor colim : (J ⥤ C) ⥤ C by saying that if S : ShortComplex (J ⥤ C) is exact, then the short complex obtained by taking the colimits is exact, where we allow the replacement of the chosen colimit cocones of the colimit API by arbitrary colimit cocones.

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasColimitsOfShapeCategoryTheory.HasExactColimitsOfShapeCategoryTheory.Limits.HasZeroMorphisms