Theorems · Definition · category theory

CategoryTheory.Functor.IsEventuallyConstantFrom.isColimitOfIsIso

{J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {F : CategoryTheory.Functor J C} →
          {i₀ : J} →
            F.IsEventuallyConstantFrom i₀ →
              [CategoryTheory.IsFiltered J] →
                (c : CategoryTheory.Limits.Cocone F) →
                  [CategoryTheory.IsIso (c.ι.app i₀)] → CategoryTheory.Limits.IsColimit c

Given a cocone c on a filtered diagram F which IsEventuallyConstantFrom i₀, such that c.π.app i₀ is an isomorphism, c a colimit cocone.

Defined in

Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.IsFilteredCategoryTheory.IsIso