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] :
- 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] :
- 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] :
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] :
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] :
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
- 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.under.forget_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] :
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
- Top.forget_preserves_colimits
- category_theory.limits.evaluation_preserves_colimits
- algebraic_geometry.PresheafedSpace.forget_preserves_colimits
- category_theory.over.forget_preserves_colimits
- category_theory.colimit_adj.category_theory.limits.preserves_colimits
@[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_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] :
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} :
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
{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 shape.
Equations
- category_theory.limits.preserves_limit_of_iso F h = {preserves := λ (c : category_theory.limits.cone K₂) (t : category_theory.limits.is_limit c), let hF : K₁ ⋙ F ≅ K₂ ⋙ F := category_theory.iso_whisker_right h F in (category_theory.limits.is_limit.of_right_adjoint (category_theory.limits.cones.postcompose_equivalence hF).functor (category_theory.limits.preserves_limit.preserves (category_theory.limits.is_limit.of_right_adjoint (category_theory.limits.cones.postcompose_equivalence h).inverse t))).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose_equivalence hF).functor.obj (F.map_cone ((category_theory.limits.cones.postcompose_equivalence h).inverse.obj 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} :
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
{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 F h = {preserves := λ (c : category_theory.limits.cocone K₂) (t : category_theory.limits.is_colimit c), let hF : K₁ ⋙ F ≅ K₂ ⋙ F := category_theory.iso_whisker_right h F in (category_theory.limits.is_colimit.of_left_adjoint (category_theory.limits.cocones.precompose_equivalence hF).inverse (category_theory.limits.preserves_colimit.preserves (category_theory.limits.is_colimit.of_left_adjoint (category_theory.limits.cocones.precompose_equivalence h).functor t))).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose_equivalence hF).inverse.obj (F.map_cocone ((category_theory.limits.cocones.precompose_equivalence h).functor.obj c))).X) _)}
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.
@[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] :
- 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] :
- 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] :
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] :
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] :
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] :
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.
@[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_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
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.
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.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))) _}}}