Documentation

Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

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.

The property of objects that are equal to limit F for some functor F : J ⥤ C where all F.obj j satisfy P.

Instances For
    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.

    Instances For
      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)) :

      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
      Instances For
        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) :

        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 := }
        Instances For

          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
          Instances For

            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
            Instances For