Equalizers of ind-objects

The eventual goal of this file is to show that if a category C has equalizers, then ind-objects are closed under equalizers. For now, it contains one of the main prerequisites, namely we show that under sufficient conditions the limit of a diagram in I ⥤ C taken in Cᵒᵖ ⥤ Type v is an ind-object.

References

• M. Kashiwara, P. Schapira, Categories and Sheaves, Section 6.1

theorem CategoryTheory.Limits.isIndObject_limit_comp_yoneda_comp_colim {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type v} [CategoryTheory.SmallCategory I] [CategoryTheory.IsFiltered I] {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J (CategoryTheory.Functor I C)) (hF : ∀ (i : I), CategoryTheory.Limits.IsIndObject (CategoryTheory.Limits.limit ((F.flip.obj i).comp CategoryTheory.yoneda))) : CategoryTheory.Limits.IsIndObject (CategoryTheory.Limits.limit (F.comp (((CategoryTheory.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 [KS06].