The category of Ind-objects

We define the v-category of Ind-objects of a category C, called Ind C, as well as the functors Ind.yoneda : C ⥤ Ind C and Ind.inclusion C : Ind C ⥤ Cᵒᵖ ⥤ Type v.

This file will mainly collect results about ind-objects (stated in terms of IsIndObject) and reinterpret them in terms of Ind C. For now, we show that Ind C has filtered colimits and that Ind.inclusion C creates them. Many other limit-colimit properties will follow.

References

• M. Kashiwara, P. Schapira, Categories and Sheaves, Chapter 6

def CategoryTheory.Ind (C : Type u) [CategoryTheory.Category.{v, u} C] : Type (max u (v + 1))

The category of Ind-objects of C.

Equations

• CategoryTheory.Ind C = CategoryTheory.ShrinkHoms.{max ?u.15 (?u.16 + 1)} (CategoryTheory.FullSubcategory CategoryTheory.Limits.IsIndObject)

noncomputable instance CategoryTheory.instCategoryInd {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Category.{v, max u (v + 1)} (CategoryTheory.Ind C)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Ind.equivalence (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Ind C ≌ CategoryTheory.FullSubcategory CategoryTheory.Limits.IsIndObject

The defining properties of Ind C are that its morphisms live in v and that it is equivalent to the full subcategory of Cᵒᵖ ⥤ Type v containing the ind-objects.

Equations

• CategoryTheory.Ind.equivalence C = (CategoryTheory.ShrinkHoms.equivalence (CategoryTheory.FullSubcategory CategoryTheory.Limits.IsIndObject)).symm

noncomputable def CategoryTheory.Ind.inclusion (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Ind C) (CategoryTheory.Functor Cᵒᵖ (Type v))

The canonical inclusion of ind-objects into presheaves.

Equations

• CategoryTheory.Ind.inclusion C = (CategoryTheory.Ind.equivalence C).functor.comp (CategoryTheory.fullSubcategoryInclusion CategoryTheory.Limits.IsIndObject)

instance CategoryTheory.instFullIndFunctorOppositeTypeInclusion {C : Type u} [CategoryTheory.Category.{v, u} C] : (CategoryTheory.Ind.inclusion C).Full

Equations

• ⋯ = ⋯

instance CategoryTheory.instFaithfulIndFunctorOppositeTypeInclusion {C : Type u} [CategoryTheory.Category.{v, u} C] : (CategoryTheory.Ind.inclusion C).Faithful

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Ind.yoneda {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor C (CategoryTheory.Ind C)

The inclusion of C into Ind C induced by the Yoneda embedding.

Equations

• CategoryTheory.Ind.yoneda = (CategoryTheory.FullSubcategory.lift CategoryTheory.Limits.IsIndObject CategoryTheory.yoneda ⋯).comp (CategoryTheory.Ind.equivalence C).inverse

instance CategoryTheory.instFullIndYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Ind.yoneda.Full

Equations

• ⋯ = ⋯

instance CategoryTheory.instFaithfulIndYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Ind.yoneda.Faithful

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Ind.yonedaCompInclusion {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Ind.yoneda.comp (CategoryTheory.Ind.inclusion C) ≅ CategoryTheory.yoneda

The composition C ⥤ Ind C ⥤ (Cᵒᵖ ⥤ Type v) is just the Yoneda embedding.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance CategoryTheory.instCreatesColimitsOfShapeIndFunctorOppositeTypeInclusionOfIsFiltered {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] : CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.Ind.inclusion C)

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.instHasFilteredColimitsInd {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Limits.HasFilteredColimits (CategoryTheory.Ind C)

Equations

• ⋯ = ⋯