C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj P.op)
⊢ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj P.op)
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj P.op)
⊢ Projective P
rw [projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj']
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj P.op)
⊢ Functor.PreservesEpimorphisms (preadditiveCoyonedaObj P.op ⋙ forget₂ (ModuleCat (End P.op)) AddCommGroupCat)
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj P.op)
⊢ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj P.op)
dsimp only [preadditiveCoyoneda]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj P.op)
⊢ Functor.PreservesEpimorphisms (preadditiveCoyonedaObj P.op ⋙ forget₂ (ModuleCat (End P.op)) AddCommGroupCat)
infer_instance