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] :
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] :
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] :
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] :
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] :
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] :