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 Punder 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)
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)
Instances For
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
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 }
Instances For
If X is a limit indexed by J of objects satisfying a property P, then
any object that is isomorphic to X also is.
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
- h.ofLE hPQ = { toLimitPresentation := h.toLimitPresentation, prop_diag_obj := ⋯ }
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
- P.limitsOfShape J X = Nonempty (P.LimitOfShape J X)
Instances For
A property of objects satisfies P.IsClosedUnderLimitsOfShape J if it
is stable by limits of shape J.
Instances
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
Alias of CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.mk'.
Alias of CategoryTheory.ObjectProperty.prop_limit.