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.

Adopting the theorem numbering of [Kashiwara2006], we show that

• Ind C has filtered colimits (6.1.8),
• Ind C ⥤ Cᵒᵖ ⥤ Type v creates filtered colimits (6.1.8),
• C ⥤ Ind C preserves finite colimits (6.1.6),
• if C has coproducts indexed by a finite type α, then Ind C has coproducts indexed by α (6.1.18(ii)),
• if C has finite coproducts, then Ind C has small coproducts (6.1.18(ii)),
• if C has products indexed by α, then Ind C has products indexed by α, and the functor Ind C ⥤ Cᵒᵖ ⥤ Type v creates such products (6.1.17)
• the functor C ⥤ Ind C preserves small limits.

More limit-colimit properties will follow.

Note that:

• the functor Ind C ⥤ Cᵒᵖ ⥤ Type v does not preserve any kind of colimit in general except for filtered colimits and
• the functor C ⥤ Ind C preserves finite colimits, but not infinite colimits in general.

References

• [M. Kashiwara, P. Schapira, Categories and Sheaves][Kashiwara2006], 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

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

noncomputable def CategoryTheory.Ind.inclusion.fullyFaithful {C : Type u} [CategoryTheory.Category.{v, u} C] : (CategoryTheory.Ind.inclusion C).FullyFaithful

The functor Ind C ⥤ Cᵒᵖ ⥤ Type v is fully faithful.

Equations

• CategoryTheory.Ind.inclusion.fullyFaithful = CategoryTheory.Functor.FullyFaithful.ofFullyFaithful (CategoryTheory.Ind.inclusion C)

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

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

noncomputable def CategoryTheory.Ind.yoneda.fullyFaithful {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Ind.yoneda.FullyFaithful

The functor C ⥤ Ind C is fully faithful.

Equations

• CategoryTheory.Ind.yoneda.fullyFaithful = CategoryTheory.Functor.FullyFaithful.ofFullyFaithful CategoryTheory.Ind.yoneda

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)

noncomputable instance CategoryTheory.instCreatesLimitsOfShapeIndFunctorOppositeTypeDiscreteInclusionOfHasLimitsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type v} [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) C] : CategoryTheory.CreatesLimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.Ind.inclusion C)

Equations

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

instance CategoryTheory.instHasLimitsOfShapeDiscreteInd {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type v} [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) C] : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.Ind C)

instance CategoryTheory.instPreservesLimitsIndYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Limits.PreservesLimits CategoryTheory.Ind.yoneda

theorem CategoryTheory.Ind.isIndObject_inclusion_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Ind C) : CategoryTheory.Limits.IsIndObject ((CategoryTheory.Ind.inclusion C).obj X)

noncomputable def CategoryTheory.Ind.presentation {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Ind C) : CategoryTheory.Limits.IndObjectPresentation ((CategoryTheory.Ind.inclusion C).obj X)

Pick a presentation of an ind-object X using choice.

Equations

• X.presentation = ⋯.presentation

noncomputable def CategoryTheory.Ind.colimitPresentationCompYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Ind C) : CategoryTheory.Limits.colimit (X.presentation.F.comp CategoryTheory.Ind.yoneda) ≅ X

An ind-object X is the colimit (in Ind C!) of the filtered diagram presenting it.

Equations

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

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

instance CategoryTheory.instPreservesFiniteColimitsIndYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.Ind.yoneda

instance CategoryTheory.instHasColimitsOfShapeDiscreteIndOfFinite {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Type v} [Finite α] [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) C] : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) (CategoryTheory.Ind C)

instance CategoryTheory.instHasCoproductsIndOfHasFiniteCoproducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteCoproducts C] : CategoryTheory.Limits.HasCoproducts (CategoryTheory.Ind C)