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.

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

TODO #

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

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

              Instances
                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
                @[deprecated CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape (since := "2025-09-22")]

                Alias of CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.


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

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

                  Alias of CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.mk'.

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

                  Alias of CategoryTheory.ObjectProperty.prop_limit.