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

If F preserves pullbacks, then it preserves monomorphisms.

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

Equations

• (_ : CategoryTheory.Functor.PreservesMonomorphisms F) = (_ : CategoryTheory.Functor.PreservesMonomorphisms F)

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

If F reflects pullbacks, then it reflects monomorphisms.

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

Equations

• (_ : CategoryTheory.Functor.ReflectsMonomorphisms F) = (_ : CategoryTheory.Functor.ReflectsMonomorphisms F)

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

If F preserves pushouts, then it preserves epimorphisms.

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

Equations

• (_ : CategoryTheory.Functor.PreservesEpimorphisms F) = (_ : CategoryTheory.Functor.PreservesEpimorphisms F)

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

If F reflects pushouts, then it reflects epimorphisms.

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

Equations

• (_ : CategoryTheory.Functor.ReflectsEpimorphisms F) = (_ : CategoryTheory.Functor.ReflectsEpimorphisms F)