Theorems · Definition · category theory

CategoryTheory.preservesColimitNatIso

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {J : Type w} →
            [inst_2 : CategoryTheory.Category.{w', w} J] →
              [CategoryTheory.Limits.PreservesColimitsOfShape J G] →
                [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J D] →
                  [inst_5 : CategoryTheory.Limits.HasColimitsOfShape J C] →
                    CategoryTheory.Limits.colim.comp G ≅
                      ((CategoryTheory.Functor.whiskeringRight J C D).obj G).comp CategoryTheory.Limits.colim

If C, D has all colimits of shape J, and G preserves them, then preservesColimitIso is functorial w.r.t. F.

Defined in

Mathlib.CategoryTheory.Limits.Preserves.Limits

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.PreservesColimitsOfShapeCategoryTheory.Limits.HasColimitsOfShapeCategoryTheory.Limits.HasColimitsOfShape