Ind-objects

For a presheaf A : Cᵒᵖ ⥤ Type v we define the type IndObjectPresentation A of presentations of A as a small filtered colimit of representable presheaves and define the predicate IsIndObject A asserting that there is at least one such presentation.

A presheaf is an ind-object if and only if the category CostructuredArrow yoneda A is filtered and finally small. In this way, CostructuredArrow yoneda A can be thought of the universal indexing category for the representation of A as a small filtered colimit of representable presheaves.

Future work

There are various useful ways to understand natural transformations between ind-objects in terms of their presentations.

The ind-objects form a locally v-small category IndCategory C which has numerous interesting properties.

Implementation notes

One might be tempted to introduce another universe parameter and consider being a w-ind-object as a property of presheaves C ⥤ TypeMax.{v, w}. This comes with significant technical hurdles. The recommended alternative is to consider ind-objects over ULiftHom.{w} C instead.

References

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

structure CategoryTheory.Limits.IndObjectPresentation {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) : Type (max u (v + 1))

The data that witnesses that a presheaf A is an ind-object. It consists of a small filtered indexing category I, a diagram F : I ⥤ C and the data for a colimit cocone on F ⋙ yoneda : I ⥤ Cᵒᵖ ⥤ Type v with cocone point A.

• I : Type v

  The indexing category of the filtered colimit presentation

• ℐ : CategoryTheory.SmallCategory self.I

  The indexing category of the filtered colimit presentation

• hI : CategoryTheory.IsFiltered self.I
• F : CategoryTheory.Functor self.I C

  The diagram of the filtered colimit presentation

• ι : CategoryTheory.Functor.comp self.F CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const self.I).obj A

  Use IndObjectPresentation.cocone instead.

• isColimit : CategoryTheory.Limits.IsColimit { pt := A, ι := self.ι }

  Use IndObjectPresenation.coconeIsColimit instead.

instance CategoryTheory.Limits.IndObjectPresentation.instSmallCategoryI {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) : CategoryTheory.SmallCategory P.I

Equations

• CategoryTheory.Limits.IndObjectPresentation.instSmallCategoryI P = P.ℐ

instance CategoryTheory.Limits.IndObjectPresentation.instIsFilteredIInstSmallCategoryI {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) : CategoryTheory.IsFiltered P.I

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.cocone_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) : (CategoryTheory.Limits.IndObjectPresentation.cocone P).pt = A

def CategoryTheory.Limits.IndObjectPresentation.cocone {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp P.F CategoryTheory.yoneda)

The (colimit) cocone with cocone point A.

Equations

• CategoryTheory.Limits.IndObjectPresentation.cocone P = { pt := A, ι := P.ι }

def CategoryTheory.Limits.IndObjectPresentation.coconeIsColimit {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.IndObjectPresentation.cocone P)

P.cocone is a colimit cocone.

Equations

• CategoryTheory.Limits.IndObjectPresentation.coconeIsColimit P = P.isColimit

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow_obj_left {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) (X : P.I) : ((CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow P).obj X).left = P.F.obj X

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow_map_left {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) : ∀ {X Y : P.I} (f : X ⟶ Y), ((CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow P).map f).left = P.F.map f

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow_obj_right_as {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) (X : P.I) : ((CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow P).obj X).right.as = PUnit.unit

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow_obj_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) (X : P.I) : ((CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow P).obj X).hom = (CategoryTheory.Limits.IndObjectPresentation.cocone P).ι.app X

def CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) : CategoryTheory.Functor P.I (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)

The canonical comparison functor between the indexing category of the presentation and the comma category CostructuredArrow yoneda A. This functor is always final.

Equations

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

instance CategoryTheory.Limits.IndObjectPresentation.instFinalIInstSmallCategoryICostructuredArrowFunctorOppositeOppositeTypeTypesCategoryYonedaInstCategoryCostructuredArrowToCostructuredArrow {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) : CategoryTheory.Functor.Final (CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow P)

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.yoneda_isColimit_desc {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (s : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.comp (CategoryTheory.Functor.fromPUnit X) CategoryTheory.yoneda)) : (CategoryTheory.Limits.IndObjectPresentation.yoneda X).isColimit.desc s = s.ι.app { as := PUnit.unit }

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.yoneda_ℐ {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.Limits.IndObjectPresentation.yoneda X).ℐ = CategoryTheory.discreteCategory PUnit.{v + 1}

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.yoneda_I {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.Limits.IndObjectPresentation.yoneda X).I = CategoryTheory.Discrete PUnit.{v + 1}

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.yoneda_ι_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (s : CategoryTheory.Discrete PUnit.{v + 1} ) : (CategoryTheory.Limits.IndObjectPresentation.yoneda X).ι.app s = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.comp (CategoryTheory.Functor.fromPUnit X) CategoryTheory.yoneda).obj s)

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.yoneda_F {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.Limits.IndObjectPresentation.yoneda X).F = CategoryTheory.Functor.fromPUnit X

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

Representable presheaves are (trivially) ind-objects.

Equations

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

structure CategoryTheory.Limits.IsIndObject {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) : Prop

A presheaf is called an ind-object if it can be written as a filtered colimit of representable presheaves.

• mk' :: (
• nonempty_presentation : Nonempty (CategoryTheory.Limits.IndObjectPresentation A)
• )

theorem CategoryTheory.Limits.IsIndObject.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) : CategoryTheory.Limits.IsIndObject A

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

Representable presheaves are (trivially) ind-objects.

noncomputable def CategoryTheory.Limits.IsIndObject.presentation {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} : CategoryTheory.Limits.IsIndObject A → CategoryTheory.Limits.IndObjectPresentation A

Pick a presentation for an ind-object using choice.

Equations

• CategoryTheory.Limits.IsIndObject.presentation x = match x with | ⋯ => Nonempty.some P

theorem CategoryTheory.Limits.IsIndObject.isFiltered {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (h : CategoryTheory.Limits.IsIndObject A) : CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)

theorem CategoryTheory.Limits.IsIndObject.finallySmall {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (h : CategoryTheory.Limits.IsIndObject A) : CategoryTheory.FinallySmall (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)

theorem CategoryTheory.Limits.isIndObject_of_isFiltered_of_finallySmall {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) [CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)] [CategoryTheory.FinallySmall (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)] : CategoryTheory.Limits.IsIndObject A

theorem CategoryTheory.Limits.isIndObject_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v)) : CategoryTheory.Limits.IsIndObject A ↔ CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) ∧ CategoryTheory.FinallySmall (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)

The recognition theorem for ind-objects: A : Cᵒᵖ ⥤ Type v is an ind-object if and only if CostructuredArrow yoneda A is filtered and finally v-small.

Theorem 6.1.5 of [Kashiwara2006]