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 [KS06], 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, Chapter 6

def CategoryTheory.Ind (C : Type u) [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} [Category.{v, u} C] : Category.{v, max u (v + 1)} (Ind C)

Equations

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

noncomputable def CategoryTheory.Ind.equivalence (C : Type u) [Category.{v, u} C] : Ind C ≌ FullSubcategory 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) [Category.{v, u} C] : Functor (Ind C) (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} [Category.{v, u} C] : (Ind.inclusion C).Full

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

noncomputable def CategoryTheory.Ind.inclusion.fullyFaithful {C : Type u} [Category.{v, u} C] : (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} [Category.{v, u} C] : Functor C (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} [Category.{v, u} C] : Ind.yoneda.Full

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

noncomputable def CategoryTheory.Ind.yoneda.fullyFaithful {C : Type u} [Category.{v, u} C] : 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} [Category.{v, u} C] : Ind.yoneda.comp (Ind.inclusion C) ≅ 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} [Category.{v, u} C] {J : Type v} [SmallCategory J] [IsFiltered J] : CreatesColimitsOfShape J (Ind.inclusion C)

Equations

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

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

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

Equations

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

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

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

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

noncomputable def CategoryTheory.Ind.presentation {C : Type u} [Category.{v, u} C] (X : Ind C) : Limits.IndObjectPresentation ((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} [Category.{v, u} C] (X : Ind C) : Limits.colimit (X.presentation.F.comp 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} [Category.{v, u} C] : RepresentablyCoflat Ind.yoneda

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

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

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