Theorems · Definition · category theory

CategoryTheory.Limits.isColimitOfReflects

{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 (F.mapCocone c) →
                    [CategoryTheory.Limits.ReflectsColimit K F] → CategoryTheory.Limits.IsColimit c

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

Defined in

Mathlib.CategoryTheory.Limits.Preserves.Basic

Cited by

19 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.ReflectsColimit