feat(Algebra): Ischebeck theorem

[Thmoas-Guan]

This PR mainly proved the Ischbecke theorem, stating that depth(N,M) is greater or equal to depth(M) - dim(N) for finitely generated module N, M over local ring.

---

• [ ] depends on: #26214
• [ ] depends on: #32081

[Thmoas-Guan]

This PR is originally from #24922

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• leanprover-community/mathlib4#26214
• leanprover-community/mathlib4#32081 By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

PR summary 86622378a5

Import changes exceeding 2%

%	File
+42.10%	Mathlib.RingTheory.Regular.Category
+26.83%	Mathlib.RingTheory.Regular.Depth

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Regular.Category	1209	1718	+509 (+42.10%)
Mathlib.RingTheory.Regular.Depth	1569	1990	+421 (+26.83%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Regular.Depth	421
Mathlib.RingTheory.Regular.Category	509
Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting (new file)	1717
Mathlib.Algebra.Category.ModuleCat.Ext.Finite (new file)	1718
Mathlib.RingTheory.Regular.Ischebeck (new file)	2115

---

Declarations diff

+ CategoryTheory.InjectivePresentation.shortComplex + CategoryTheory.InjectivePresentation.shortComplex_shortExact + Ideal.depth + Ideal.depth_eq_of_iso + Ideal.quotient_smul_top_lt_of_le_smul_top + IsLocalRing.depth + IsLocalRing.depth_eq_of_iso + IsLocalRing.depth_eq_sSup_length_regular + IsLocalRing.ideal_depth_eq_sSup_length_regular + IsLocalRing.ideal_depth_le_depth + LinearMap.shortComplexKer + LinearMap.shortExact_shortComplexKer + Module.exists_finite_presentation + Module.finite_shrink + Module.free_shrink + ModuleCat.finite_ext + ModuleCat.projective_shortComplex + ModuleCat.projective_shortComplex_shortExact + Submodule.comap_lt_top_of_lt_range + Submodule.smul_top_eq_comap_smul_top_of_surjective + depth_le_ringKrullDim + depth_le_ringKrullDim_associatedPrime + depth_le_supportDim + depth_ne_top + exists_isRegular_of_exists_subsingleton_ext + exists_isRegular_tfae + extClass_postcomp_surjective_of_projective_X₂ + extClass_precomp_surjective_of_projective_X₂ + ext_subsingleton_of_exists_isRegular + ext_subsingleton_of_lt_moduleDepth + instance [Small.{v} R] (M : ModuleCat.{v} R) : Module.Free R M.projective_shortComplex.X₂ + instance {M : ModuleCat.{v} R} (ip : InjectivePresentation M) : Injective ip.shortComplex.X₂ := ip.2 + 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_depth_sub_dim + 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 + mono_postcomp_mk₀_of_mono + mono_precomp_mk₀_of_epi + postcomp_mk₀_injective_of_mono + pow_mono_of_mono + precomp_mk₀_injective_of_epi + quotSMulTop_nontrivial + quotient_prime_ringKrullDim_ne_bot + ring_depth_invariant + ring_depth_uLift + smul_id_postcomp_eq_zero_of_mem_ann + subsingleton_of_injective + subsingleton_of_projective

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

[mathlib4-merge-conflict-bot]

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

[mathlib4-merge-conflict-bot]

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

[mathlib4-merge-conflict-bot]

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

[mathlib4-merge-conflict-bot]

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