C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
J : C
hP : PreservesFiniteColimits (preadditiveYonedaObj J)
⊢ Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
J : C
hP : PreservesFiniteColimits (preadditiveYonedaObj J)
⊢ Injective J
rw [injective_iff_preservesEpimorphisms_preadditive_yoneda_obj']
no goals
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
J : C
hP : PreservesFiniteColimits (preadditiveYonedaObj J)
⊢ Functor.PreservesEpimorphisms (preadditiveYonedaObj J)
infer_instance