Preservation and reflection of (co)limits. #
There are various distinct notions of "preserving limits". The one we aim to capture here is: A functor F : C → D "preserves limits" if it sends every limit cone in C to a limit cone in D. Informally, F preserves all the limits which exist in C.
Note that:
-
Of course, we do not want to require F to strictly take chosen limit cones of C to chosen limit cones of D. Indeed, the above definition makes no reference to a choice of limit cones so it makes sense without any conditions on C or D.
-
Some diagrams in C may have no limit. In this case, there is no condition on the behavior of F on such diagrams. There are other notions (such as "flat functor") which impose conditions also on diagrams in C with no limits, but these are not considered here.
In order to be able to express the property of preserving limits of a certain form, we say that a functor F preserves the limit of a diagram K if F sends every limit cone on K to a limit cone. This is vacuously satisfied when K does not admit a limit, which is consistent with the above definition of "preserves limits".
- preserves : Π {c : category_theory.limits.cone K}, category_theory.limits.is_limit c → category_theory.limits.is_limit (F.map_cone c)
A functor F
preserves limits of K
(written as preserves_limit K F
)
if F
maps any limit cone over K
to a limit cone.
- preserves : Π {c : category_theory.limits.cocone K}, category_theory.limits.is_colimit c → category_theory.limits.is_colimit (F.map_cocone c)
A functor F
preserves colimits of K
(written as preserves_colimit K F
)
if F
maps any colimit cocone over K
to a colimit cocone.
- preserves_limit : Π {K : J ⥤ C}, category_theory.limits.preserves_limit K F
We say that F
preserves limits of shape J
if F
preserves limits for every diagram
K : J ⥤ C
, i.e., F
maps limit cones over K
to limit cones.
- preserves_colimit : Π {K : J ⥤ C}, category_theory.limits.preserves_colimit K F
We say that F
preserves colimits of shape J
if F
preserves colimits for every diagram
K : J ⥤ C
, i.e., F
maps colimit cocones over K
to colimit cocones.
- preserves_limits_of_shape : Π {J : Type ?} [𝒥 : category_theory.small_category J], category_theory.limits.preserves_limits_of_shape J F
We say that F
preserves limits if it sends limit cones over any diagram to limit cones.
Instances
- category_theory.preserves_limits_of_creates_limits_and_has_limits
- category_theory.adjunction.is_equivalence_preserves_limits
- category_theory.limits.id_preserves_limits
- category_theory.limits.comp_preserves_limits
- Mon.forget_preserves_limits
- AddMon.forget_preserves_limits
- CommMon.forget₂_Mon_preserves_limits
- AddCommMon.forget₂_AddMon_preserves_limits
- CommMon.forget_preserves_limits
- AddCommMon.forget_preserves_limits
- Group.forget₂_Mon_preserves_limits
- AddGroup.forget₂_AddMon_preserves_limits
- Group.forget_preserves_limits
- AddGroup.forget_preserves_limits
- CommGroup.forget₂_Group_preserves_limits
- AddCommGroup.forget₂_AddGroup_preserves_limits
- CommGroup.forget₂_CommMon_preserves_limits
- AddCommGroup.forget₂_AddCommMon_preserves_limits
- CommGroup.forget_preserves_limits
- AddCommGroup.forget_preserves_limits
- Module.forget₂_AddCommGroup_preserves_limits
- Module.forget_preserves_limits
- SemiRing.forget₂_AddCommMon_preserves_limits
- SemiRing.forget₂_Mon_preserves_limits
- SemiRing.forget_preserves_limits
- CommSemiRing.forget₂_SemiRing_preserves_limits
- CommSemiRing.forget_preserves_limits
- Ring.forget₂_SemiRing_preserves_limits
- Ring.forget₂_AddCommGroup_preserves_limits
- Ring.forget_preserves_limits
- CommRing.forget₂_Ring_preserves_limits
- CommRing.forget₂_CommSemiRing_preserves_limits
- CommRing.forget_preserves_limits
- Algebra.forget₂_Ring_preserves_limits
- Algebra.forget₂_Module_preserves_limits
- Algebra.forget_preserves_limits
- Top.forget_preserves_limits
- category_theory.limits.evaluation_preserves_limits
- category_theory.yoneda_preserves_limits
- category_theory.coyoneda_preserves_limits
- Mon_.forget_preserves_limits
- preserves_colimits_of_shape : Π {J : Type ?} [𝒥 : category_theory.small_category J], category_theory.limits.preserves_colimits_of_shape J F
We say that F
preserves colimits if it sends colimit cocones over any diagram to colimit
cocones.
Instances
- category_theory.preserves_colimits_of_creates_colimits_and_has_colimits
- category_theory.adjunction.is_equivalence_preserves_colimits
- category_theory.limits.id_preserves_colimits
- category_theory.limits.comp_preserves_colimits
- Top.forget_preserves_colimits
- category_theory.limits.evaluation_preserves_colimits
- algebraic_geometry.PresheafedSpace.forget_preserves_colimits
- category_theory.obj.limits.preserves_colimits
- category_theory.colimit_adj.extend_along_yoneda.category_theory.limits.preserves_colimits
A convenience function for preserves_limit
, which takes the functor as an explicit argument to
guide typeclass resolution.
A convenience function for preserves_colimit
, which takes the functor as an explicit argument to
guide typeclass resolution.
Equations
- category_theory.limits.id_preserves_limits = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), {preserves_limit := λ (K : J ⥤ C), {preserves := λ (c : category_theory.limits.cone K) (h : category_theory.limits.is_limit c), {lift := λ (s : category_theory.limits.cone (K ⋙ 𝟭 C)), h.lift {X := s.X, π := {app := λ (j : J), s.π.app j, naturality' := _}}, fac' := _, uniq' := _}}}}
Equations
- category_theory.limits.id_preserves_colimits = {preserves_colimits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), {preserves_colimit := λ (K : J ⥤ C), {preserves := λ (c : category_theory.limits.cocone K) (h : category_theory.limits.is_colimit c), {desc := λ (s : category_theory.limits.cocone (K ⋙ 𝟭 C)), h.desc {X := s.X, ι := {app := λ (j : J), s.ι.app j, naturality' := _}}, fac' := _, uniq' := _}}}}
Equations
- category_theory.limits.comp_preserves_limits_of_shape F G = {preserves_limit := λ (K : J ⥤ C), infer_instance}
Equations
- category_theory.limits.comp_preserves_limits F G = {preserves_limits_of_shape := λ (J : Type v) (𝒥₁ : category_theory.small_category J), infer_instance}
Equations
- category_theory.limits.comp_preserves_colimits_of_shape F G = {preserves_colimit := λ (K : J ⥤ C), infer_instance}
Equations
- category_theory.limits.comp_preserves_colimits F G = {preserves_colimits_of_shape := λ (J : Type v) (𝒥₁ : category_theory.small_category J), infer_instance}
If F preserves one limit cone for the diagram K, then it preserves any limit cone for K.
Equations
- category_theory.limits.preserves_limit_of_preserves_limit_cone h hF = {preserves := λ (t' : category_theory.limits.cone K) (h' : category_theory.limits.is_limit t'), hF.of_iso_limit ((category_theory.limits.cones.functoriality K F).map_iso (h.unique_up_to_iso h'))}
Transfer preservation of limits along a natural isomorphism in the diagram.
Equations
- category_theory.limits.preserves_limit_of_iso_diagram F h = {preserves := λ (c : category_theory.limits.cone K₂) (t : category_theory.limits.is_limit c), ⇑(category_theory.limits.is_limit.postcompose_inv_equiv (category_theory.iso_whisker_right h F) (F.map_cone c)) ((category_theory.limits.is_limit_of_preserves F (⇑((category_theory.limits.is_limit.postcompose_inv_equiv h c).symm) t)).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl (F.map_cone ((category_theory.limits.cones.postcompose h.inv).obj c)).X) _))}
Transfer preservation of a limit along a natural isomorphism in the functor.
Transfer preservation of limits of shape along a natural isomorphism in the functor.
Equations
Transfer preservation of limits along a natural isomorphism in the functor.
Equations
Transfer preservation of limits along a equivalence in the shape.
Equations
- category_theory.limits.preserves_limits_of_shape_of_equiv e F = {preserves_limit := λ (K : J' ⥤ C), {preserves := λ (c : category_theory.limits.cone K) (t : category_theory.limits.is_limit c), let equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.inv_fun_id_assoc (K ⋙ F) in (⇑((category_theory.limits.is_limit.postcompose_hom_equiv equ (category_theory.limits.cone.whisker e.symm.functor (F.map_cone (category_theory.limits.cone.whisker e.functor c)))).symm) ((category_theory.limits.is_limit_of_preserves F (t.whisker_equivalence e)).whisker_equivalence e.symm)).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose equ.hom).obj (category_theory.limits.cone.whisker e.symm.functor (F.map_cone (category_theory.limits.cone.whisker e.functor c)))).X) _)}}
If F preserves one colimit cocone for the diagram K, then it preserves any colimit cocone for K.
Equations
- category_theory.limits.preserves_colimit_of_preserves_colimit_cocone h hF = {preserves := λ (t' : category_theory.limits.cocone K) (h' : category_theory.limits.is_colimit t'), hF.of_iso_colimit ((category_theory.limits.cocones.functoriality K F).map_iso (h.unique_up_to_iso h'))}
Transfer preservation of colimits along a natural isomorphism in the shape.
Equations
- category_theory.limits.preserves_colimit_of_iso_diagram F h = {preserves := λ (c : category_theory.limits.cocone K₂) (t : category_theory.limits.is_colimit c), ⇑(category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.iso_whisker_right h F) (F.map_cocone c)) ((category_theory.limits.is_colimit_of_preserves F (⇑((category_theory.limits.is_colimit.precompose_hom_equiv h c).symm) t)).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl (F.map_cocone ((category_theory.limits.cocones.precompose h.hom).obj c)).X) _))}
Transfer preservation of a colimit along a natural isomorphism in the functor.
Transfer preservation of colimits of shape along a natural isomorphism in the functor.
Equations
Transfer preservation of colimits along a natural isomorphism in the functor.
Equations
Transfer preservation of colimits along a equivalence in the shape.
Equations
- category_theory.limits.preserves_colimits_of_shape_of_equiv e F = {preserves_colimit := λ (K : J' ⥤ C), {preserves := λ (c : category_theory.limits.cocone K) (t : category_theory.limits.is_colimit c), let equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.inv_fun_id_assoc (K ⋙ F) in (⇑((category_theory.limits.is_colimit.precompose_inv_equiv equ (category_theory.limits.cocone.whisker e.symm.functor (F.map_cocone (category_theory.limits.cocone.whisker e.functor c)))).symm) ((category_theory.limits.is_colimit_of_preserves F (t.whisker_equivalence e)).whisker_equivalence e.symm)).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose equ.inv).obj (category_theory.limits.cocone.whisker e.symm.functor (F.map_cocone (category_theory.limits.cocone.whisker e.functor c)))).X) _)}}
- reflects : Π {c : category_theory.limits.cone K}, category_theory.limits.is_limit (F.map_cone c) → category_theory.limits.is_limit c
A functor F : C ⥤ D
reflects limits for K : J ⥤ C
if
whenever the image of a cone over K
under F
is a limit cone in D
,
the cone was already a limit cone in C
.
Note that we do not assume a priori that D
actually has any limits.
- reflects : Π {c : category_theory.limits.cocone K}, category_theory.limits.is_colimit (F.map_cocone c) → category_theory.limits.is_colimit c
A functor F : C ⥤ D
reflects colimits for K : J ⥤ C
if
whenever the image of a cocone over K
under F
is a colimit cocone in D
,
the cocone was already a colimit cocone in C
.
Note that we do not assume a priori that D
actually has any colimits.
- reflects_limit : Π {K : J ⥤ C}, category_theory.limits.reflects_limit K F
A functor F : C ⥤ D
reflects limits of shape J
if
whenever the image of a cone over some K : J ⥤ C
under F
is a limit cone in D
,
the cone was already a limit cone in C
.
Note that we do not assume a priori that D
actually has any limits.
- reflects_colimit : Π {K : J ⥤ C}, category_theory.limits.reflects_colimit K F
A functor F : C ⥤ D
reflects colimits of shape J
if
whenever the image of a cocone over some K : J ⥤ C
under F
is a colimit cocone in D
,
the cocone was already a colimit cocone in C
.
Note that we do not assume a priori that D
actually has any colimits.
- reflects_limits_of_shape : Π {J : Type ?} {𝒥 : category_theory.small_category J}, category_theory.limits.reflects_limits_of_shape J F
A functor F : C ⥤ D
reflects limits if
whenever the image of a cone over some K : J ⥤ C
under F
is a limit cone in D
,
the cone was already a limit cone in C
.
Note that we do not assume a priori that D
actually has any limits.
- reflects_colimits_of_shape : Π {J : Type ?} {𝒥 : category_theory.small_category J}, category_theory.limits.reflects_colimits_of_shape J F
A functor F : C ⥤ D
reflects colimits if
whenever the image of a cocone over some K : J ⥤ C
under F
is a colimit cocone in D
,
the cocone was already a colimit cocone in C
.
Note that we do not assume a priori that D
actually has any colimits.
A convenience function for reflects_limit
, which takes the functor as an explicit argument to
guide typeclass resolution.
A convenience function for reflects_colimit
, which takes the functor as an explicit argument to
guide typeclass resolution.
Equations
- category_theory.limits.id_reflects_limits = {reflects_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), {reflects_limit := λ (K : J ⥤ C), {reflects := λ (c : category_theory.limits.cone K) (h : category_theory.limits.is_limit ((𝟭 C).map_cone c)), {lift := λ (s : category_theory.limits.cone K), h.lift {X := s.X, π := {app := λ (j : J), s.π.app j, naturality' := _}}, fac' := _, uniq' := _}}}}
Equations
- category_theory.limits.id_reflects_colimits = {reflects_colimits_of_shape := λ (J : Type v) (𝒥 : category_theory.small_category J), {reflects_colimit := λ (K : J ⥤ C), {reflects := λ (c : category_theory.limits.cocone K) (h : category_theory.limits.is_colimit ((𝟭 C).map_cocone c)), {desc := λ (s : category_theory.limits.cocone K), h.desc {X := s.X, ι := {app := λ (j : J), s.ι.app j, naturality' := _}}, fac' := _, uniq' := _}}}}
Equations
Equations
- category_theory.limits.comp_reflects_limits_of_shape F G = {reflects_limit := λ (K : J ⥤ C), infer_instance}
Equations
- category_theory.limits.comp_reflects_limits F G = {reflects_limits_of_shape := λ (J : Type v) (𝒥₁ : category_theory.small_category J), infer_instance}
Equations
Equations
- category_theory.limits.comp_reflects_colimits_of_shape F G = {reflects_colimit := λ (K : J ⥤ C), infer_instance}
Equations
- category_theory.limits.comp_reflects_colimits F G = {reflects_colimits_of_shape := λ (J : Type v) (𝒥₁ : category_theory.small_category J), infer_instance}
If F ⋙ G
preserves limits for K
, and G
reflects limits for K ⋙ F
,
then F
preserves limits for K
.
Equations
If F ⋙ G
preserves limits of shape J
and G
reflects limits of shape J
, then F
preserves
limits of shape J
.
Equations
If F ⋙ G
preserves limits and G
reflects limits, then F
preserves limits.
Equations
Transfer reflection of a limit along a natural isomorphism in the functor.
Equations
Transfer reflection of limits of shape along a natural isomorphism in the functor.
Equations
Transfer reflection of limits along a natural isomorphism in the functor.
Equations
If the limit of F
exists and G
preserves it, then if G
reflects isomorphisms then it
reflects the limit of F
.
Equations
If C
has limits of shape J
and G
preserves them, then if G
reflects isomorphisms then it
reflects limits of shape J
.
If C
has limits and G
preserves limits, then if G
reflects isomorphisms then it reflects
limits.
If F ⋙ G
preserves colimits for K
, and G
reflects colimits for K ⋙ F
,
then F
preserves colimits for K
.
If F ⋙ G
preserves colimits of shape J
and G
reflects colimits of shape J
, then F
preserves colimits of shape J
.
If F ⋙ G
preserves colimits and G
reflects colimits, then F
preserves colimits.
Equations
Transfer reflection of a colimit along a natural isomorphism in the functor.
Transfer reflection of colimits of shape along a natural isomorphism in the functor.
Equations
Transfer reflection of colimits along a natural isomorphism in the functor.
Equations
If the colimit of F
exists and G
preserves it, then if G
reflects isomorphisms then it
reflects the colimit of F
.
Equations
If C
has colimits of shape J
and G
preserves them, then if G
reflects isomorphisms then it
reflects colimits of shape J
.
If C
has colimits and G
preserves colimits, then if G
reflects isomorphisms then it reflects
colimits.
A fully faithful functor reflects limits.
Equations
- category_theory.limits.fully_faithful_reflects_limits F = {reflects_limits_of_shape := λ (J : Type v) (𝒥₁ : category_theory.small_category J), {reflects_limit := λ (K : J ⥤ C), {reflects := λ (c : category_theory.limits.cone K) (t : category_theory.limits.is_limit (F.map_cone c)), category_theory.limits.is_limit.mk_cone_morphism (λ (s : category_theory.limits.cone K), (category_theory.limits.cones.functoriality K F).preimage (t.lift_cone_morphism ((category_theory.limits.cones.functoriality K F).obj s))) _}}}
A fully faithful functor reflects colimits.
Equations
- category_theory.limits.fully_faithful_reflects_colimits F = {reflects_colimits_of_shape := λ (J : Type v) (𝒥₁ : category_theory.small_category J), {reflects_colimit := λ (K : J ⥤ C), {reflects := λ (c : category_theory.limits.cocone K) (t : category_theory.limits.is_colimit (F.map_cocone c)), category_theory.limits.is_colimit.mk_cocone_morphism (λ (s : category_theory.limits.cocone K), (category_theory.limits.cocones.functoriality K F).preimage (t.desc_cocone_morphism ((category_theory.limits.cocones.functoriality K F).obj s))) _}}}