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] : Mono f ↔ ∀ (k : K), Mono (f.app k)

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 (Functor.whiskerRight f H)

instance CategoryTheory.instPreservesMonomorphismsFunctorObjWhiskeringRight {K : Type u} [Category.{v, u} K] {C : Type u'} [Category.{v', u'} C] {D : Type u''} [Category.{v'', u''} D] [Limits.HasPullbacks C] (F : Functor C D) [F.PreservesMonomorphisms] : ((Functor.whiskeringRight K C D).obj F).PreservesMonomorphisms

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] : Epi f ↔ ∀ (k : K), Epi (f.app k)

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 (Functor.whiskerRight f H)