feat(Algebra): depth of QuotSMulTop

[Thmoas-Guan]

In this PR, we proved for a local ring R and a finitely generated R module M N, IsSMulRegular M x and x ∈ Module.annihilator R N, then depth(N, M/xM) + 1 = depth(N, M), and its corollary for quotient regular seqence.

---

• depends on: feat(Algebra): definition of depth #26214

[Thmoas-Guan]

This PR is originally from #25109

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(Algebra): definition of depth #26214
  By Dependent Issues (🤖). Happy coding!

[github-actions]

PR summary 2ff88851d5

Import changes exceeding 2%

%	File
+25.29%	Mathlib.RingTheory.Regular.Depth

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Regular.Depth	1815	2274	+459 (+25.29%)
Mathlib.RingTheory.Regular.Category	1480	1343	-137 (-9.26%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Regular.Category	-137
Mathlib.RingTheory.Regular.Depth	459
Mathlib.RingTheory.Depth.Basic (new file)	2273

---

Declarations diff

+ CategoryTheory.Abelian.Ext.pow_mono_of_mono
+ Ext.smul_id_postcomp_eq_zero_of_mem_ann
+ Ideal.depth
+ Ideal.depth_eq_of_iso
+ Ideal.depth_quotSMulTop_succ_eq_moduleDepth
+ IsLocalRing.depth
+ IsLocalRing.depth_eq_of_algebraMap_surjective
+ IsLocalRing.depth_eq_of_iso
+ IsLocalRing.depth_eq_of_ringEquiv
+ IsLocalRing.depth_eq_sSup_length_regular
+ IsLocalRing.depth_quotSMulTop_succ_eq_moduleDepth
+ IsLocalRing.depth_quotient_regular_sequence_add_length_eq_depth
+ IsLocalRing.depth_quotient_regular_succ_eq_depth
+ IsLocalRing.depth_quotient_span_regular_succ_eq_depth
+ IsLocalRing.ideal_depth_eq_sSup_length_regular
+ IsLocalRing.ideal_depth_le_depth
+ LinearMap.exact_lsmul_smul_top_mkQ
+ ModuleCat.exists_isRegular_of_exists_subsingleton_ext
+ ModuleCat.exists_isRegular_tfae
+ ModuleCat.subsingleton_ext_of_exists_isRegular
+ Submodule.comap_lt_top_of_lt_range
+ depth_quotient_regular_sequence_add_length_eq_depth
+ ext_subsingleton_of_lt_moduleDepth
+ ideal_depth_quotient_regular_sequence_add_length_eq_ideal_depth
+ moduleDepth
+ moduleDepth_eq_depth_of_supp_eq
+ moduleDepth_eq_find
+ moduleDepth_eq_iff
+ moduleDepth_eq_moduleDepth_shrink
+ moduleDepth_eq_of_iso_fst
+ moduleDepth_eq_of_iso_snd
+ moduleDepth_eq_sSup_length_regular
+ moduleDepth_eq_sup_nat
+ moduleDepth_eq_top_iff
+ moduleDepth_eq_zero_of_hom_nontrivial
+ moduleDepth_ge_min_of_shortExact_fst_fst
+ moduleDepth_ge_min_of_shortExact_fst_snd
+ moduleDepth_ge_min_of_shortExact_snd_fst
+ moduleDepth_ge_min_of_shortExact_snd_snd
+ moduleDepth_ge_min_of_shortExact_trd_fst
+ moduleDepth_ge_min_of_shortExact_trd_snd
+ moduleDepth_lt_top_iff
+ moduleDepth_quotSMulTop_succ_eq_moduleDepth
+ moduleDepth_quotient_regular_sequence_add_length_eq_moduleDepth
+ ring_depth_invariant
+ ring_depth_uLift
+ smulShortComplex_f_eq_smul_id
+ smulShortComplex_f_hom_eq_smul_id

You can run this locally as follows

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

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

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

---

Increase in tech debt: (relative, absolute) = (8.00, 0.00)

Current number	Change	Type
6423	8	backward.isDefEq.respectTransparency

Current commit b0eac540f4
Reference commit 2ff88851d5

You can run this locally as

./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-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.