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.

For a small filtered category I, we also define Ind.lim I : (I ⥤ C) ⥤ Ind C and show that it preserves finite limits and finite colimits.

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 the following properties:

Limits:

• 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),
• if C has equalizers, then Ind C has equalizers, and the functor Ind C ⥤ Cᵒᵖ ⥤ Type v creates them (6.1.17)
• if C has small limits (resp. finite limits), then Ind C has small limits (resp. finite limits) and the functor Ind C ⥤ Cᵒᵖ ⥤ Type v creates them (6.1.17),
• the functor C ⥤ Ind C preserves small limits (6.1.17).

Colimits:

• Ind C has filtered colimits (6.1.8), and the functor Ind C ⥤ Cᵒᵖ ⥤ Type v preserves filtered colimits,
• 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 coequalizers, then Ind C has coequalizers (6.1.18(i)),
• if C has finite colimits, then Ind C has small colimits (6.1.18(iii)).
• C ⥤ Ind C preserves finite colimits (6.1.6),

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

The category of Ind-objects of C.

Equations

• CategoryTheory.Ind C = CategoryTheory.ShrinkHoms.{max ?u.10 (?u.11 + 1)} (CategoryTheory.ObjectProperty.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 ≌ ObjectProperty.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.ObjectProperty.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.ObjectProperty.ι 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.ObjectProperty.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)

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

Equations

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

instance CategoryTheory.instHasLimitsOfShapeWalkingParallelPairInd {C : Type u} [Category.{v, u} C] [Limits.HasLimitsOfShape Limits.WalkingParallelPair C] : Limits.HasLimitsOfShape Limits.WalkingParallelPair (Ind C)

noncomputable instance CategoryTheory.instCreatesFiniteLimitsIndFunctorOppositeTypeInclusionOfHasFiniteLimits {C : Type u} [Category.{v, u} C] [Limits.HasFiniteLimits C] : Limits.CreatesFiniteLimits (Ind.inclusion C)

Equations

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

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

noncomputable instance CategoryTheory.instCreatesLimitsOfSizeIndFunctorOppositeTypeInclusionOfHasLimits {C : Type u} [Category.{v, u} C] [Limits.HasLimits C] : CreatesLimitsOfSize.{v, v, v, max u v, max u (v + 1), max u (v + 1)} (Ind.inclusion C)

Equations

• CategoryTheory.instCreatesLimitsOfSizeIndFunctorOppositeTypeInclusionOfHasLimits = CategoryTheory.Limits.createsLimitsOfSizeOfCreatesEqualizersAndProducts (CategoryTheory.Ind.inclusion C)

instance CategoryTheory.instHasLimitsInd {C : Type u} [Category.{v, u} C] [Limits.HasLimits C] : Limits.HasLimits (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

noncomputable def CategoryTheory.Ind.lim {C : Type u} [Category.{v, u} C] (I : Type v) [SmallCategory I] [IsFiltered I] : Functor (Functor I C) (Ind C)

This is the functor (I ⥤ C) ⥤ Ind C that sends a functor F to colim (Y ∘ F), where Y is the Yoneda embedding. It is known as "ind-lim" and denoted “colim” in [Kashiwara2006].

Equations

• CategoryTheory.Ind.lim I = ((CategoryTheory.whiskeringRight I C (CategoryTheory.Ind C)).obj CategoryTheory.Ind.yoneda).comp CategoryTheory.Limits.colim

noncomputable def CategoryTheory.Ind.limCompInclusion {C : Type u} [Category.{v, u} C] {I : Type v} [SmallCategory I] [IsFiltered I] : (Ind.lim I).comp (Ind.inclusion C) ≅ ((whiskeringRight I C (Functor Cᵒᵖ (Type v))).obj yoneda).comp Limits.colim

Computing ind-lims in Ind C is the same as computing them in Cᵒᵖ ⥤ Type v.

Equations

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

instance CategoryTheory.instPreservesLimitsOfShapeFunctorIndLimOfFinCategoryOfHasLimitsOfShape {C : Type u} [Category.{v, u} C] {α : Type w} [SmallCategory α] [FinCategory α] [Limits.HasLimitsOfShape α C] {I : Type v} [SmallCategory I] [IsFiltered I] : Limits.PreservesLimitsOfShape α (Ind.lim I)

instance CategoryTheory.instPreservesColimitsOfShapeFunctorIndLimOfFinCategoryOfHasColimitsOfShape {C : Type u} [Category.{v, u} C] {α : Type w} [SmallCategory α] [FinCategory α] [Limits.HasColimitsOfShape α C] {I : Type v} [SmallCategory I] [IsFiltered I] : Limits.PreservesColimitsOfShape α (Ind.lim I)

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)

noncomputable def CategoryTheory.IndParallelPairPresentation.parallelPairIsoParallelPairCompIndYoneda {C : Type u} [Category.{v, u} C] {A B : Ind C} {f g : A ⟶ B} (P : IndParallelPairPresentation ((Ind.inclusion C).map f) ((Ind.inclusion C).map g)) : Limits.parallelPair f g ≅ (Limits.parallelPair P.φ P.ψ).comp (Ind.lim P.I)

Given an IndParallelPairPresentation f g, we can understand the parallel pair (f, g) as the colimit of (P.φ, P.ψ) in Ind C.

Equations

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

instance CategoryTheory.instHasColimitsOfShapeWalkingParallelPairInd {C : Type u} [Category.{v, u} C] [Limits.HasColimitsOfShape Limits.WalkingParallelPair C] : Limits.HasColimitsOfShape Limits.WalkingParallelPair (Ind C)

instance CategoryTheory.instHasColimitsIndOfHasFiniteColimits {C : Type u} [Category.{v, u} C] [Limits.HasFiniteColimits C] : Limits.HasColimits (Ind C)

theorem CategoryTheory.Ind.exists_nonempty_arrow_mk_iso_ind_lim {C : Type u} [Category.{v, u} C] {A B : Ind C} {f : A ⟶ B} : ∃ (I : Type v) (x : SmallCategory I) (x_1 : IsFiltered I) (F : Functor I C) (G : Functor I C) (φ : F ⟶ G), Nonempty (Arrow.mk f ≅ Arrow.mk ((Ind.lim I).map φ))

A way to understand morphisms in Ind C: every morphism is induced by a natural transformation of diagrams.

noncomputable def CategoryTheory.Ind.leftExactFunctorEquivalence (C : Type u) [SmallCategory C] [Limits.HasFiniteColimits C] : Ind C ≌ Cᵒᵖ ⥤ₗ Type u

For small finitely cocomplete categories C : Type u, the category of Ind-objects Ind C is equivalent to the category of left-exact functors Cᵒᵖ ⥤ Type u

Equations

• CategoryTheory.Ind.leftExactFunctorEquivalence C = (CategoryTheory.Ind.equivalence C).trans (CategoryTheory.ObjectProperty.fullSubcategoryCongr ⋯)