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
.
- 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)