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

• ℐ : SmallCategory self.I

  The indexing category of the filtered colimit presentation

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

  The diagram of the filtered colimit presentation

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

  Use IndObjectPresentation.cocone instead.

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

  Use IndObjectPresentation.coconeIsColimit instead.

def CategoryTheory.Limits.IndObjectPresentation.ofCocone {C : Type u} [Category.{v, u} C] {I : Type v} [SmallCategory I] [IsFiltered I] {F : Functor I C} (c : Cocone (F.comp CategoryTheory.yoneda)) (hc : IsColimit c) : IndObjectPresentation c.pt

Alternative constructor for IndObjectPresentation taking a cocone instead of its defining natural transformation.

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.ofCocone_I {C : Type u} [Category.{v, u} C] {I : Type v} [SmallCategory I] [IsFiltered I] {F : Functor I C} (c : Cocone (F.comp CategoryTheory.yoneda)) (hc : IsColimit c) : (ofCocone c hc).I = I

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.ofCocone_ι {C : Type u} [Category.{v, u} C] {I : Type v} [SmallCategory I] [IsFiltered I] {F : Functor I C} (c : Cocone (F.comp CategoryTheory.yoneda)) (hc : IsColimit c) : (ofCocone c hc).ι = c.ι

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.ofCocone_F {C : Type u} [Category.{v, u} C] {I : Type v} [SmallCategory I] [IsFiltered I] {F : Functor I C} (c : Cocone (F.comp CategoryTheory.yoneda)) (hc : IsColimit c) : (ofCocone c hc).F = F

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.ofCocone_isColimit {C : Type u} [Category.{v, u} C] {I : Type v} [SmallCategory I] [IsFiltered I] {F : Functor I C} (c : Cocone (F.comp CategoryTheory.yoneda)) (hc : IsColimit c) : (ofCocone c hc).isColimit = hc

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.ofCocone_ℐ {C : Type u} [Category.{v, u} C] {I : Type v} [SmallCategory I] [IsFiltered I] {F : Functor I C} (c : Cocone (F.comp CategoryTheory.yoneda)) (hc : IsColimit c) : (ofCocone c hc).ℐ = inst✝

@[implicit_reducible]

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

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

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

The (colimit) cocone with cocone point A.

@[simp]

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

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

P.cocone is a colimit cocone.

noncomputable def CategoryTheory.Limits.IndObjectPresentation.extend {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ (Type v)} (P : IndObjectPresentation A) (η : A ⟶ B) [IsIso η] : IndObjectPresentation B

If A and B are isomorphic, then an ind-object presentation of A can be extended to an ind-object presentation of B.

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.extend_ι_app_app {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ (Type v)} (P : IndObjectPresentation A) (η : A ⟶ B) [IsIso η] (X : P.I) (X✝ : Cᵒᵖ) (a✝ : ((P.F.comp CategoryTheory.yoneda).obj X).obj X✝) : ((P.extend η).ι.app X).app X✝ a✝ = η.app X✝ ((P.cocone.ι.app X).app X✝ a✝)

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.extend_ℐ {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ (Type v)} (P : IndObjectPresentation A) (η : A ⟶ B) [IsIso η] : (P.extend η).ℐ = P.ℐ

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.extend_isColimit_desc_app {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ (Type v)} (P : IndObjectPresentation A) (η : A ⟶ B) [IsIso η] (s : Cocone (P.F.comp CategoryTheory.yoneda)) (X : Cᵒᵖ) (a✝ : (P.cocone.extend η).pt.obj X) : ((P.extend η).isColimit.desc s).app X a✝ = (P.coconeIsColimit.desc s).app X (inv (η.app X) a✝)

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.extend_F {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ (Type v)} (P : IndObjectPresentation A) (η : A ⟶ B) [IsIso η] : (P.extend η).F = P.F

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.extend_I {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ (Type v)} (P : IndObjectPresentation A) (η : A ⟶ B) [IsIso η] : (P.extend η).I = P.I

def CategoryTheory.Limits.IndObjectPresentation.toCostructuredArrow {C : Type u} [Category.{v, u} C] {A : Functor Cᵒᵖ (Type v)} (P : IndObjectPresentation A) : Functor P.I (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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Representable presheaves are (trivially) ind-objects.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

structure CategoryTheory.Limits.IsIndObject {C : Type u} [Category.{v, u} C] (A : 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 (IndObjectPresentation A)
• )

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

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

Representable presheaves are (trivially) ind-objects.

theorem CategoryTheory.Limits.IsIndObject.map {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ (Type v)} (η : A ⟶ B) [IsIso η] : IsIndObject A → IsIndObject B

theorem CategoryTheory.Limits.IsIndObject.iff_of_iso {C : Type u} [Category.{v, u} C] {A B : Functor Cᵒᵖ (Type v)} (η : A ⟶ B) [IsIso η] : IsIndObject A ↔ IsIndObject B

instance CategoryTheory.Limits.IsIndObject.instIsClosedUnderIsomorphismsFunctorOppositeType {C : Type u} [Category.{v, u} C] : ObjectProperty.IsClosedUnderIsomorphisms IsIndObject

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

Pick a presentation for an ind-object using choice.

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

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

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

theorem CategoryTheory.Limits.isIndObject_iff {C : Type u} [Category.{v, u} C] (A : Functor Cᵒᵖ (Type v)) : IsIndObject A ↔ IsFiltered (CostructuredArrow yoneda A) ∧ FinallySmall (CostructuredArrow 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]

theorem CategoryTheory.Limits.isIndObject_limit_comp_yoneda {C : Type u} [Category.{v, u} C] {J : Type u'} [Category.{v', u'} J] (F : Functor J C) [HasLimit F] : IsIndObject (limit (F.comp yoneda))

If a limit already exists in C, then the limit of the image of the diagram under the Yoneda embedding is an ind-object.

theorem CategoryTheory.Limits.isIndObject_iff_preservesFiniteLimits {C : Type u} [SmallCategory C] [HasFiniteColimits C] (A : Functor Cᵒᵖ (Type u)) : IsIndObject A ↔ PreservesFiniteLimits A

Presheaves over a small finitely cocomplete category C : Type u are Ind-objects if and only if they are left-exact.