Theorems · Definition · category theory

CategoryTheory.Limits.ColimitPresentation.bind

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      {I : J → Type w} →
        [inst_1 : CategoryTheory.SmallCategory J] →
          [inst_2 : (j : J) → CategoryTheory.SmallCategory (I j)] →
            {X : C} →
              (P : CategoryTheory.Limits.ColimitPresentation J X) →
                (Q : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (P.diag.obj j)) →
                  [∀ (j : J), CategoryTheory.IsFiltered (I j)] →
                    [∀ (j : J) (i : I j), CategoryTheory.IsFinitelyPresentable ((Q j).diag.obj i)] →
                      CategoryTheory.Limits.ColimitPresentation (CategoryTheory.Limits.ColimitPresentation.Total Q) X

If P is a colimit presentation over J of X and for every j we are given a colimit presentation Qⱼ over I j of the P.diag.obj j, this is the refined colimit presentation of X over Total Q.

Defined in

Mathlib.CategoryTheory.Presentable.ColimitPresentation

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.SmallCategoryCategoryTheory.SmallCategoryCategoryTheory.IsFilteredCategoryTheory.IsFinitelyPresentable