Theorems · Definition · category theory

CategoryTheory.Limits.fiberwiseColim

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (F : CategoryTheory.Functor C CategoryTheory.Cat) →
      (H : Type u₂) →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} H] →
          [∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] →
            CategoryTheory.Functor (CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)
              (CategoryTheory.Functor C H)

Similar to colimit and colim, taking fiberwise colimits is a functor (Grothendieck F ⥤ H) ⥤ (C ⥤ H) between functor categories.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Cited by

9 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasColimitsOfShape