Theorems · Definition · category theory

CategoryTheory.Limits.isColimitOfPreserves

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              (F : CategoryTheory.Functor C D) →
                {c : CategoryTheory.Limits.Cocone K} →
                  CategoryTheory.Limits.IsColimit c →
                    [CategoryTheory.Limits.PreservesColimit K F] → CategoryTheory.Limits.IsColimit (F.mapCocone c)

A convenience function for PreservesColimit, which takes the functor as an explicit argument to guide typeclass resolution.

Defined in

Mathlib.CategoryTheory.Limits.Preserves.Basic

Cited by

118 results in Mathlib

Foundations

Depth 32 from the axioms, rests on 121 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.PreservesColimit