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} [CategoryTheory.Category.{v, u} K] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F G : CategoryTheory.Functor K C} (f : F ⟶ G) [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Mono f] (k : K) : CategoryTheory.Mono (f.app k)

Equations

• ⋯ = ⋯

theorem CategoryTheory.NatTrans.mono_iff_mono_app {K : Type u} [CategoryTheory.Category.{v, u} K] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F G : CategoryTheory.Functor K C} (f : F ⟶ G) [CategoryTheory.Limits.HasPullbacks C] : CategoryTheory.Mono f ↔ ∀ (k : K), CategoryTheory.Mono (f.app k)

instance CategoryTheory.instMonoFunctorWhiskerRightOfPreservesMonomorphisms {K : Type u} [CategoryTheory.Category.{v, u} K] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {D : Type u''} [CategoryTheory.Category.{v'', u''} D] {F G : CategoryTheory.Functor K C} (f : F ⟶ G) [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Mono f] (H : CategoryTheory.Functor C D) [H.PreservesMonomorphisms] : CategoryTheory.Mono (CategoryTheory.whiskerRight f H)

Equations

• ⋯ = ⋯

instance CategoryTheory.instEpiAppOfFunctor {K : Type u} [CategoryTheory.Category.{v, u} K] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F G : CategoryTheory.Functor K C} (f : F ⟶ G) [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Epi f] (k : K) : CategoryTheory.Epi (f.app k)

Equations

• ⋯ = ⋯

theorem CategoryTheory.NatTrans.epi_iff_epi_app {K : Type u} [CategoryTheory.Category.{v, u} K] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {F G : CategoryTheory.Functor K C} (f : F ⟶ G) [CategoryTheory.Limits.HasPushouts C] : CategoryTheory.Epi f ↔ ∀ (k : K), CategoryTheory.Epi (f.app k)

instance CategoryTheory.instEpiFunctorWhiskerRightOfPreservesEpimorphisms {K : Type u} [CategoryTheory.Category.{v, u} K] {C : Type u'} [CategoryTheory.Category.{v', u'} C] {D : Type u''} [CategoryTheory.Category.{v'', u''} D] {F G : CategoryTheory.Functor K C} (f : F ⟶ G) [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Epi f] (H : CategoryTheory.Functor C D) [H.PreservesEpimorphisms] : CategoryTheory.Epi (CategoryTheory.whiskerRight f H)

Equations

• ⋯ = ⋯