Objects that are limits 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.strictLimitsOfShape J and P.limitsOfShape J. The former contains exactly the objects of the form limit F for any functor F : J ⥤ C that has a limit 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 limit F.

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

By requiring P.limitsOfShape J ≤ P, we introduce a typeclass P.IsClosedUnderLimitsOfShape J.

TODO

• formalize the closure of P under finite limits (which require iterating over ℕ), and more generally the closure under limits indexed by a category whose type of arrows has a cardinality that is bounded by a certain regular cardinal (@joelriou)

inductive CategoryTheory.ObjectProperty.strictLimitsOfShape {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 limit F for some functor F : J ⥤ C where all F.obj j satisfy P.

• limit {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.HasLimit F] (hF : ∀ (j : J), P (F.obj j)) : P.strictLimitsOfShape J (Limits.limit F)

theorem CategoryTheory.ObjectProperty.strictLimitsOfShape_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.strictLimitsOfShape J ≤ Q.strictLimitsOfShape J

structure CategoryTheory.ObjectProperty.LimitOfShape {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.LimitPresentation J X : Type (max (max (max u' u_1) u_2) v')

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

• diag : Functor J C
• π : (Functor.const J).obj X ⟶ self.diag
• isLimit : IsLimit { pt := X, π := self.π }
• prop_diag_obj (j : J) : P (self.diag.obj j)

noncomputable def CategoryTheory.ObjectProperty.LimitOfShape.limit {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.HasLimit F] (hF : ∀ (j : J), P (F.obj j)) : P.LimitOfShape J (Limits.limit F)

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

Equations

• CategoryTheory.ObjectProperty.LimitOfShape.limit F hF = { toLimitPresentation := CategoryTheory.Limits.LimitPresentation.limit F, prop_diag_obj := hF }

def CategoryTheory.ObjectProperty.LimitOfShape.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.LimitOfShape J X) {Y : C} (e : X ≅ Y) : P.LimitOfShape J Y

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

Equations

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

@[simp]

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

def CategoryTheory.ObjectProperty.LimitOfShape.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.LimitOfShape J X) {Q : ObjectProperty C} (hPQ : P ≤ Q) : Q.LimitOfShape J X

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

Equations

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

@[simp]

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

noncomputable def CategoryTheory.ObjectProperty.LimitOfShape.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.LimitOfShape J X) (G : Functor J' J) [G.Initial] : P.LimitOfShape J' X

Change the index category for ObjectProperty.LimitOfShape.

Equations

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

@[simp]

theorem CategoryTheory.ObjectProperty.LimitOfShape.reindex_toLimitPresentation {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.LimitOfShape J X) (G : Functor J' J) [G.Initial] : (h.reindex G).toLimitPresentation = h.reindex G

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

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

Equations

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

@[simp]

theorem CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrow_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.LimitOfShape J X) (j : J) : p.toStructuredArrow.obj j = StructuredArrow.mk (p.π.app j)

@[simp]

theorem CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrow_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.LimitOfShape J X) {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) : p.toStructuredArrow.map f = StructuredArrow.homMk (p.diag.map f) ⋯

def CategoryTheory.ObjectProperty.limitsOfShape {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 limit cone for a functor F : J ⥤ C where all objects F.obj j satisfy P.

Equations

• P.limitsOfShape J X = Nonempty (P.LimitOfShape J X)

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

theorem CategoryTheory.ObjectProperty.strictLimitsOfShape_le_limitsOfShape {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] : P.strictLimitsOfShape J ≤ P.limitsOfShape J

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

@[simp]

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

theorem CategoryTheory.ObjectProperty.limitsOfShape_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.limitsOfShape J ≤ Q.limitsOfShape J

@[simp]

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

instance CategoryTheory.ObjectProperty.instSmallStrictLimitsOfShapeOfSmallOfLocallySmall {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.strictLimitsOfShape J)

instance CategoryTheory.ObjectProperty.instEssentiallySmallLimitsOfShapeOfSmallOfSmallOfLocallySmall {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.EssentiallySmall.{w, u_2, u_1} (P.limitsOfShape J)

class CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape {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.IsClosedUnderLimitsOfShape J if it is stable by limits of shape J.

• limitsOfShape_le : P.limitsOfShape J ≤ P

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

theorem CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.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.strictLimitsOfShape J ≤ P) : P.IsClosedUnderLimitsOfShape J

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

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

theorem CategoryTheory.ObjectProperty.prop_limit {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) {J : Type u'} [Category.{v', u'} J] [P.IsClosedUnderLimitsOfShape J] (F : Functor J C) [Limits.HasLimit F] (hF : ∀ (j : J), P (F.obj j)) : P (Limits.limit F)

theorem CategoryTheory.ObjectProperty.limitsOfShape_le_of_initial {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.Initial] : P.limitsOfShape J' ≤ P.limitsOfShape J

theorem CategoryTheory.ObjectProperty.limitsOfShape_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.limitsOfShape J = P.limitsOfShape J'

theorem CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_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.IsClosedUnderLimitsOfShape J ↔ P.IsClosedUnderLimitsOfShape J'

theorem CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.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.IsClosedUnderLimitsOfShape J] : P.IsClosedUnderLimitsOfShape J'

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

def CategoryTheory.Limits.ClosedUnderLimitsOfShape {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.IsClosedUnderLimitsOfShape.

---

A property of objects satisfies P.IsClosedUnderLimitsOfShape J if it is stable by limits of shape J.

Equations

• @CategoryTheory.Limits.ClosedUnderLimitsOfShape = @CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape

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

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

Alias of CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.mk'.

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

theorem CategoryTheory.Limits.ClosedUnderLimitsOfShape.limit {C : Type u_1} [Category.{u_2, u_1} C] (P : ObjectProperty C) {J : Type u'} [Category.{v', u'} J] [P.IsClosedUnderLimitsOfShape J] (F : Functor J C) [HasLimit F] (hF : ∀ (j : J), P (F.obj j)) : P (Limits.limit F)

Alias of CategoryTheory.ObjectProperty.prop_limit.