feat(Algebra): finite projective dimension of regular

[Thmoas-Guan]

In this PR, we proved every finitely generated module over regular local ring has finite projective dimension. With this and Auslander Buchsbaum theorem, we can obtain the global dimension of regular local ring is equal to its krull dimension.

---

• depends on: feat(Algebra): maximal Cohen Macaulay module #29533
• depends on: feat(Algebra): Auslander–Buchsbaum theorem #26215

[github-actions]

PR summary 4ec5d95aa6

Import changes exceeding 2%

%	File
+33.54%	Mathlib.RingTheory.Regular.Category
+25.26%	Mathlib.RingTheory.Regular.Depth

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Regular.Category	1479	1975	+496 (+33.54%)
Mathlib.RingTheory.Regular.Depth	1813	2271	+458 (+25.26%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Regular.Depth	458
Mathlib.RingTheory.Regular.Category	496
Mathlib.RingTheory.RegularLocalRing.Basic (new file)	2162
Mathlib.RingTheory.Regular.Ischebeck (new file)	2310
Mathlib.RingTheory.Regular.AuslanderBuchsbaum (new file)	2357
Mathlib.RingTheory.CohenMacaulay.Basic (new file)	2414
Mathlib.RingTheory.CohenMacaulay.Maximal (new file)	2425
Mathlib.RingTheory.RegularLocalRing.GlobalDimension (new file)	2431

---

Declarations diff

+ AuslanderBuchsbaum
+ AuslanderBuchsbaum_one
+ CategoryTheory.Abelian.Ext.pow_mono_of_mono
+ Ext.smulShortComplex_f_postcomp_eq_zero_of_mem_ann
+ Ext.smul_id_postcomp_eq_zero_of_mem_ann
+ Ideal.depth
+ Ideal.depth_eq_of_iso
+ Ideal.depth_quotSMulTop_succ_eq_moduleDepth
+ IsCohenMacaulayLocalRing
+ IsCohenMacaulayLocalRing.of_isLocalRing_of_isCohenMacaulayRing
+ IsCohenMacaulayRing
+ IsCohenMacaulayRing.of_isCohenMacaulayLocalRing
+ IsDiscreteValuationRing.of_isRegularLocalRing_of_ringKrullDim_eq_one
+ IsLocalRing.ResidueField.map_bijective_of_surjective
+ 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
+ LinearMapOfSemiLinearMapAlgebraMap
+ ModuleCat.IsCohenMacaulay
+ ModuleCat.IsCohenMacaulay_of_iso
+ ModuleCat.IsMaximalCohenMacaulay
+ ModuleCat.depth_eq_supportDim_of_cohenMacaulay
+ ModuleCat.depth_eq_supportDim_unbot_of_cohenMacaulay
+ ModuleCat.exists_isRegular_of_exists_subsingleton_ext
+ ModuleCat.exists_isRegular_tfae
+ ModuleCat.free_of_projective_of_isLocalRing
+ ModuleCat.isCohenMacaulay_iff
+ ModuleCat.subsingleton_ext_of_exists_isRegular
+ SemiLinearMapAlgebraMapOfLinearMap
+ Submodule.comap_lt_top_of_lt_range
+ associatedPrimes_self_eq_minimalPrimes
+ associated_prime_eq_minimalPrimes_isCohenMacaulay
+ associated_prime_minimal_of_isCohenMacaulay
+ basis_lift
+ basis_lift_ker_le
+ depth_eq_dim_quotient_associated_prime_of_isCohenMacaulay
+ depth_le_ringKrullDim
+ depth_le_ringKrullDim_associatedPrime
+ depth_le_supportDim
+ depth_ne_top
+ depth_quotient_regular_sequence_add_length_eq_depth
+ exist_nat_eq
+ ext_hom_zero_of_mem_ideal_smul
+ ext_subsingleton_of_lt_moduleDepth
+ finite_projectiveDimension_of_isRegularLocalRing
+ finite_projectiveDimension_of_isRegularLocalRing_aux
+ finte_free_ext_vanish_iff
+ free_depth_eq_ring_depth
+ free_of_isMaximalCohenMacaulay_of_isRegularLocalRing
+ free_of_quotSMulTop_free
+ ideal_depth_quotient_regular_sequence_add_length_eq_ideal_depth
+ instance (I : Ideal R) (M : Type*) [AddCommGroup M] [Module R M]
+ instance [IsCohenMacaulayLocalRing R] : (ModuleCat.of R R).IsCohenMacaulay
+ instance [IsNoetherianRing R] [IsLocalRing R] [Small.{v} R]
+ instance [IsRegularLocalRing R] : IsDomain R := isDomain_of_isRegularLocalRing R
+ isCohenMacaulayLocalRing_def
+ isCohenMacaulayLocalRing_iff
+ isCohenMacaulayLocalRing_localization_atPrime
+ isCohenMacaulayLocalRing_of_isRegularLocalRing
+ isCohenMacaulayLocalRing_of_ringEquiv
+ isCohenMacaulayLocalRing_of_ringKrullDim_le_depth
+ isCohenMacaulayRing_def
+ isCohenMacaulayRing_def'
+ isCohenMacaulayRing_iff
+ isCohenMacaulayRing_of_ringEquiv
+ isCohenMacaulay_of_isMaximalCohenMacaulay
+ isDomain_of_isRegularLocalRing
+ isField_of_isRegularLocalRing_of_dimension_zero
+ isLocalization_at_prime_prime_depth_le_depth
+ isLocalize_at_prime_depth_eq_of_isCohenMacaulay
+ isLocalize_at_prime_dim_eq_prime_depth_of_isCohenMacaulay
+ isLocalize_at_prime_isCohenMacaulay_of_isCohenMacaulay
+ isLocalizedModule_quotSMulTop_isLocalizedModule_map
+ isMaximalCohenMacaulay_def
+ isRegular_of_span_eq_maximalIdeal
+ localize_at_prime_depth_eq_of_isCohenMacaulay
+ localize_at_prime_isCohenMacaulay_of_isCohenMacaulay
+ 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_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
+ moduleDepth_quotSMulTop_succ_eq_moduleDepth
+ moduleDepth_quotient_regular_sequence_add_length_eq_moduleDepth
+ nontrivial_ring_of_nontrivial_module
+ quotSMulTop_isCohenMacaulay_iff_isCohenMacaulay
+ quotSMulTop_isLocalizedModule_map
+ quotient_isRegularLocalRing_tfae
+ quotient_prime_ringKrullDim_ne_bot
+ quotient_regular_isCohenMacaulay_iff_isCohenMacaulay
+ quotient_regular_sequence_isCohenMacaulay_iff_isCohenMacaulay
+ quotient_regular_smul_top_isCohenMacaulay_iff_isCohenMacaulay
+ quotient_span_regular_isCohenMacaulay_iff_isCohenMacaulay
+ quotient_span_singleton
+ ring_depth_invariant
+ ring_depth_uLift
+ smulShortComplex_f_eq_smul_id
+ smulShortComplex_f_hom_eq_smul_id
+ smul_prod_of_smul
+ subsingleton_of_pi
- LinearMap.exact_smul_id_smul_top_mkQ

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) = (24.00, 0.00)

Current number	Change	Type
6919	24	backward.isDefEq

Current commit fb0f83a20c
Reference commit 4ec5d95aa6

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(Algebra): maximal Cohen Macaulay module #29533
• feat(Algebra): Auslander–Buchsbaum theorem #26215
  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.

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

[mathlib-merge-conflicts]

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