Theorems · Theorem · category theory

CategoryTheory.Limits.isIndObject_limit_comp_yoneda_comp_colim

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type v} [inst_1 : CategoryTheory.SmallCategory I]
  [CategoryTheory.IsFiltered I] {J : Type} [inst_3 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor I C)),
  (∀ (i : I),
      CategoryTheory.Limits.IsIndObject (CategoryTheory.Limits.limit ((F.flip.obj i).comp CategoryTheory.yoneda))) →
    CategoryTheory.Limits.IsIndObject
      (CategoryTheory.Limits.limit
        (F.comp
          (((CategoryTheory.Functor.whiskeringRight I C (CategoryTheory.Functor Cᵒᵖ (Type v))).obj
                CategoryTheory.yoneda).comp
            CategoryTheory.Limits.colim)))

Suppose F : J ⥤ I ⥤ C is a finite diagram in the functor category I ⥤ C, where I is small and filtered. If i : I, we can apply the Yoneda embedding to F(·, i) to obtain a diagram of presheaves J ⥤ Cᵒᵖ ⥤ Type v. Suppose that the limits of this diagram is always an ind-object. For j : J we can apply the Yoneda embedding to F(j, ·) and take colimits to obtain a finite diagram J ⥤ Cᵒᵖ ⥤ Type v (which is actually a diagram J ⥤ Ind C). The theorem states that the limit of this diagram is an ind-object. This theorem will be used to construct equalizers in the category of ind-objects. It can be interpreted as saying that ind-objects are closed under finite limits as long as the diagram we are taking the limit of comes from a diagram in a functor category I ⥤ C. We will show (TODO) that this is the case for any parallel pair of morphisms in Ind C and deduce that ind-objects are closed under equalizers. This is Proposition 6.1.16(i) in [Kashiwara2006].

Defined in

Mathlib.CategoryTheory.Limits.Indization.Equalizers

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.SmallCategoryCategoryTheory.IsFilteredCategoryTheory.SmallCategoryCategoryTheory.FinCategory