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.

By requiring P.colimitsOfShape J ≤ P, we introduce a typeclass P.IsClosedUnderColimitsOfShape J.

We also show that colimitsOfShape in a category C is related to limitsOfShape in the opposite category Cᵒᵖ and vice versa.

TODO

• 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

noncomputable def CategoryTheory.ObjectProperty.ColimitOfShape.reindex {C : Type u_1} [Category.{u_2, u_1} C] {P : ObjectProperty C} {J : Type u'} [Category.{v', u'} J] {J' : Type u''} [Category.{v'', u''} J'] {X : C} (h : P.ColimitOfShape J X) (G : Functor J' J) [G.Final] : P.ColimitOfShape J' X

Change the index category for ObjectProperty.ColimitOfShape.

Equations

• h.reindex G = { toColimitPresentation := h.reindex G, prop_diag_obj := ⋯ }

@[simp]

theorem CategoryTheory.ObjectProperty.ColimitOfShape.reindex_toColimitPresentation {C : Type u_1} [Category.{u_2, u_1} C] {P : ObjectProperty C} {J : Type u'} [Category.{v', u'} J] {J' : Type u''} [Category.{v'', u''} J'] {X : C} (h : P.ColimitOfShape J X) (G : Functor J' J) [G.Final] : (h.reindex G).toColimitPresentation = h.reindex G

def CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow {C : Type u_1} [Category.{u_2, u_1} C] {P : ObjectProperty C} {J : Type u'} [Category.{v', u'} J] {X : C} (p : P.ColimitOfShape J X) : Functor J (CostructuredArrow P.ι X)

Given P : ObjectProperty C, and a presentation P.ColimitOfShape J X of an object X : C, this is the induced functor J ⥤ CostructuredArrow P.ι X.

Equations

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

@[simp]

theorem CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow_map {C : Type u_1} [Category.{u_2, u_1} C] {P : ObjectProperty C} {J : Type u'} [Category.{v', u'} J] {X : C} (p : P.ColimitOfShape J X) {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) : p.toCostructuredArrow.map f = CostructuredArrow.homMk (p.diag.map f) ⋯

@[simp]

theorem CategoryTheory.ObjectProperty.ColimitOfShape.toCostructuredArrow_obj {C : Type u_1} [Category.{u_2, u_1} C] {P : ObjectProperty C} {J : Type u'} [Category.{v', u'} J] {X : C} (p : P.ColimitOfShape J X) (j : J) : p.toCostructuredArrow.obj j = CostructuredArrow.mk (p.ι.app j)

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)

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

A property of objects satisfies P.IsClosedUnderColimitsOfShape J if it is stable by colimits of shape J.

• colimitsOfShape_le : P.colimitsOfShape J ≤ P

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

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

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

theorem CategoryTheory.ObjectProperty.prop_of_isColimit {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) {J : Type u'} [Category.{v', u'} J] [P.IsClosedUnderColimitsOfShape J] {F : Functor J C} {c : Limits.Cocone F} (hc : Limits.IsColimit c) (hF : ∀ (j : J), P (F.obj j)) : P c.pt

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

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

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

theorem CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff_of_equivalence {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) {J : Type u'} [Category.{v', u'} J] {J' : Type u''} [Category.{v'', u''} J'] (e : J ≌ J') : P.IsClosedUnderColimitsOfShape J ↔ P.IsClosedUnderColimitsOfShape J'

theorem CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.of_equivalence {C : Type u_1} [Category.{u_2, u_1} C] {P : ObjectProperty C} {J : Type u'} [Category.{v', u'} J] {J' : Type u''} [Category.{v'', u''} J'] (e : J ≌ J') [P.IsClosedUnderColimitsOfShape J] : P.IsClosedUnderColimitsOfShape J'

theorem CategoryTheory.ObjectProperty.colimitsOfShape_eq_unop_limitsOfShape {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] : P.colimitsOfShape J = (P.op.limitsOfShape Jᵒᵖ).unop

theorem CategoryTheory.ObjectProperty.limitsOfShape_eq_unop_colimitsOfShape {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] : P.limitsOfShape J = (P.op.colimitsOfShape Jᵒᵖ).unop

theorem CategoryTheory.ObjectProperty.limitsOfShape_op {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] : P.op.limitsOfShape J = (P.colimitsOfShape Jᵒᵖ).op

theorem CategoryTheory.ObjectProperty.colimitsOfShape_op {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] : P.op.colimitsOfShape J = (P.limitsOfShape Jᵒᵖ).op

theorem CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff_op {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] : P.IsClosedUnderColimitsOfShape J ↔ P.op.IsClosedUnderLimitsOfShape Jᵒᵖ

theorem CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff_op {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] : P.IsClosedUnderLimitsOfShape J ↔ P.op.IsClosedUnderColimitsOfShape Jᵒᵖ

theorem CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_op_iff_op {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] : P.IsClosedUnderColimitsOfShape Jᵒᵖ ↔ P.op.IsClosedUnderLimitsOfShape J

theorem CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_op_iff_op {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] : P.IsClosedUnderLimitsOfShape Jᵒᵖ ↔ P.op.IsClosedUnderColimitsOfShape J

instance CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeOppositeOpOfIsClosedUnderColimitsOfShape {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] [P.IsClosedUnderColimitsOfShape J] : P.op.IsClosedUnderLimitsOfShape Jᵒᵖ

instance CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeOppositeOpOfIsClosedUnderLimitsOfShape {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] [P.IsClosedUnderLimitsOfShape J] : P.op.IsClosedUnderColimitsOfShape Jᵒᵖ

instance CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeOppositeOpOfIsClosedUnderColimitsOfShape_1 {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] [P.IsClosedUnderColimitsOfShape Jᵒᵖ] : P.op.IsClosedUnderLimitsOfShape J

instance CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeOppositeOpOfIsClosedUnderLimitsOfShape_1 {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] [P.IsClosedUnderLimitsOfShape Jᵒᵖ] : P.op.IsClosedUnderColimitsOfShape J

theorem CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff_unop {C : Type u_1} [Category.{u_2, u_1} C] (J : Type u') [Category.{v', u'} J] (Q : ObjectProperty Cᵒᵖ) : Q.IsClosedUnderColimitsOfShape J ↔ Q.unop.IsClosedUnderLimitsOfShape Jᵒᵖ

theorem CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff_unop {C : Type u_1} [Category.{u_2, u_1} C] (J : Type u') [Category.{v', u'} J] (Q : ObjectProperty Cᵒᵖ) : Q.IsClosedUnderLimitsOfShape J ↔ Q.unop.IsClosedUnderColimitsOfShape Jᵒᵖ

theorem CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_op_iff_unop {C : Type u_1} [Category.{u_2, u_1} C] (J : Type u') [Category.{v', u'} J] (Q : ObjectProperty Cᵒᵖ) : Q.IsClosedUnderColimitsOfShape Jᵒᵖ ↔ Q.unop.IsClosedUnderLimitsOfShape J

theorem CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_op_iff_unop {C : Type u_1} [Category.{u_2, u_1} C] (J : Type u') [Category.{v', u'} J] (Q : ObjectProperty Cᵒᵖ) : Q.IsClosedUnderLimitsOfShape Jᵒᵖ ↔ Q.unop.IsClosedUnderColimitsOfShape J

instance CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeUnopOppositeOfIsClosedUnderColimitsOfShape {C : Type u_1} [Category.{u_2, u_1} C] (J : Type u') [Category.{v', u'} J] (Q : ObjectProperty Cᵒᵖ) [Q.IsClosedUnderColimitsOfShape J] : Q.unop.IsClosedUnderLimitsOfShape Jᵒᵖ

instance CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeUnopOppositeOfIsClosedUnderLimitsOfShape {C : Type u_1} [Category.{u_2, u_1} C] (J : Type u') [Category.{v', u'} J] (Q : ObjectProperty Cᵒᵖ) [Q.IsClosedUnderLimitsOfShape J] : Q.unop.IsClosedUnderColimitsOfShape Jᵒᵖ

instance CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeUnopOfIsClosedUnderColimitsOfShapeOpposite {C : Type u_1} [Category.{u_2, u_1} C] (J : Type u') [Category.{v', u'} J] (Q : ObjectProperty Cᵒᵖ) [Q.IsClosedUnderColimitsOfShape Jᵒᵖ] : Q.unop.IsClosedUnderLimitsOfShape J

instance CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeUnopOfIsClosedUnderLimitsOfShapeOpposite {C : Type u_1} [Category.{u_2, u_1} C] (J : Type u') [Category.{v', u'} J] (Q : ObjectProperty Cᵒᵖ) [Q.IsClosedUnderLimitsOfShape Jᵒᵖ] : Q.unop.IsClosedUnderColimitsOfShape J

@[deprecated CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape (since := "2025-09-22")]

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

Alias of CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.

---

A property of objects satisfies P.IsClosedUnderColimitsOfShape J if it is stable by colimits of shape J.

Equations

• @CategoryTheory.Limits.ClosedUnderColimitsOfShape = @CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape

@[deprecated CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.mk' (since := "2025-09-22")]

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

Alias of CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.mk'.

@[deprecated CategoryTheory.ObjectProperty.prop_colimit (since := "2025-09-22")]

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

Alias of CategoryTheory.ObjectProperty.prop_colimit.