Documentation

Mathlib.CategoryTheory.Preadditive.Yoneda.Injective

An object is injective iff the preadditive yoneda functor on it preserves epimorphisms.