Cokernel realization of the right Freyd category

An additive functor F : V ⥤ C into an abelian category sends an arrow of V to a morphism of C. Taking its cokernel kills right homotopies, hence descends to the right Freyd category. When F is fully faithful and its values are projective, this realization is fully faithful.

This is the cokernel/projective dual of the kernel/injective realization used elsewhere in the project. It packages the standard projective-presentation lifting argument needed for Auslander's coherent duality.

noncomputable def CategoryTheory.Preadditive.RightFreyd.rawCokernel {V : Type u} [Category.{v, u} V] {C : Type u'} [Category.{v', u'} C] [Abelian C] (F : Functor V C) : Functor (Arrow V) C

Before quotienting by right homotopy, send an arrow in V to the cokernel of its image under F.

noncomputable def CategoryTheory.Preadditive.RightFreyd.cokernelFunctor {V : Type u} [Category.{v, u} V] [Preadditive V] {C : Type u'} [Category.{v', u'} C] [Abelian C] (F : Functor V C) [F.Additive] : Functor (RightFreyd V) C

The cokernel realization of a right Freyd category along an additive functor.

theorem CategoryTheory.Preadditive.RightFreyd.cokernelFunctor_full_of_projective_objects {V : Type u} [Category.{v, u} V] [Preadditive V] {C : Type u'} [Category.{v', u'} C] [Abelian C] (F : Functor V C) [F.Additive] [F.Full] [F.Faithful] (hP : ∀ (X : V), Projective (F.obj X)) : (cokernelFunctor F).Full

Cokernel realization along a fully faithful functor with projective values is full.

theorem CategoryTheory.Preadditive.RightFreyd.cokernelFunctor_faithful_of_projective_objects {V : Type u} [Category.{v, u} V] [Preadditive V] {C : Type u'} [Category.{v', u'} C] [Abelian C] (F : Functor V C) [F.Additive] [F.Full] [F.Faithful] (hP : ∀ (X : V), Projective (F.obj X)) : (cokernelFunctor F).Faithful

Cokernel realization along a fully faithful functor with projective values is faithful.

theorem CategoryTheory.Preadditive.RightFreyd.cokernelFunctor_essSurj_of_epi_covers {V : Type u} [Category.{v, u} V] [Preadditive V] {C : Type u'} [Category.{v', u'} C] [Abelian C] (F : Functor V C) [F.Additive] [F.Full] (hcover : ∀ (Y : C), ∃ (X : V) (p : F.obj X ⟶ Y), Epi p) : (cokernelFunctor F).EssSurj

If every target object is an epimorphic image of an object in the image of F, then every target object is the cokernel realization of a right-Freyd presentation. Applying the same hypothesis to the kernel of a chosen cover produces the two-term presentation.