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".
@[class]
structure
category_theory.limits.preserves_limit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
(F : C ⥤ D) :
Type (max u₁ u₂ v)
- 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.
@[class]
structure
category_theory.limits.preserves_colimit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
(F : C ⥤ D) :
Type (max u₁ u₂ v)
- 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.
@[class]
structure
category_theory.limits.preserves_limits_of_shape
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(J : Type v)
[category_theory.small_category J]
(F : C ⥤ D) :
Type (max u₁ u₂ v)
- 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.
@[class]
structure
category_theory.limits.preserves_colimits_of_shape
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(J : Type v)
[category_theory.small_category J]
(F : C ⥤ D) :
Type (max u₁ u₂ v)
- 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.
@[class]
structure
category_theory.limits.preserves_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
Type (max u₁ u₂ (v+1))
- 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
@[class]
structure
category_theory.limits.preserves_colimits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
Type (max u₁ u₂ (v+1))
- 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
def
category_theory.limits.is_limit_of_preserves
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ C}
(F : C ⥤ D)
{c : category_theory.limits.cone K}
(t : category_theory.limits.is_limit c)
[category_theory.limits.preserves_limit K F] :
A convenience function for preserves_limit, which takes the functor as an explicit argument to
guide typeclass resolution.
def
category_theory.limits.is_colimit_of_preserves
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ C}
(F : C ⥤ D)
{c : category_theory.limits.cocone K}
(t : category_theory.limits.is_colimit c)
[category_theory.limits.preserves_colimit K F] :
A convenience function for preserves_colimit, which takes the functor as an explicit argument to
guide typeclass resolution.
@[instance]
def
category_theory.limits.preserves_limit_subsingleton
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
(F : C ⥤ D) :
@[instance]
def
category_theory.limits.preserves_colimit_subsingleton
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
(F : C ⥤ D) :
@[instance]
def
category_theory.limits.preserves_limits_of_shape_subsingleton
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(J : Type v)
[category_theory.small_category J]
(F : C ⥤ D) :
@[instance]
def
category_theory.limits.preserves_colimits_of_shape_subsingleton
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(J : Type v)
[category_theory.small_category J]
(F : C ⥤ D) :
@[instance]
def
category_theory.limits.preserves_limits_subsingleton
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
@[instance]
def
category_theory.limits.preserves_colimits_subsingleton
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
@[instance]
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' := _}}}}
@[instance]
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' := _}}}}
@[instance]
def
category_theory.limits.comp_preserves_limit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ C}
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.preserves_limit K F]
[category_theory.limits.preserves_limit (K ⋙ F) G] :
@[instance]
def
category_theory.limits.comp_preserves_limits_of_shape
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.preserves_limits_of_shape J F]
[category_theory.limits.preserves_limits_of_shape J G] :
Equations
- category_theory.limits.comp_preserves_limits_of_shape F G = {preserves_limit := λ (K : J ⥤ C), infer_instance}
@[instance]
def
category_theory.limits.comp_preserves_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.preserves_limits F]
[category_theory.limits.preserves_limits G] :
Equations
- category_theory.limits.comp_preserves_limits F G = {preserves_limits_of_shape := λ (J : Type v) (𝒥₁ : category_theory.small_category J), infer_instance}
@[instance]
def
category_theory.limits.comp_preserves_colimit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ C}
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.preserves_colimit K F]
[category_theory.limits.preserves_colimit (K ⋙ F) G] :
@[instance]
def
category_theory.limits.comp_preserves_colimits_of_shape
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.preserves_colimits_of_shape J F]
[category_theory.limits.preserves_colimits_of_shape J G] :
Equations
- category_theory.limits.comp_preserves_colimits_of_shape F G = {preserves_colimit := λ (K : J ⥤ C), infer_instance}
@[instance]
def
category_theory.limits.comp_preserves_colimits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.preserves_colimits F]
[category_theory.limits.preserves_colimits G] :
Equations
- category_theory.limits.comp_preserves_colimits F G = {preserves_colimits_of_shape := λ (J : Type v) (𝒥₁ : category_theory.small_category J), infer_instance}
def
category_theory.limits.preserves_limit_of_preserves_limit_cone
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ C}
{F : C ⥤ D}
{t : category_theory.limits.cone K}
(h : category_theory.limits.is_limit t)
(hF : category_theory.limits.is_limit (F.map_cone t)) :
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'))}
def
category_theory.limits.preserves_limit_of_iso_diagram
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{K₁ K₂ : J ⥤ C}
(F : C ⥤ D)
(h : K₁ ≅ K₂)
[category_theory.limits.preserves_limit K₁ F] :
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) _))}
def
category_theory.limits.preserves_limit_of_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
{F G : C ⥤ D}
(h : F ≅ G)
[category_theory.limits.preserves_limit K F] :
Transfer preservation of a limit along a natural isomorphism in the functor.
def
category_theory.limits.preserves_limits_of_shape_of_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{F G : C ⥤ D}
(h : F ≅ G)
[category_theory.limits.preserves_limits_of_shape J F] :
Transfer preservation of limits of shape along a natural isomorphism in the functor.
Equations
def
category_theory.limits.preserves_limits_of_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(h : F ≅ G)
[category_theory.limits.preserves_limits F] :
Transfer preservation of limits along a natural isomorphism in the functor.
Equations
def
category_theory.limits.preserves_limits_of_shape_of_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{J' : Type v}
[category_theory.small_category J']
(e : J ≌ J')
(F : C ⥤ D)
[category_theory.limits.preserves_limits_of_shape J F] :
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) _)}}
def
category_theory.limits.preserves_colimit_of_preserves_colimit_cocone
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ C}
{F : C ⥤ D}
{t : category_theory.limits.cocone K}
(h : category_theory.limits.is_colimit t)
(hF : category_theory.limits.is_colimit (F.map_cocone t)) :
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'))}
def
category_theory.limits.preserves_colimit_of_iso_diagram
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{K₁ K₂ : J ⥤ C}
(F : C ⥤ D)
(h : K₁ ≅ K₂)
[category_theory.limits.preserves_colimit K₁ F] :
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) _))}
def
category_theory.limits.preserves_colimit_of_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
{F G : C ⥤ D}
(h : F ≅ G)
[category_theory.limits.preserves_colimit K F] :
Transfer preservation of a colimit along a natural isomorphism in the functor.
def
category_theory.limits.preserves_colimits_of_shape_of_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{F G : C ⥤ D}
(h : F ≅ G)
[category_theory.limits.preserves_colimits_of_shape J F] :
Transfer preservation of colimits of shape along a natural isomorphism in the functor.
Equations
def
category_theory.limits.preserves_colimits_of_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(h : F ≅ G)
[category_theory.limits.preserves_colimits F] :
Transfer preservation of colimits along a natural isomorphism in the functor.
Equations
def
category_theory.limits.preserves_colimits_of_shape_of_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{J' : Type v}
[category_theory.small_category J']
(e : J ≌ J')
(F : C ⥤ D)
[category_theory.limits.preserves_colimits_of_shape J F] :
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) _)}}
@[class]
structure
category_theory.limits.reflects_limit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
(F : C ⥤ D) :
Type (max u₁ u₂ v)
- 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.
@[class]
structure
category_theory.limits.reflects_colimit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
(F : C ⥤ D) :
Type (max u₁ u₂ v)
- 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.
@[class]
structure
category_theory.limits.reflects_limits_of_shape
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(J : Type v)
[category_theory.small_category J]
(F : C ⥤ D) :
Type (max u₁ u₂ v)
- 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.
@[class]
structure
category_theory.limits.reflects_colimits_of_shape
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(J : Type v)
[category_theory.small_category J]
(F : C ⥤ D) :
Type (max u₁ u₂ v)
- 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.
@[class]
structure
category_theory.limits.reflects_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
Type (max u₁ u₂ (v+1))
- 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.
@[class]
structure
category_theory.limits.reflects_colimits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
Type (max u₁ u₂ (v+1))
- 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.
def
category_theory.limits.is_limit_of_reflects
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ C}
(F : C ⥤ D)
{c : category_theory.limits.cone K}
(t : category_theory.limits.is_limit (F.map_cone c))
[category_theory.limits.reflects_limit K F] :
A convenience function for reflects_limit, which takes the functor as an explicit argument to
guide typeclass resolution.
def
category_theory.limits.is_colimit_of_reflects
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ C}
(F : C ⥤ D)
{c : category_theory.limits.cocone K}
(t : category_theory.limits.is_colimit (F.map_cocone c))
[category_theory.limits.reflects_colimit K F] :
A convenience function for reflects_colimit, which takes the functor as an explicit argument to
guide typeclass resolution.
@[instance]
def
category_theory.limits.reflects_limit_subsingleton
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
(F : C ⥤ D) :
@[instance]
def
category_theory.limits.reflects_colimit_subsingleton
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
(F : C ⥤ D) :
@[instance]
def
category_theory.limits.reflects_limits_of_shape_subsingleton
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(J : Type v)
[category_theory.small_category J]
(F : C ⥤ D) :
@[instance]
def
category_theory.limits.reflects_colimits_of_shape_subsingleton
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(J : Type v)
[category_theory.small_category J]
(F : C ⥤ D) :
@[instance]
def
category_theory.limits.reflects_limits_subsingleton
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
@[instance]
def
category_theory.limits.reflects_colimits_subsingleton
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
@[instance]
def
category_theory.limits.reflects_limit_of_reflects_limits_of_shape
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
(F : C ⥤ D)
[H : category_theory.limits.reflects_limits_of_shape J F] :
@[instance]
def
category_theory.limits.reflects_colimit_of_reflects_colimits_of_shape
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
(F : C ⥤ D)
[H : category_theory.limits.reflects_colimits_of_shape J F] :
@[instance]
def
category_theory.limits.reflects_limits_of_shape_of_reflects_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(F : C ⥤ D)
[H : category_theory.limits.reflects_limits F] :
@[instance]
def
category_theory.limits.reflects_colimits_of_shape_of_reflects_colimits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(F : C ⥤ D)
[H : category_theory.limits.reflects_colimits F] :
@[instance]
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' := _}}}}
@[instance]
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' := _}}}}
@[instance]
def
category_theory.limits.comp_reflects_limit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ C}
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.reflects_limit K F]
[category_theory.limits.reflects_limit (K ⋙ F) G] :
Equations
@[instance]
def
category_theory.limits.comp_reflects_limits_of_shape
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.reflects_limits_of_shape J F]
[category_theory.limits.reflects_limits_of_shape J G] :
Equations
- category_theory.limits.comp_reflects_limits_of_shape F G = {reflects_limit := λ (K : J ⥤ C), infer_instance}
@[instance]
def
category_theory.limits.comp_reflects_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.reflects_limits F]
[category_theory.limits.reflects_limits G] :
Equations
- category_theory.limits.comp_reflects_limits F G = {reflects_limits_of_shape := λ (J : Type v) (𝒥₁ : category_theory.small_category J), infer_instance}
@[instance]
def
category_theory.limits.comp_reflects_colimit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ C}
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.reflects_colimit K F]
[category_theory.limits.reflects_colimit (K ⋙ F) G] :
Equations
@[instance]
def
category_theory.limits.comp_reflects_colimits_of_shape
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.reflects_colimits_of_shape J F]
[category_theory.limits.reflects_colimits_of_shape J G] :
Equations
- category_theory.limits.comp_reflects_colimits_of_shape F G = {reflects_colimit := λ (K : J ⥤ C), infer_instance}
@[instance]
def
category_theory.limits.comp_reflects_colimits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.reflects_colimits F]
[category_theory.limits.reflects_colimits G] :
Equations
- category_theory.limits.comp_reflects_colimits F G = {reflects_colimits_of_shape := λ (J : Type v) (𝒥₁ : category_theory.small_category J), infer_instance}
def
category_theory.limits.preserves_limit_of_reflects_of_preserves
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ C}
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.preserves_limit K (F ⋙ G)]
[category_theory.limits.reflects_limit (K ⋙ F) G] :
If F ⋙ G preserves limits for K, and G reflects limits for K ⋙ F,
then F preserves limits for K.
Equations
def
category_theory.limits.preserves_limits_of_shape_of_reflects_of_preserves
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.preserves_limits_of_shape J (F ⋙ G)]
[category_theory.limits.reflects_limits_of_shape J G] :
If F ⋙ G preserves limits of shape J and G reflects limits of shape J, then F preserves
limits of shape J.
Equations
def
category_theory.limits.preserves_limits_of_reflects_of_preserves
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.preserves_limits (F ⋙ G)]
[category_theory.limits.reflects_limits G] :
If F ⋙ G preserves limits and G reflects limits, then F preserves limits.
Equations
def
category_theory.limits.reflects_limit_of_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
{F G : C ⥤ D}
(h : F ≅ G)
[category_theory.limits.reflects_limit K F] :
Transfer reflection of a limit along a natural isomorphism in the functor.
Equations
def
category_theory.limits.reflects_limits_of_shape_of_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{F G : C ⥤ D}
(h : F ≅ G)
[category_theory.limits.reflects_limits_of_shape J F] :
Transfer reflection of limits of shape along a natural isomorphism in the functor.
Equations
def
category_theory.limits.reflects_limits_of_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(h : F ≅ G)
[category_theory.limits.reflects_limits F] :
Transfer reflection of limits along a natural isomorphism in the functor.
Equations
def
category_theory.limits.reflects_limit_of_reflects_isomorphisms
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
(G : C ⥤ D)
[category_theory.reflects_isomorphisms G]
[category_theory.limits.has_limit F]
[category_theory.limits.preserves_limit F G] :
If the limit of F exists and G preserves it, then if G reflects isomorphisms then it
reflects the limit of F.
Equations
def
category_theory.limits.reflects_limits_of_shape_of_reflects_isomorphisms
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{G : C ⥤ D}
[category_theory.reflects_isomorphisms G]
[category_theory.limits.has_limits_of_shape J C]
[category_theory.limits.preserves_limits_of_shape J G] :
If C has limits of shape J and G preserves them, then if G reflects isomorphisms then it
reflects limits of shape J.
def
category_theory.limits.reflects_limits_of_reflects_isomorphisms
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G : C ⥤ D}
[category_theory.reflects_isomorphisms G]
[category_theory.limits.has_limits C]
[category_theory.limits.preserves_limits G] :
If C has limits and G preserves limits, then if G reflects isomorphisms then it reflects
limits.
def
category_theory.limits.preserves_colimit_of_reflects_of_preserves
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{K : J ⥤ C}
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.preserves_colimit K (F ⋙ G)]
[category_theory.limits.reflects_colimit (K ⋙ F) G] :
If F ⋙ G preserves colimits for K, and G reflects colimits for K ⋙ F,
then F preserves colimits for K.
def
category_theory.limits.preserves_colimits_of_shape_of_reflects_of_preserves
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.preserves_colimits_of_shape J (F ⋙ G)]
[category_theory.limits.reflects_colimits_of_shape J G] :
If F ⋙ G preserves colimits of shape J and G reflects colimits of shape J, then F
preserves colimits of shape J.
def
category_theory.limits.preserves_colimits_of_reflects_of_preserves
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[ℰ : category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.limits.preserves_colimits (F ⋙ G)]
[category_theory.limits.reflects_colimits G] :
If F ⋙ G preserves colimits and G reflects colimits, then F preserves colimits.
Equations
def
category_theory.limits.reflects_colimit_of_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(K : J ⥤ C)
{F G : C ⥤ D}
(h : F ≅ G)
[category_theory.limits.reflects_colimit K F] :
Transfer reflection of a colimit along a natural isomorphism in the functor.
def
category_theory.limits.reflects_colimits_of_shape_of_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{F G : C ⥤ D}
(h : F ≅ G)
[category_theory.limits.reflects_colimits_of_shape J F] :
Transfer reflection of colimits of shape along a natural isomorphism in the functor.
Equations
def
category_theory.limits.reflects_colimits_of_nat_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(h : F ≅ G)
[category_theory.limits.reflects_colimits F] :
Transfer reflection of colimits along a natural isomorphism in the functor.
Equations
def
category_theory.limits.reflects_colimit_of_reflects_isomorphisms
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
(F : J ⥤ C)
(G : C ⥤ D)
[category_theory.reflects_isomorphisms G]
[category_theory.limits.has_colimit F]
[category_theory.limits.preserves_colimit F G] :
If the colimit of F exists and G preserves it, then if G reflects isomorphisms then it
reflects the colimit of F.
Equations
def
category_theory.limits.reflects_colimits_of_shape_of_reflects_isomorphisms
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{J : Type v}
[category_theory.small_category J]
{G : C ⥤ D}
[category_theory.reflects_isomorphisms G]
[category_theory.limits.has_colimits_of_shape J C]
[category_theory.limits.preserves_colimits_of_shape J G] :
If C has colimits of shape J and G preserves them, then if G reflects isomorphisms then it
reflects colimits of shape J.
def
category_theory.limits.reflects_colimits_of_reflects_isomorphisms
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{G : C ⥤ D}
[category_theory.reflects_isomorphisms G]
[category_theory.limits.has_colimits C]
[category_theory.limits.preserves_colimits G] :
If C has colimits and G preserves colimits, then if G reflects isomorphisms then it reflects
colimits.
def
category_theory.limits.fully_faithful_reflects_limits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.full F]
[category_theory.faithful F] :
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))) _}}}
def
category_theory.limits.fully_faithful_reflects_colimits
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.full F]
[category_theory.faithful F] :
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))) _}}}