Theorems · Definition · category theory

CategoryTheory.WithInitial.isColimitEquiv

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {X : C} →
          {K : CategoryTheory.Functor J (CategoryTheory.Under X)} →
            {t : CategoryTheory.Limits.Cocone K} →
              CategoryTheory.Limits.IsColimit (CategoryTheory.WithInitial.coconeEquiv.functor.obj t) ≃
                CategoryTheory.Limits.IsColimit t

A cocone t of K : J ⥤ Under X is a colimit if and only if the corresponding cocone coconeLift t of liftFromUnder.obj K : WithInitial K ⥤ C is a colimit.

Defined in

Mathlib.CategoryTheory.WithTerminal.Cone

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category