feat(CategoryTheory): Noetherian objects

[joelriou]

An object X in a category C is Noetherian if the ordered type Subobject X satisfies the ascending chain condition. In this PR, we show that this property is closed under subobjects. (In a future PR, it shall be shown that if C is an abelian category, then this is a Serre class.)

---

[github-actions]

PR summary 0a0692b62d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Subobject.NoetherianObject (new file)	928

---

Declarations diff

+ Is
+ IsNoetherianObject
+ PartialOrder.isIso_iff_eq
+ hom_self_eq_id
+ instance : (isNoetherianObject (C := C)).IsClosedUnderSubobjects
+ instance : (representative (X := X)).IsEquivalence
+ instance [HasZeroObject C] : (isNoetherianObject (C := C)).ContainsZero
+ instance [IsNoetherianObject X] : WellFoundedGT (Subobject X)
+ instance {A B : MonoOver X} (f : A ⟶ B) [IsIso f] : IsIso f.left
+ isEventuallyConstant_of_isNoetherianObject
+ isIso_iff_isIso_left
+ isIso_iff_subobjectMk_eq
+ isIso_left_iff_subobjectMk_eq
+ isNoetherianObject
+ isNoetherianObject_iff_isEventuallyConstant
+ isNoetherianObject_iff_monotone_chain_condition
+ isNoetherianObject_iff_not_strictMono
+ isNoetherianObject_of_isZero
+ isNoetherianObject_of_mono
+ is_of_prop
+ mk_surjective
+ monotone_chain_condition_of_isNoetherianObject
+ not_strictMono_of_isNoetherianObject
+ prop_of_is
+ subobjectMk_le_mk_of_hom
+ subsingleton_of_isZero
- MonoOver.subobjectMk_le_mk_of_hom

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).

[callesonne]

A few comments, will look over the main file NotherianObject later today or tomorrow.

[callesonne]

Nice!