feat(CategoryTheory/ObjectProperty/HasFiniteResolution): relation with projective dimension

[mbkybky]

X has a projective resolution of length n if and only if X has projective dimension ≤ n.

• depends on: feat(CategoryTheory/ObjectProperty): define objects admitting finite resolutions by objects satisfying P : ObjectProperty C #41880

---

[github-actions]

PR summary 5913fd18c0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.ObjectProperty.HasFiniteResolution.Basic (new file)	802
Mathlib.CategoryTheory.ObjectProperty.HasFiniteResolution.Projective (new file)	1607

---

Declarations diff (regex)

+ HasFiniteResolution
+ HasFiniteResolutionOfLength
+ hasFiniteResolution
+ hasProjectiveDimensionLE
+ iff_hasProjectiveDimensionLE
+ instance [P.Is X] : P.HasFiniteResolution X
+ of_property
+ of_shortExact
+ property
++ map_exactFunctor
++ monotone
++ of_iso
++ property_of_isClosedUnderQuotients

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 5913fd1).

• +33 new declarations
• −0 removed declarations

+CategoryTheory.ObjectProperty.HasFiniteResolution
+CategoryTheory.ObjectProperty.HasFiniteResolution.casesOn
+CategoryTheory.ObjectProperty.HasFiniteResolution.instOfIs
+CategoryTheory.ObjectProperty.HasFiniteResolution.map_exactFunctor
+CategoryTheory.ObjectProperty.HasFiniteResolution.mk
+CategoryTheory.ObjectProperty.HasFiniteResolution.monotone
+CategoryTheory.ObjectProperty.HasFiniteResolution.of_iso
+CategoryTheory.ObjectProperty.HasFiniteResolution.of_property
+CategoryTheory.ObjectProperty.HasFiniteResolution.of_shortExact
+CategoryTheory.ObjectProperty.HasFiniteResolution.out
+CategoryTheory.ObjectProperty.HasFiniteResolution.property_of_isClosedUnderQuotients
+CategoryTheory.ObjectProperty.HasFiniteResolution.rec
+CategoryTheory.ObjectProperty.HasFiniteResolution.recOn
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.below
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.below.casesOn
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.below.rec
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.below.succ
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.below.zero
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.brecOn
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.casesOn
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.hasFiniteResolution
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.hasProjectiveDimensionLE
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.iff_hasProjectiveDimensionLE
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.map_exactFunctor
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.monotone
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.of_iso
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.property
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.property_of_isClosedUnderQuotients
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.rec
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.recOn
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.succ
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.zero

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 5913fd18c0
Reference commit abb22825db

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(CategoryTheory/ObjectProperty): define objects admitting finite resolutions by objects satisfying P : ObjectProperty C #41880
  By Dependent Issues (🤖). Happy coding!