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.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]
:
Equations
- ⋯ = ⋯
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.map 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]
:
Equations
- ⋯ = ⋯
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.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]
:
Equations
- ⋯ = ⋯
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.map 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]
:
Equations
- ⋯ = ⋯