mathlib

5e188d2f - feat(category_theory/abelian): definition of projective object (#7108)

feat(category_theory/abelian): definition of projective object (#7108) This is extracted from @TwoFX's `projective` branch, with some slight tweaks (make things `Prop` valued classes), and documentation. This is just the definition of `projective` and `enough_projectives`, with no attempt to construct projective resolutions. I want this in place because constructing projective resolutions will hopefully be a good test of experiments with chain complexes. Co-authored-by: Markus Himmel <markus@himmel-villmar.de> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>