Preservation of filtered colimits and cofiltered limits. #
Typically forgetful functors from algebraic categories preserve filtered colimits
(although not general colimits). See e.g. Algebra/Category/MonCat/FilteredColimits
.
PreservesFilteredColimitsOfSize.{w', w} F
means that F
sends all colimit cocones over any
filtered diagram J ⥤ C
to colimit cocones, where J : Type w
with [Category.{w'} J]
.
- preserves_filtered_colimits (J : Type w) [Category.{w', w} J] [IsFiltered J] : PreservesColimitsOfShape J F
Instances
A functor is said to preserve filtered colimits, if it preserves all colimits of shape J
, where
J
is a filtered category which is small relative to the universe in which morphisms of the source
live.
Equations
Instances For
A functor preserving larger filtered colimits also preserves smaller filtered colimits.
PreservesFilteredColimitsOfSize_shrink.{w, w'} F
tries to obtain
PreservesFilteredColimitsOfSize.{w, w'} F
from some other PreservesFilteredColimitsOfSize F
.
Preserving filtered colimits at any universe implies preserving filtered colimits at universe 0
.
ReflectsFilteredColimitsOfSize.{w', w} F
means that whenever the image of a filtered cocone
under F
is a colimit cocone, the original cocone was already a colimit.
- reflects_filtered_colimits (J : Type w) [Category.{w', w} J] [IsFiltered J] : ReflectsColimitsOfShape J F
Instances
A functor is said to reflect filtered colimits, if it reflects all colimits of shape J
, where
J
is a filtered category which is small relative to the universe in which morphisms of the source
live.
Equations
Instances For
A functor reflecting larger filtered colimits also reflects smaller filtered colimits.
ReflectsFilteredColimitsOfSize_shrink.{w, w'} F
tries to obtain
ReflectsFilteredColimitsOfSize.{w, w'} F
from some other ReflectsFilteredColimitsOfSize F
.
Reflecting filtered colimits at any universe implies reflecting filtered colimits at universe 0
.
PreservesCofilteredLimitsOfSize.{w', w} F
means that F
sends all limit cones over any
cofiltered diagram J ⥤ C
to limit cones, where J : Type w
with [Category.{w'} J]
.
- preserves_cofiltered_limits (J : Type w) [Category.{w', w} J] [IsCofiltered J] : PreservesLimitsOfShape J F
Instances
A functor is said to preserve cofiltered limits, if it preserves all limits of shape J
, where
J
is a cofiltered category which is small relative to the universe in which morphisms of the
source live.
Equations
Instances For
A functor preserving larger cofiltered limits also preserves smaller cofiltered limits.
PreservesCofilteredLimitsOfSizeShrink.{w, w'} F
tries to obtain
PreservesCofilteredLimitsOfSize.{w, w'} F
from some other PreservesCofilteredLimitsOfSize F
.
Preserving cofiltered limits at any universe implies preserving cofiltered limits at universe 0
.
ReflectsCofilteredLimitsOfSize.{w', w} F
means that whenever the image of a cofiltered cone
under F
is a limit cone, the original cone was already a limit.
- reflects_cofiltered_limits (J : Type w) [Category.{w', w} J] [IsCofiltered J] : ReflectsLimitsOfShape J F
Instances
A functor is said to reflect cofiltered limits, if it reflects all limits of shape J
, where
J
is a cofiltered category which is small relative to the universe in which morphisms of the
source live.
Equations
Instances For
A functor reflecting larger cofiltered limits also reflects smaller cofiltered limits.
ReflectsCofilteredLimitsOfSize_shrink.{w, w'} F
tries to obtain
ReflectsCofilteredLimitsOfSize.{w, w'} F
from some other ReflectsCofilteredLimitsOfSize F
.
Reflecting cofiltered limits at any universe implies reflecting cofiltered limits at universe 0
.