Closure of a property of objects under colimits of certain shapes

In this file, given a property P of objects in a category C and family of categories J : α → Type _, we introduce the closure P.colimitsClosure J of P under colimits of shapes J a for all a : α, and under certain smallness assumptions, we show that it is essentially small.

(We deduce these results about the closure under colimits by dualising the results in the file Mathlib/CategoryTheory/ObjectProperty/LimitsClosure.lean.)

inductive CategoryTheory.ObjectProperty.colimitsClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] : ObjectProperty C

The closure of a property of objects of a category under colimits of shape J a for a family of categories J.

• of_mem {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {α : Type t} {J : α → Type u'} [(a : α) → Category.{v', u'} (J a)] (X : C) (hX : P X) : P.colimitsClosure J X
• of_isoClosure {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {α : Type t} {J : α → Type u'} [(a : α) → Category.{v', u'} (J a)] {X Y : C} (e : X ≅ Y) (hX : P.colimitsClosure J X) : P.colimitsClosure J Y
• of_colimitPresentation {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {α : Type t} {J : α → Type u'} [(a : α) → Category.{v', u'} (J a)] {X : C} {a : α} (pres : Limits.ColimitPresentation (J a) X) (h : ∀ (j : J a), P.colimitsClosure J (pres.diag.obj j)) : P.colimitsClosure J X

@[simp]

theorem CategoryTheory.ObjectProperty.le_colimitsClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] : P ≤ P.colimitsClosure J

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsColimitsClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] : (P.colimitsClosure J).IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeColimitsClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] (a : α) : (P.colimitsClosure J).IsClosedUnderColimitsOfShape (J a)

theorem CategoryTheory.ObjectProperty.colimitsClosure_le {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {α : Type t} {J : α → Type u'} [(a : α) → Category.{v', u'} (J a)] {Q : ObjectProperty C} [Q.IsClosedUnderIsomorphisms] [∀ (a : α), Q.IsClosedUnderColimitsOfShape (J a)] (h : P ≤ Q) : P.colimitsClosure J ≤ Q

theorem CategoryTheory.ObjectProperty.colimitsClosure_monotone {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] {Q : ObjectProperty C} (h : P ≤ Q) : P.colimitsClosure J ≤ Q.colimitsClosure J

theorem CategoryTheory.ObjectProperty.colimitsClosure_isoClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] : P.isoClosure.colimitsClosure J = P.colimitsClosure J

theorem CategoryTheory.ObjectProperty.colimitsClosure_eq_unop_limitsClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] : P.colimitsClosure J = (P.op.limitsClosure fun (a : α) => (J a)ᵒᵖ).unop

instance CategoryTheory.ObjectProperty.instEssentiallySmallColimitsClosureOfSmallOfLocallySmall {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] [ObjectProperty.EssentiallySmall.{w, v, u} P] [LocallySmall.{w, v, u} C] [Small.{w, t} α] [∀ (a : α), Small.{w, u'} (J a)] [∀ (a : α), LocallySmall.{w, v', u'} (J a)] : ObjectProperty.EssentiallySmall.{w, v, u} (P.colimitsClosure J)