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.{v_1, 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.{v_1, 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.{v_1, 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

@[simp]

theorem CategoryTheory.ObjectProperty.strictLimitsOfShape_bot {C : Type u_1} [Category.{v_1, u_1} C] (J : Type u') [Category.{v', u'} J] [Nonempty J] : ⊥.strictLimitsOfShape J = ⊥

structure CategoryTheory.ObjectProperty.LimitOfShape {C : Type u_1} [Category.{v_1, 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) v') v_1)

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.{v_1, 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.

def CategoryTheory.ObjectProperty.LimitOfShape.ofIso {C : Type u_1} [Category.{v_1, 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.

@[simp]

theorem CategoryTheory.ObjectProperty.LimitOfShape.ofIso_toLimitPresentation {C : Type u_1} [Category.{v_1, 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.{v_1, 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.

@[simp]

theorem CategoryTheory.ObjectProperty.LimitOfShape.ofLE_toLimitPresentation {C : Type u_1} [Category.{v_1, 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.{v_1, 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.

@[simp]

theorem CategoryTheory.ObjectProperty.LimitOfShape.reindex_toLimitPresentation {C : Type u_1} [Category.{v_1, 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.{v_1, 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.

@[simp]

theorem CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrow_map {C : Type u_1} [Category.{v_1, 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 (homMk (p.diag.map f)) ⋯

@[simp]

theorem CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrow_obj {C : Type u_1} [Category.{v_1, 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)

def CategoryTheory.ObjectProperty.limitsOfShape {C : Type u_1} [Category.{v_1, 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.

theorem CategoryTheory.ObjectProperty.LimitOfShape.limitsOfShape {C : Type u_1} [Category.{v_1, 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.{v_1, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] : P.strictLimitsOfShape J ≤ P.limitsOfShape J

@[simp]

theorem CategoryTheory.ObjectProperty.limitsOfShape_bot {C : Type u_1} [Category.{v_1, u_1} C] (J : Type u') [Category.{v', u'} J] [Nonempty J] : ⊥.limitsOfShape J = ⊥

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsLimitsOfShape {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] [ObjectProperty.Small.{w, v_1, u_1} P] [LocallySmall.{w, v_1, u_1} C] [Small.{w, u'} J] [LocallySmall.{w, v', u'} J] : ObjectProperty.Small.{w, v_1, u_1} (P.strictLimitsOfShape J)

instance CategoryTheory.ObjectProperty.instEssentiallySmallLimitsOfShapeOfSmallOfSmallOfLocallySmall {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] [ObjectProperty.Small.{w, v_1, u_1} P] [LocallySmall.{w, v_1, u_1} C] [Small.{w, u'} J] [LocallySmall.{w, v', u'} J] : ObjectProperty.EssentiallySmall.{w, v_1, u_1} (P.limitsOfShape J)

class CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, u_1} C] {P : ObjectProperty C} {J : Type u'} [Category.{v', u'} J] [P.IsClosedUnderIsomorphisms] (h : P.strictLimitsOfShape J ≤ P) : P.IsClosedUnderLimitsOfShape J

instance CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeBotOfNonempty {C : Type u_1} [Category.{v_1, u_1} C] (J : Type u') [Category.{v', u'} J] [Nonempty J] : ⊥.IsClosedUnderLimitsOfShape J

instance CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeTop {C : Type u_1} [Category.{v_1, u_1} C] (J : Type u') [Category.{v', u'} J] : ⊤.IsClosedUnderLimitsOfShape J

theorem CategoryTheory.ObjectProperty.LimitOfShape.prop {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.prop_pi {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {J : Type u_3} [P.IsClosedUnderLimitsOfShape (Discrete J)] (X : J → C) [Limits.HasProduct X] (hF : ∀ (j : J), P (X j)) : P (∏ᶜ X)

theorem CategoryTheory.ObjectProperty.limitsOfShape_le_of_initial {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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'

instance CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.inverseImage {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (J : Type u') [Category.{v', u'} J] (P : ObjectProperty D) (F : Functor C D) [P.IsClosedUnderLimitsOfShape J] [Limits.PreservesLimitsOfShape J F] : (P.inverseImage F).IsClosedUnderLimitsOfShape J

theorem CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_inverseImage_iff {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (J : Type u') [Category.{v', u'} J] (P : ObjectProperty D) [P.IsClosedUnderIsomorphisms] (e : C ≌ D) : (P.inverseImage e.functor).IsClosedUnderLimitsOfShape J ↔ P.IsClosedUnderLimitsOfShape J