Equalizers of ind-objects

We show that if a category C has equalizers, then ind-objects are closed under equalizers.

References

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

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

theorem CategoryTheory.Limits.closedUnderLimitsOfShape_walkingParallelPair_isIndObject {C : Type u} [Category.{v, u} C] [HasEqualizers C] : ClosedUnderLimitsOfShape WalkingParallelPair IsIndObject

If C has equalizers. then ind-objects are closed under equalizers.

This is Proposition 6.1.17(i) in [Kashiwara2006].