Commit 2025-07-15 16:05 ccca4728

feat(CategoryTheory/Preadditive/Injective/Basic, CategoryTheory/Preadditive/Projective/Basic): injectivity/projectivity criterion (#27156) Prove that, if F : C ⥤ D is a fully faithful functor that preserves monomorphisms (resp. epimorphisms), and if the image by F of a map f of C is injective (resp. projective), then so is f. This will be used when F is the inclusion of a full abelian subcategory to show that we only need to check injectivity/projectivity of a map in the big category.