feat(Algebra): Auslander–Buchsbaum theorem

[Thmoas-Guan]

This PR mainly proved the Auslander-Buchsbaum theorem stating for a noetherian local ring R and a finitely generated R module M , proj.dim(M) + depth(M) = depth(R).

Co-authored-by: Yongle Hu [email protected]

---

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

[Thmoas-Guan]

This PR is originally from #24923

[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.RingTheory.Regular.AuslanderBuchsbaum (new file)	2092

---

Declarations diff

+ AuslanderBuchsbaum + AuslanderBuchsbaum_one + 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.free_of_projective_of_isLocalRing + ModuleCat.projective_shortComplex + ModuleCat.projective_shortComplex_shortExact + Submodule.comap_lt_top_of_lt_range + Submodule.smul_top_eq_comap_smul_top_of_surjective + basis_lift + basis_lift_ker_le + coprodIsoDirectSum + coproductCocone + coproductCoconeIsColimit + exists_isRegular_of_exists_subsingleton_ext + exists_isRegular_tfae + extClass_postcomp_surjective_of_projective_X₂ + extClass_precomp_surjective_of_projective_X₂ + ext_hom_zero_of_mem_ideal_smul + ext_subsingleton_of_exists_isRegular + ext_subsingleton_of_lt_moduleDepth + finte_free_ext_vanish_iff + free_depth_eq_ring_depth + instance (I : Ideal R) (M : Type*) [AddCommGroup M] [Module R M] + 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 + mem_smul_top_of_range_le_smul_top + 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 + mono_postcomp_mk₀_of_mono + mono_precomp_mk₀_of_epi + nontrivial_ring_of_nontrivial_module + postcomp_mk₀_injective_of_mono + pow_mono_of_mono + precomp_mk₀_injective_of_epi + ring_depth_invariant + ring_depth_uLift + smul_id_postcomp_eq_zero_of_mem_ann + smul_prod_of_smul + subsingleton_of_injective + subsingleton_of_pi + 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-dependent-issues-bot]

This PR/issue depends on:

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

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