Documentation

Mathlib.CategoryTheory.Limits.Indization.IndObject

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 #

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 Fyoneda : I ⥤ Cᵒᵖ ⥤ Type v with cocone point A.

Instances For

    The (colimit) cocone with cocone point A.

    Equations
    • P.cocone = { pt := A, ι := P }
    Instances For
      @[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_ι_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)

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

      Equations
      Instances For

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

        Equations
        Instances For

          Representable presheaves are (trivially) ind-objects.

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

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

            Instances For

              Representable presheaves are (trivially) ind-objects.

              Pick a presentation for an ind-object using choice.

              Equations
              • x.presentation = match x with | => P.some
              Instances For

                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]