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₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (f : X ⟶ Y) [Limits.PreservesLimit (Limits.cospan f f) F] [Mono f] : Mono (F.map f)

If F preserves pullbacks, then it preserves monomorphisms.

@[instance 100]

instance CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesLimitsOfShape Limits.WalkingCospan F] : F.PreservesMonomorphisms

theorem CategoryTheory.reflects_mono_of_reflectsLimit {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (f : X ⟶ Y) [Limits.ReflectsLimit (Limits.cospan f f) F] [Mono (F.map f)] : Mono f

If F reflects pullbacks, then it reflects monomorphisms.

@[instance 100]

instance CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [Limits.ReflectsLimitsOfShape Limits.WalkingCospan F] : F.ReflectsMonomorphisms

theorem CategoryTheory.preserves_epi_of_preservesColimit {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (f : X ⟶ Y) [Limits.PreservesColimit (Limits.span f f) F] [Epi f] : Epi (F.map f)

If F preserves pushouts, then it preserves epimorphisms.

@[instance 100]

instance CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesColimitsOfShape Limits.WalkingSpan F] : F.PreservesEpimorphisms

theorem CategoryTheory.reflects_epi_of_reflectsColimit {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (f : X ⟶ Y) [Limits.ReflectsColimit (Limits.span f f) F] [Epi (F.map f)] : Epi f

If F reflects pushouts, then it reflects epimorphisms.

@[instance 100]

instance CategoryTheory.reflectsEpimorphisms_of_reflectsColimitsOfShape {C : Type u₁} {D : Type u₂} [Category.{v₁, u₁} C] [Category.{v₂, u₂} D] (F : Functor C D) [Limits.ReflectsColimitsOfShape Limits.WalkingSpan F] : F.ReflectsEpimorphisms