# mathlib3documentation

category_theory.limits.preserves.basic

# Preservation and reflection of (co)limits. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w)
• preserves :

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.

Instances of this typeclass
Instances of other typeclasses for `category_theory.limits.preserves_limit`
@[class]
structure category_theory.limits.preserves_colimit {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w)
• preserves :

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.

Instances of this typeclass
Instances of other typeclasses for `category_theory.limits.preserves_colimit`
@[class]
structure category_theory.limits.preserves_limits_of_shape {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w w')
• preserves_limit : (Π {K : J C}, . "apply_instance"

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.

Instances of this typeclass
Instances of other typeclasses for `category_theory.limits.preserves_limits_of_shape`
@[class]
structure category_theory.limits.preserves_colimits_of_shape {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w w')
• preserves_colimit : (Π {K : J C}, . "apply_instance"

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.

Instances of this typeclass
Instances of other typeclasses for `category_theory.limits.preserves_colimits_of_shape`
@[nolint, class]
structure category_theory.limits.preserves_limits_of_size {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ v₂ (w+1) (w'+1))
• preserves_limits_of_shape : (Π {J : Type ?} [_inst_4 : , . "apply_instance"

`preserves_limits_of_size.{v u} F` means that `F` sends all limit cones over any diagram `J ⥤ C` to limit cones, where `J : Type u` with `[category.{v} J]`.

Instances of this typeclass
Instances of other typeclasses for `category_theory.limits.preserves_limits_of_size`
@[reducible]
def category_theory.limits.preserves_limits {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ (v₂+1))

We say that `F` preserves (small) limits if it sends small limit cones over any diagram to limit cones.

@[nolint, class]
structure category_theory.limits.preserves_colimits_of_size {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ v₂ (w+1) (w'+1))
• preserves_colimits_of_shape : (Π {J : Type ?} [_inst_4 : , . "apply_instance"

`preserves_colimits_of_size.{v u} F` means that `F` sends all colimit cocones over any diagram `J ⥤ C` to colimit cocones, where `J : Type u` with `[category.{v} J]`.

Instances of this typeclass
Instances of other typeclasses for `category_theory.limits.preserves_colimits_of_size`
@[reducible]
def category_theory.limits.preserves_colimits {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ (v₂+1))

We say that `F` preserves (small) limits if it sends small limit cones over any diagram to limit cones.

def category_theory.limits.is_limit_of_preserves {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} (F : C D)  :

A convenience function for `preserves_limit`, which takes the functor as an explicit argument to guide typeclass resolution.

Equations
def category_theory.limits.is_colimit_of_preserves {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} (F : C D)  :

A convenience function for `preserves_colimit`, which takes the functor as an explicit argument to guide typeclass resolution.

Equations
@[protected, instance]
def category_theory.limits.preserves_limit_subsingleton {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
@[protected, instance]
def category_theory.limits.preserves_colimit_subsingleton {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
@[protected, instance]
def category_theory.limits.preserves_limits_of_shape_subsingleton {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
@[protected, instance]
def category_theory.limits.preserves_colimits_of_shape_subsingleton {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
@[protected, instance]
def category_theory.limits.preserves_limits_subsingleton {C : Type u₁} {D : Type u₂} (F : C D) :
@[protected, instance]
def category_theory.limits.preserves_colimits_subsingleton {C : Type u₁} {D : Type u₂} (F : C D) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def category_theory.limits.comp_preserves_limit {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E) [ G] :
Equations
@[protected, instance]
def category_theory.limits.comp_preserves_limits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
@[protected, instance]
def category_theory.limits.comp_preserves_limits {C : Type u₁} {D : Type u₂} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
@[protected, instance]
def category_theory.limits.comp_preserves_colimit {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
@[protected, instance]
def category_theory.limits.comp_preserves_colimits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
@[protected, instance]
def category_theory.limits.comp_preserves_colimits {C : Type u₁} {D : Type u₂} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations

If F preserves one limit cone for the diagram K, then it preserves any limit cone for K.

Equations
def category_theory.limits.preserves_limit_of_iso_diagram {C : Type u₁} {D : Type u₂} {J : Type w} {K₁ K₂ : J C} (F : C D) (h : K₁ K₂)  :

Transfer preservation of limits along a natural isomorphism in the diagram.

Equations
def category_theory.limits.preserves_limit_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) {F G : C D} (h : F G)  :

Transfer preservation of a limit along a natural isomorphism in the functor.

Equations
def category_theory.limits.preserves_limits_of_shape_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} {F G : C D} (h : F G)  :

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₁} {D : Type u₂} {F G : C D} (h : F G)  :

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₁} {D : Type u₂} {J : Type w} {J' : Type w₂} (e : J J') (F : C D)  :

Transfer preservation of limits along a equivalence in the shape.

Equations

`preserves_limits_of_size_shrink.{w w'} F` tries to obtain `preserves_limits_of_size.{w w'} F` from some other `preserves_limits_of_size F`.

Equations

Preserving limits at any universe level implies preserving limits in universe `0`.

Equations

If F preserves one colimit cocone for the diagram K, then it preserves any colimit cocone for K.

Equations
def category_theory.limits.preserves_colimit_of_iso_diagram {C : Type u₁} {D : Type u₂} {J : Type w} {K₁ K₂ : J C} (F : C D) (h : K₁ K₂)  :

Transfer preservation of colimits along a natural isomorphism in the shape.

Equations
def category_theory.limits.preserves_colimit_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) {F G : C D} (h : F G)  :

Transfer preservation of a colimit along a natural isomorphism in the functor.

Equations
def category_theory.limits.preserves_colimits_of_shape_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} {F G : C D} (h : F G)  :

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₁} {D : Type u₂} {F G : C D} (h : F G)  :

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₁} {D : Type u₂} {J : Type w} {J' : Type w₂} (e : J J') (F : C D)  :

Transfer preservation of colimits along a equivalence in the shape.

Equations

`preserves_colimits_of_size_shrink.{w w'} F` tries to obtain `preserves_colimits_of_size.{w w'} F` from some other `preserves_colimits_of_size F`.

Equations

Preserving colimits at any universe implies preserving colimits at universe `0`.

Equations
@[class]
structure category_theory.limits.reflects_limit {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w)
• reflects :

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.

Instances of this typeclass
Instances of other typeclasses for `category_theory.limits.reflects_limit`
@[class]
structure category_theory.limits.reflects_colimit {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w)
• reflects :

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.

Instances of this typeclass
Instances of other typeclasses for `category_theory.limits.reflects_colimit`
@[class]
structure category_theory.limits.reflects_limits_of_shape {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w w')
• reflects_limit : (Π {K : J C}, . "apply_instance"

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.

Instances of this typeclass
Instances of other typeclasses for `category_theory.limits.reflects_limits_of_shape`
@[class]
structure category_theory.limits.reflects_colimits_of_shape {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
Type (max u₁ u₂ v₁ v₂ w w')
• reflects_colimit : (Π {K : J C}, . "apply_instance"

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.

Instances of this typeclass
Instances of other typeclasses for `category_theory.limits.reflects_colimits_of_shape`
@[nolint, class]
structure category_theory.limits.reflects_limits_of_size {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ v₂ (w+1) (w'+1))
• reflects_limits_of_shape : (Π {J : Type ?} [_inst_4 : , . "apply_instance"

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.

Instances of this typeclass
Instances of other typeclasses for `category_theory.limits.reflects_limits_of_size`
@[reducible]
def category_theory.limits.reflects_limits {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ (v₂+1))

A functor `F : C ⥤ D` reflects (small) 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.

@[nolint, class]
structure category_theory.limits.reflects_colimits_of_size {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ v₂ (w+1) (w'+1))
• reflects_colimits_of_shape : (Π {J : Type ?} [_inst_4 : , . "apply_instance"

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.

Instances of this typeclass
Instances of other typeclasses for `category_theory.limits.reflects_colimits_of_size`
@[reducible]
def category_theory.limits.reflects_colimits {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ u₂ v₁ (v₂+1))

A functor `F : C ⥤ D` reflects (small) 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₁} {D : Type u₂} {J : Type w} {K : J C} (F : C D) (t : category_theory.limits.is_limit (F.map_cone c))  :

A convenience function for `reflects_limit`, which takes the functor as an explicit argument to guide typeclass resolution.

Equations
def category_theory.limits.is_colimit_of_reflects {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} (F : C D) (t : category_theory.limits.is_colimit (F.map_cocone c))  :

A convenience function for `reflects_colimit`, which takes the functor as an explicit argument to guide typeclass resolution.

Equations
@[protected, instance]
def category_theory.limits.reflects_limit_subsingleton {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
@[protected, instance]
def category_theory.limits.reflects_colimit_subsingleton {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D) :
@[protected, instance]
def category_theory.limits.reflects_limits_of_shape_subsingleton {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
@[protected, instance]
def category_theory.limits.reflects_colimits_of_shape_subsingleton {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D) :
@[protected, instance]
def category_theory.limits.reflects_limits_subsingleton {C : Type u₁} {D : Type u₂} (F : C D) :
@[protected, instance]
def category_theory.limits.reflects_colimits_subsingleton {C : Type u₁} {D : Type u₂} (F : C D) :
@[protected, instance]
def category_theory.limits.reflects_limit_of_reflects_limits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D)  :
Equations
@[protected, instance]
def category_theory.limits.reflects_colimit_of_reflects_colimits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) (F : C D)  :
Equations
@[protected, instance]
def category_theory.limits.reflects_limits_of_shape_of_reflects_limits {C : Type u₁} {D : Type u₂} (J : Type w) (F : C D)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def category_theory.limits.comp_reflects_limit {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E) [ G] :
Equations
@[protected, instance]
def category_theory.limits.comp_reflects_limits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
@[protected, instance]
def category_theory.limits.comp_reflects_limits {C : Type u₁} {D : Type u₂} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
@[protected, instance]
def category_theory.limits.comp_reflects_colimit {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E) [ G] :
Equations
@[protected, instance]
def category_theory.limits.comp_reflects_colimits_of_shape {C : Type u₁} {D : Type u₂} {J : Type w} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
@[protected, instance]
def category_theory.limits.comp_reflects_colimits {C : Type u₁} {D : Type u₂} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :
Equations
def category_theory.limits.preserves_limit_of_reflects_of_preserves {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E) [ (F G)] [ 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₁} {D : Type u₂} {J : Type w} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :

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₁} {D : Type u₂} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :

If `F ⋙ G` preserves limits and `G` reflects limits, then `F` preserves limits.

Equations
def category_theory.limits.reflects_limit_of_iso_diagram {C : Type u₁} {D : Type u₂} {J : Type w} {K₁ K₂ : J C} (F : C D) (h : K₁ K₂)  :

Transfer reflection of limits along a natural isomorphism in the diagram.

Equations
def category_theory.limits.reflects_limit_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) {F G : C D} (h : F G)  :

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₁} {D : Type u₂} {J : Type w} {F G : C D} (h : F G)  :

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₁} {D : Type u₂} {F G : C D} (h : F G)  :

Transfer reflection of limits along a natural isomorphism in the functor.

Equations
def category_theory.limits.reflects_limits_of_shape_of_equiv {C : Type u₁} {D : Type u₂} {J : Type w} {J' : Type w₂} (e : J J') (F : C D)  :

Transfer reflection of limits along a equivalence in the shape.

Equations

`reflects_limits_of_size_shrink.{w w'} F` tries to obtain `reflects_limits_of_size.{w w'} F` from some other `reflects_limits_of_size F`.

Equations

Reflecting limits at any universe implies reflecting limits at universe `0`.

Equations
noncomputable def category_theory.limits.reflects_limit_of_reflects_isomorphisms {C : Type u₁} {D : Type u₂} {J : Type w} (F : J C) (G : C D)  :

If the limit of `F` exists and `G` preserves it, then if `G` reflects isomorphisms then it reflects the limit of `F`.

Equations
noncomputable def category_theory.limits.reflects_limits_of_shape_of_reflects_isomorphisms {C : Type u₁} {D : Type u₂} {J : Type w} {G : C D}  :

If `C` has limits of shape `J` and `G` preserves them, then if `G` reflects isomorphisms then it reflects limits of shape `J`.

Equations

If `C` has limits and `G` preserves limits, then if `G` reflects isomorphisms then it reflects limits.

Equations
def category_theory.limits.preserves_colimit_of_reflects_of_preserves {C : Type u₁} {D : Type u₂} {J : Type w} {K : J C} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E) [ G] :

If `F ⋙ G` preserves colimits for `K`, and `G` reflects colimits for `K ⋙ F`, then `F` preserves colimits for `K`.

Equations
def category_theory.limits.preserves_colimits_of_shape_of_reflects_of_preserves {C : Type u₁} {D : Type u₂} {J : Type w} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :

If `F ⋙ G` preserves colimits of shape `J` and `G` reflects colimits of shape `J`, then `F` preserves colimits of shape `J`.

Equations
def category_theory.limits.preserves_colimits_of_reflects_of_preserves {C : Type u₁} {D : Type u₂} {E : Type u₃} [ℰ : category_theory.category E] (F : C D) (G : D E)  :

If `F ⋙ G` preserves colimits and `G` reflects colimits, then `F` preserves colimits.

Equations
def category_theory.limits.reflects_colimit_of_iso_diagram {C : Type u₁} {D : Type u₂} {J : Type w} {K₁ K₂ : J C} (F : C D) (h : K₁ K₂)  :

Transfer reflection of colimits along a natural isomorphism in the diagram.

Equations
def category_theory.limits.reflects_colimit_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} (K : J C) {F G : C D} (h : F G)  :

Transfer reflection of a colimit along a natural isomorphism in the functor.

Equations
def category_theory.limits.reflects_colimits_of_shape_of_nat_iso {C : Type u₁} {D : Type u₂} {J : Type w} {F G : C D} (h : F G)  :

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₁} {D : Type u₂} {F G : C D} (h : F G)  :

Transfer reflection of colimits along a natural isomorphism in the functor.

Equations
def category_theory.limits.reflects_colimits_of_shape_of_equiv {C : Type u₁} {D : Type u₂} {J : Type w} {J' : Type w₂} (e : J J') (F : C D)  :

Transfer reflection of colimits along a equivalence in the shape.

Equations

`reflects_colimits_of_size_shrink.{w w'} F` tries to obtain `reflects_colimits_of_size.{w w'} F` from some other `reflects_colimits_of_size F`.

Equations

Reflecting colimits at any universe implies reflecting colimits at universe `0`.

Equations
noncomputable def category_theory.limits.reflects_colimit_of_reflects_isomorphisms {C : Type u₁} {D : Type u₂} {J : Type w} (F : J C) (G : C D)  :

If the colimit of `F` exists and `G` preserves it, then if `G` reflects isomorphisms then it reflects the colimit of `F`.

Equations
noncomputable def category_theory.limits.reflects_colimits_of_shape_of_reflects_isomorphisms {C : Type u₁} {D : Type u₂} {J : Type w} {G : C D}  :

If `C` has colimits of shape `J` and `G` preserves them, then if `G` reflects isomorphisms then it reflects colimits of shape `J`.

Equations

If `C` has colimits and `G` preserves colimits, then if `G` reflects isomorphisms then it reflects colimits.

Equations
def category_theory.limits.fully_faithful_reflects_limits {C : Type u₁} {D : Type u₂} (F : C D)  :

A fully faithful functor reflects limits.

Equations

A fully faithful functor reflects colimits.

Equations