Relating monomorphisms and epimorphisms to limits and colimits #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
If F preserves (resp. reflects) pullbacks, then it preserves (resp. reflects) monomorphisms.
We also provide the dual version for epimorphisms.
theorem
category_theory.preserves_mono_of_preserves_limit
{C : Type u₁}
{D : Type u₂}
[category_theory.category C]
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.preserves_limit (category_theory.limits.cospan f f) F]
[category_theory.mono f] :
category_theory.mono (F.map f)
If F preserves pullbacks, then it preserves monomorphisms.
@[protected, instance]
theorem
category_theory.reflects_mono_of_reflects_limit
{C : Type u₁}
{D : Type u₂}
[category_theory.category C]
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.reflects_limit (category_theory.limits.cospan f f) F]
[category_theory.mono (F.map f)] :
If F reflects pullbacks, then it reflects monomorphisms.
@[protected, instance]
theorem
category_theory.preserves_epi_of_preserves_colimit
{C : Type u₁}
{D : Type u₂}
[category_theory.category C]
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.preserves_colimit (category_theory.limits.span f f) F]
[category_theory.epi f] :
category_theory.epi (F.map f)
If F preserves pushouts, then it preserves epimorphisms.
@[protected, instance]
theorem
category_theory.reflects_epi_of_reflects_colimit
{C : Type u₁}
{D : Type u₂}
[category_theory.category C]
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.reflects_colimit (category_theory.limits.span f f) F]
[category_theory.epi (F.map f)] :
If F reflects pushouts, then it reflects epimorphisms.
@[protected, instance]