Objects that are colimits of objects satisfying a certain property

Given a property of objects P : ObjectProperty C and a category J, we introduce two properties of objects P.strictColimitsOfShape J and P.colimitsOfShape J. The former contains exactly the objects of the form colimit F for any functor F : J ⥤ C that has a colimit and such that F.obj j satisfies P for any j, while the latter contains all the objects that are isomorphic to these "chosen" objects colimit F.

Under certain circumstances, the type of objects satisfying P.strictColimitsOfShape J is small: the main reason this variant is introduced is to deduce that the full subcategory of P.colimitsOfShape J is essentially small.

TODO

• refactor ClosedUnderColimitsOfShape J P to make it a typeclass which would say that P.colimitsOfShape J ≤ J.
• refactor ObjectProperty.ind by saying that it is the supremum of P.colimitsOfShape J for a filtered category J (generalize also to κ-filtered categories?)
• formalize the closure of P under finite colimits (which require iterating over ℕ), and more generally the closure under colimits indexed by a category whose type of arrows has a cardinality that is bounded by a certain regular cardinal (@joelriou)

inductive CategoryTheory.ObjectProperty.strictColimitsOfShape {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] : ObjectProperty C

The property of objects that are equal to colimit F for some functor F : J ⥤ C where all F.obj j satisfy P.

• colimit {C : Type u_1} [Category.{u_2, u_1} C] {P : ObjectProperty C} {J : Type u'} [Category.{v', u'} J] (F : Functor J C) [Limits.HasColimit F] (hF : ∀ (j : J), P (F.obj j)) : P.strictColimitsOfShape J (Limits.colimit F)

theorem CategoryTheory.ObjectProperty.strictColimitsOfShape_monotone {C : Type u_1} [Category.{u_2, u_1} C] {P : ObjectProperty C} (J : Type u') [Category.{v', u'} J] {Q : ObjectProperty C} (h : P ≤ Q) : P.strictColimitsOfShape J ≤ Q.strictColimitsOfShape J

structure CategoryTheory.ObjectProperty.ColimitOfShape {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] (X : C) extends CategoryTheory.Limits.ColimitPresentation J X : Type (max (max (max u' u_1) u_2) v')

A structure expressing that X : C is the colimit of a functor diag : J ⥤ C such that P (diag.obj j) holds for all j.

• diag : Functor J C
• ι : self.diag ⟶ (Functor.const J).obj X
• isColimit : IsColimit { pt := X, ι := self.ι }
• prop_diag_obj (j : J) : P (self.diag.obj j)

noncomputable def CategoryTheory.ObjectProperty.ColimitOfShape.colimit {C : Type u_1} [Category.{u_2, u_1} C] {P : ObjectProperty C} {J : Type u'} [Category.{v', u'} J] (F : Functor J C) [Limits.HasColimit F] (hF : ∀ (j : J), P (F.obj j)) : P.ColimitOfShape J (Limits.colimit F)

If F : J ⥤ C is a functor that has a colimit and is such that for all j, F.obj j satisfies a property P, then this structure expresses that colimit F is indeed a colimit of objects satisfying P.

Equations

• CategoryTheory.ObjectProperty.ColimitOfShape.colimit F hF = { toColimitPresentation := CategoryTheory.Limits.ColimitPresentation.colimit F, prop_diag_obj := hF }

@[simp]

theorem CategoryTheory.ObjectProperty.ColimitOfShape.colimit_toColimitPresentation {C : Type u_1} [Category.{u_2, u_1} C] {P : ObjectProperty C} {J : Type u'} [Category.{v', u'} J] (F : Functor J C) [Limits.HasColimit F] (hF : ∀ (j : J), P (F.obj j)) : (colimit F hF).toColimitPresentation = Limits.ColimitPresentation.colimit F

def CategoryTheory.ObjectProperty.ColimitOfShape.ofIso {C : Type u_1} [Category.{u_2, u_1} C] {P : ObjectProperty C} {J : Type u'} [Category.{v', u'} J] {X : C} (h : P.ColimitOfShape J X) {Y : C} (e : X ≅ Y) : P.ColimitOfShape J Y

If X is a colimit indexed by J of objects satisfying a property P, then any object that is isomorphic to X also is.

Equations

• h.ofIso e = { toColimitPresentation := h.ofIso e, prop_diag_obj := ⋯ }

@[simp]

theorem CategoryTheory.ObjectProperty.ColimitOfShape.ofIso_toColimitPresentation {C : Type u_1} [Category.{u_2, u_1} C] {P : ObjectProperty C} {J : Type u'} [Category.{v', u'} J] {X : C} (h : P.ColimitOfShape J X) {Y : C} (e : X ≅ Y) : (h.ofIso e).toColimitPresentation = h.ofIso e

def CategoryTheory.ObjectProperty.ColimitOfShape.ofLE {C : Type u_1} [Category.{u_2, u_1} C] {P : ObjectProperty C} {J : Type u'} [Category.{v', u'} J] {X : C} (h : P.ColimitOfShape J X) {Q : ObjectProperty C} (hPQ : P ≤ Q) : Q.ColimitOfShape J X

If X is a colimit indexed by J of objects satisfying a property P, it is also a colimit indexed by J of objects satisfying Q if P ≤ Q.

Equations

• h.ofLE hPQ = { toColimitPresentation := h.toColimitPresentation, prop_diag_obj := ⋯ }

@[simp]

theorem CategoryTheory.ObjectProperty.ColimitOfShape.ofLE_toColimitPresentation {C : Type u_1} [Category.{u_2, u_1} C] {P : ObjectProperty C} {J : Type u'} [Category.{v', u'} J] {X : C} (h : P.ColimitOfShape J X) {Q : ObjectProperty C} (hPQ : P ≤ Q) : (h.ofLE hPQ).toColimitPresentation = h.toColimitPresentation

def CategoryTheory.ObjectProperty.colimitsOfShape {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] : ObjectProperty C

The property of objects that are the point of a colimit cocone for a functor F : J ⥤ C where all objects F.obj j satisfy P.

Equations

• P.colimitsOfShape J X = Nonempty (P.ColimitOfShape J X)

theorem CategoryTheory.ObjectProperty.ColimitOfShape.colimitsOfShape {C : Type u_1} [Category.{u_2, u_1} C] {P : ObjectProperty C} {J : Type u'} [Category.{v', u'} J] {X : C} (h : P.ColimitOfShape J X) : P.colimitsOfShape J X

theorem CategoryTheory.ObjectProperty.strictColimitsOfShape_le_colimitsOfShape {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] : P.strictColimitsOfShape J ≤ P.colimitsOfShape J

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsColimitsOfShape {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] : (P.colimitsOfShape J).IsClosedUnderIsomorphisms

@[simp]

theorem CategoryTheory.ObjectProperty.isoClosure_strictColimitsOfShape {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] : (P.strictColimitsOfShape J).isoClosure = P.colimitsOfShape J

theorem CategoryTheory.ObjectProperty.colimitsOfShape_monotone {C : Type u_1} [Category.{u_2, u_1} C] {P : ObjectProperty C} (J : Type u') [Category.{v', u'} J] {Q : ObjectProperty C} (hPQ : P ≤ Q) : P.colimitsOfShape J ≤ Q.colimitsOfShape J

@[simp]

theorem CategoryTheory.ObjectProperty.colimitsOfShape_isoClosure {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] : P.isoClosure.colimitsOfShape J = P.colimitsOfShape J

instance CategoryTheory.ObjectProperty.instSmallStrictColimitsOfShapeOfSmallOfLocallySmall {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] [ObjectProperty.Small.{w, u_2, u_1} P] [LocallySmall.{w, u_2, u_1} C] [Small.{w, u'} J] [LocallySmall.{w, v', u'} J] : ObjectProperty.Small.{w, u_2, u_1} (P.strictColimitsOfShape J)