# Relating monomorphisms and epimorphisms to limits and colimits #

If F preserves (resp. reflects) pullbacks, then it preserves (resp. reflects) monomorphisms.

We also provide the dual version for epimorphisms.

theorem CategoryTheory.preserves_mono_of_preservesLimit {C : Type u₁} {D : Type u₂} [] [] (F : ) {X : C} {Y : C} (f : X Y) :

If F preserves pullbacks, then it preserves monomorphisms.

@[instance 100]
instance CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape {C : Type u₁} {D : Type u₂} [] [] (F : ) :
F.PreservesMonomorphisms
Equations
• =
theorem CategoryTheory.reflects_mono_of_reflectsLimit {C : Type u₁} {D : Type u₂} [] [] (F : ) {X : C} {Y : C} (f : X Y) [CategoryTheory.Mono (F.map f)] :

If F reflects pullbacks, then it reflects monomorphisms.

@[instance 100]
instance CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape {C : Type u₁} {D : Type u₂} [] [] (F : ) :
F.ReflectsMonomorphisms
Equations
• =
theorem CategoryTheory.preserves_epi_of_preservesColimit {C : Type u₁} {D : Type u₂} [] [] (F : ) {X : C} {Y : C} (f : X Y) :

If F preserves pushouts, then it preserves epimorphisms.

@[instance 100]
instance CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape {C : Type u₁} {D : Type u₂} [] [] (F : ) :
F.PreservesEpimorphisms
Equations
• =
theorem CategoryTheory.reflects_epi_of_reflectsColimit {C : Type u₁} {D : Type u₂} [] [] (F : ) {X : C} {Y : C} (f : X Y) [CategoryTheory.Epi (F.map f)] :

If F reflects pushouts, then it reflects epimorphisms.

@[instance 100]
instance CategoryTheory.reflectsEpimorphisms_of_reflectsColimitsOfShape {C : Type u₁} {D : Type u₂} [] [] (F : ) :
F.ReflectsEpimorphisms
Equations
• =