Objects that are colimits 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.strictColimitsOfShape J
and P.colimitsOfShape J. The former contains exactly the objects
of the form colimit F for any functor F : J ⥤ C that has
a colimit 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 colimit F.
Under certain circumstances, the type of objects satisfying
P.strictColimitsOfShape J is small: the main reason this variant is
introduced is to deduce that the full subcategory of P.colimitsOfShape J
is essentially small.
By requiring P.colimitsOfShape J ≤ P, we introduce a typeclass
P.IsClosedUnderColimitsOfShape J.
TODO #
- refactor ObjectProperty.indby saying that it is the supremum ofP.colimitsOfShape Jfor a filtered categoryJ(generalize also toκ-filtered categories?)
- formalize the closure of Punder finite colimits (which require iterating overℕ), and more generally the closure under colimits 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 colimit F for some
functor F : J ⥤ C where all F.obj j satisfy P.
- colimit {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.HasColimit F] (hF : ∀ (j : J), P (F.obj j)) : P.strictColimitsOfShape J (Limits.colimit F)
Instances For
A structure expressing that X : C is the colimit 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 colimit and is such that for all j,
F.obj j satisfies a property P, then this structure expresses that colimit F
is indeed a colimit of objects satisfying P.
Equations
- CategoryTheory.ObjectProperty.ColimitOfShape.colimit F hF = { toColimitPresentation := CategoryTheory.Limits.ColimitPresentation.colimit F, prop_diag_obj := hF }
Instances For
If X is a colimit 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 colimit indexed by J of objects satisfying a property P,
it is also a colimit indexed by J of objects satisfying Q if P ≤ Q.
Equations
- h.ofLE hPQ = { toColimitPresentation := h.toColimitPresentation, prop_diag_obj := ⋯ }
Instances For
The property of objects that are the point of a colimit cocone for a
functor F : J ⥤ C where all objects F.obj j satisfy P.
Equations
- P.colimitsOfShape J X = Nonempty (P.ColimitOfShape J X)
Instances For
A property of objects satisfies P.IsClosedUnderColimitsOfShape J if it
is stable by colimits of shape J.
Instances
Alias of CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.
A property of objects satisfies P.IsClosedUnderColimitsOfShape J if it
is stable by colimits of shape J.
Equations
Instances For
Alias of CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.mk'.