[Merged by Bors] - feat(CategoryTheory): characterization of injective objects in terms of lifting properties

[joelriou]

This PR adds the lemma injective_iff_rlp_monomorphisms_zero which shows that I is an injective object iff 0 : I ⟶ 0 has the right lifting property with respect to the class of monomorphisms. We also move the files regarding injectives objects to a subdirectory. (Dual results for projective objects are also added.)

---

[github-actions]

PR summary 140a0d7782

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Abelian.ProjectiveDimension	-1375
Mathlib.CategoryTheory.Abelian.Injective Mathlib.CategoryTheory.Abelian.Projective	-1195
Mathlib.CategoryTheory.Abelian.ProjectiveResolution	-1026
Mathlib.CategoryTheory.Abelian.InjectiveResolution	-1023
Mathlib.CategoryTheory.Preadditive.InjectiveResolution Mathlib.CategoryTheory.Preadditive.ProjectiveResolution	-1017
Mathlib.CategoryTheory.Preadditive.Injective	-601
Mathlib.CategoryTheory.Preadditive.Projective	-600
Mathlib.CategoryTheory.Preadditive.Projective.Basic	600
Mathlib.CategoryTheory.Preadditive.Injective.Basic	601
Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties (new file)	635
Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties (new file)	636
Mathlib.CategoryTheory.Preadditive.Injective.Resolution Mathlib.CategoryTheory.Preadditive.Projective.Resolution	1017
Mathlib.CategoryTheory.Abelian.Injective.Resolution	1023
Mathlib.CategoryTheory.Abelian.Projective.Resolution	1026
Mathlib.CategoryTheory.Abelian.Injective.Basic Mathlib.CategoryTheory.Abelian.Projective.Basic	1195
Mathlib.CategoryTheory.Abelian.Projective.Dimension	1375

---

Declarations diff

+ injective_iff_rlp_monomorphisms_of_isZero
+ injective_iff_rlp_monomorphisms_zero
+ instance {A B I : C} (i : A ⟶ B) [Mono i] [Injective I] [HasZeroObject C] (p : I ⟶ 0) :
+ instance {X Y P : C} (p : X ⟶ Y) [Epi p] [Projective P] [HasZeroObject C] (i : 0 ⟶ P) :
+ projective_iff_llp_epimorphisms_of_isZero
+ projective_iff_llp_epimorphisms_zero
++ hasLiftingProperty_of_isZero

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[TwoFX]

Presumably there is a dual result for projective objects? Could you add that as well?

[TwoFX]

Thanks!
bors r+

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed (retrying...):

• Build

[TwoFX]

bors r-

[mathlib-bors]

Canceled.

[TwoFX]

✖ [714/6192] Running Mathlib.CategoryTheory.Abelian.Projective
error: no such file or directory (error code: 2)
  file: ././././Mathlib/CategoryTheory/Abelian/Projective.lean
✖ [715/6192] Running Mathlib.CategoryTheory.Abelian.Yoneda
error: ././././Mathlib/CategoryTheory/Abelian/Yoneda.lean: bad import 'Mathlib.CategoryTheory.Abelian.Projective'
✖ [793/6192] Running Mathlib
error: ././././Mathlib.lean: bad import 'Mathlib.CategoryTheory.Abelian.Yoneda'

bors d+

[mathlib-bors]

✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[joelriou]

Thanks! I hope it will work this time...

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style