Theorems · Definition · category theory

CategoryTheory.Limits.IsColimit.pullbackOfHasExactColimitsOfShape

{J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    [CategoryTheory.IsConnected J] →
      {C : Type u} →
        [inst_2 : CategoryTheory.Category.{v, u} C] →
          [inst_3 : CategoryTheory.Limits.HasPullbacks C] →
            [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J C] →
              [CategoryTheory.HasExactColimitsOfShape J C] →
                {F : CategoryTheory.Functor J C} →
                  {c : CategoryTheory.Limits.Cocone F} →
                    CategoryTheory.Limits.IsColimit c →
                      {X : C} →
                        (f : X ⟶ c.pt) →
                          CategoryTheory.Limits.IsColimit
                            { pt := X,
                              ι := CategoryTheory.Limits.pullback.snd c.ι ((CategoryTheory.Functor.const J).map f) }

If c is a cocone over a functor J ⥤ C and f : X ⟶ c.pt, then for every j : J we can take the pullback of c.ι.app j and f. This gives a new cocone with cone point X, and this cocone is again a colimit cocone as long as J is connected and C has exact colimits of shape J.

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsConnectedCategoryTheory.CategoryCategoryTheory.Limits.HasPullbacksCategoryTheory.Limits.HasColimitsOfShapeCategoryTheory.HasExactColimitsOfShape