Monomorphisms and epimorphisms in functor categories #
A natural transformation f : F ⟶ G between functors K ⥤ C
is a mono (resp. epi) iff for all k : K, f.app k is,
at least when C has pullbacks (resp. pushouts),
see NatTrans.mono_iff_mono_app and NatTrans.epi_iff_epi_app.
instance
CategoryTheory.instMonoAppOfFunctor
{K : Type u}
[Category.{v, u} K]
{C : Type u'}
[Category.{v', u'} C]
{F G : Functor K C}
(f : F ⟶ G)
[Limits.HasPullbacks C]
[Mono f]
(k : K)
:
Mono (f.app k)
theorem
CategoryTheory.NatTrans.mono_iff_mono_app
{K : Type u}
[Category.{v, u} K]
{C : Type u'}
[Category.{v', u'} C]
{F G : Functor K C}
(f : F ⟶ G)
[Limits.HasPullbacks C]
:
instance
CategoryTheory.instMonoFunctorWhiskerRightOfPreservesMonomorphisms
{K : Type u}
[Category.{v, u} K]
{C : Type u'}
[Category.{v', u'} C]
{D : Type u''}
[Category.{v'', u''} D]
{F G : Functor K C}
(f : F ⟶ G)
[Limits.HasPullbacks C]
[Mono f]
(H : Functor C D)
[H.PreservesMonomorphisms]
:
Mono (whiskerRight f H)
instance
CategoryTheory.instEpiAppOfFunctor
{K : Type u}
[Category.{v, u} K]
{C : Type u'}
[Category.{v', u'} C]
{F G : Functor K C}
(f : F ⟶ G)
[Limits.HasPushouts C]
[Epi f]
(k : K)
:
Epi (f.app k)
theorem
CategoryTheory.NatTrans.epi_iff_epi_app
{K : Type u}
[Category.{v, u} K]
{C : Type u'}
[Category.{v', u'} C]
{F G : Functor K C}
(f : F ⟶ G)
[Limits.HasPushouts C]
:
instance
CategoryTheory.instEpiFunctorWhiskerRightOfPreservesEpimorphisms
{K : Type u}
[Category.{v, u} K]
{C : Type u'}
[Category.{v', u'} C]
{D : Type u''}
[Category.{v'', u''} D]
{F G : Functor K C}
(f : F ⟶ G)
[Limits.HasPushouts C]
[Epi f]
(H : Functor C D)
[H.PreservesEpimorphisms]
:
Epi (whiskerRight f H)