feat(CategoryTheory/ObjectProperty): define objects admitting finite resolutions by objects satisfying P : ObjectProperty C

[mbkybky]

Let C be a category, P : ObjectProperty C be a property of objectsin C. We say that X : C has a P-resolution of length n if there exists an exact sequence 0 ⟶ Eₙ ⟶ ⋯ ⟶ E₀ ⟶ X ⟶ 0 such that each Eᵢ : C satisfies P.

---

[github-actions]

PR summary 0673ab95b0

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

---

Declarations diff (regex)

+ HasFiniteResolution
+ HasFiniteResolutionOfLength
+ hasFiniteResolution
+ 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 0673ab9).

• +31 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.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 0673ab95b0
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).

[joelriou]

I think we should say that in the implementation it is defined using an inductive predicate.