Theorems · Definition · category theory

CategoryTheory.Limits.IsColimit.mapCoconeEquiv

{J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {K : CategoryTheory.Functor J C} →
              {F G : CategoryTheory.Functor C D} →
                (F ≅ G) →
                  {c : CategoryTheory.Limits.Cocone K} →
                    CategoryTheory.Limits.IsColimit (F.mapCocone c) → CategoryTheory.Limits.IsColimit (G.mapCocone c)

If F and G are naturally isomorphic, then F.mapCocone c being a colimit implies G.mapCocone c is also a colimit.

Defined in

Mathlib.CategoryTheory.Limits.IsLimit

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category