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

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

  Use IndObjectPresentation.cocone instead.

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

  Use IndObjectPresenation.coconeIsColimit instead.

theorem CategoryTheory.Limits.IndObjectPresentation.hI {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (self : CategoryTheory.Limits.IndObjectPresentation A) : CategoryTheory.IsFiltered self.I

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.IndObjectPresentation.ofCocone c hc = CategoryTheory.Limits.IndObjectPresentation.mk I F c.ι hc

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

• P.instSmallCategoryI = P.ℐ

instance CategoryTheory.Limits.IndObjectPresentation.instIsFilteredI {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) : P.cocone.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 (P.F.comp CategoryTheory.yoneda)

The (colimit) cocone with cocone point A.

Equations

• P.cocone = { 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 P.cocone

P.cocone is a colimit cocone.

Equations

• P.coconeIsColimit = P.isColimit

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.extend_isColimit_desc_app {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {B : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) (η : A ⟶ B) [CategoryTheory.IsIso η] (s : CategoryTheory.Limits.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 (CategoryTheory.inv (η.app X) a)

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.IndObjectPresentation.extend_ι_app_app {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {B : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) (η : A ⟶ B) [CategoryTheory.IsIso η] (X : P.I) (X : Cᵒᵖ) : ∀ (a : ((Opposite.unop (Opposite.op (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_F {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {B : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) (η : A ⟶ B) [CategoryTheory.IsIso η] : (P.extend η).F = P.F

noncomputable def CategoryTheory.Limits.IndObjectPresentation.extend {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {B : CategoryTheory.Functor Cᵒᵖ (Type v)} (P : CategoryTheory.Limits.IndObjectPresentation A) (η : A ⟶ B) [CategoryTheory.IsIso η] : CategoryTheory.Limits.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.

Equations

• P.extend η = CategoryTheory.Limits.IndObjectPresentation.ofCocone (P.cocone.extend η) (CategoryTheory.Limits.IsColimit.extendIso η P.coconeIsColimit)

@[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) : (P.toCostructuredArrow.obj X).hom = P.cocone.ι.app 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), (P.toCostructuredArrow.map f).left = P.F.map f

@[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) : (P.toCostructuredArrow.obj X).left = P.F.obj X

@[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) : (P.toCostructuredArrow.obj X).right.as = PUnit.unit

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

• P.toCostructuredArrow = P.cocone.toCostructuredArrow.comp (CategoryTheory.CostructuredArrow.pre P.F CategoryTheory.yoneda P.cocone.pt)

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

Equations

• ⋯ = ⋯

@[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_F {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.Limits.IndObjectPresentation.yoneda X).F = CategoryTheory.Functor.fromPUnit X

@[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.fromPUnit X).comp CategoryTheory.yoneda).obj s)

@[simp]

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

@[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}

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.nonempty_presentation {C : Type u} [CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (self : CategoryTheory.Limits.IsIndObject A) : 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.

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

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

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

• x.presentation = match x with | ⋯ => P.some

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]