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 : CategoryTheory.Functor K C}
{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 : CategoryTheory.Functor K C}
{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 : CategoryTheory.Functor K C}
{G : CategoryTheory.Functor K C}
(f : F ⟶ G)
[CategoryTheory.Limits.HasPullbacks C]
[CategoryTheory.Mono f]
(H : CategoryTheory.Functor C D)
[H.PreservesMonomorphisms]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.instEpiAppOfFunctor
{K : Type u}
[CategoryTheory.Category.{v, u} K]
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{F : CategoryTheory.Functor K C}
{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 : CategoryTheory.Functor K C}
{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 : CategoryTheory.Functor K C}
{G : CategoryTheory.Functor K C}
(f : F ⟶ G)
[CategoryTheory.Limits.HasPushouts C]
[CategoryTheory.Epi f]
(H : CategoryTheory.Functor C D)
[H.PreservesEpimorphisms]
:
Equations
- ⋯ = ⋯