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.instNonemptyColimitsClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] [P.Nonempty] : (P.colimitsClosure J).Nonempty

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_eq_self {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] [P.IsClosedUnderIsomorphisms] [∀ (a : α), P.IsClosedUnderColimitsOfShape (J a)] : P.colimitsClosure J = P

@[simp]

theorem CategoryTheory.ObjectProperty.colimitsClosure_bot {C : Type u} [Category.{v, u} C] {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] [∀ (a : α), Nonempty (J a)] : ⊥.colimitsClosure J = ⊥

@[simp]

theorem CategoryTheory.ObjectProperty.colimitsClosure_top {C : Type u} [Category.{v, u} C] {α : Type t} (J : α → Type u') [(a : α) → Category.{v', u'} (J a)] : ⊤.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

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.colimitClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (J : Type u_1) [Category.{v_1, u_1} J] : ObjectProperty C

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

Equations

• P.colimitClosure J = P.colimitsClosure fun (x : Unit) => J

instance CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeColimitClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (J : Type u_1) [Category.{v_1, u_1} J] : (P.colimitClosure J).IsClosedUnderColimitsOfShape 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)