feat(Algebra/RingTheory): global dimension of regular ring

[Thmoas-Guan]

In this PR, we proved that the global (homological dimension) of regular ring is equal to its krull dimension.

---

• depends on: feat(RingTheory): definition of regular ring #28684
• depends on: feat(RingTheory): global dimension equals the supremum over localizations #31999
• depends on: feat(Algebra): global dimension of regular local ring #29534

[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.Algebra.Category.ModuleCat.Baer (new file)	1917
Mathlib.RingTheory.GlobalDimension (new file)	2081
Mathlib.RingTheory.RegularLocalRing.RegularRing.Basic (new file)	2159
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)	2445
Mathlib.RingTheory.RegularLocalRing.RegularRing.GlobalDimension (new file)	2447

---

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
+ IsRegularLocalRing.globalDimension_eq_ringKrullDim
+ IsRegularRing
+ IsRegularRing.globalDimension_eq_ringKrullDim
+ LinearEquiv.conj_symm_exact_iff_exact
+ 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
+ _root_.LinearEquiv.comp_snd_exact_iff_exact
+ _root_.LinearEquiv.fst_comp_exact_iff_exact
+ 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_quotient_one_subsingleton_iff
+ ext_subsingleton_of_lt_moduleDepth
+ ext_subsingleton_of_quotients
+ ext_subsingleton_of_quotients'
+ finite_projectiveDimension_of_isRegularLocalRing_aux
+ finte_free_ext_vanish_iff
+ free_depth_eq_ring_depth
+ free_of_isMaximalCohenMacaulay_of_isRegularLocalRing
+ free_of_quotSMulTop_free
+ globalDimension
+ globalDimension_eq_bot_iff
+ globalDimension_eq_iSup_loclization_maximal
+ globalDimension_eq_iSup_loclization_prime
+ globalDimension_eq_of_ringEquiv
+ globalDimension_eq_of_small
+ globalDimension_eq_sup_injectiveDimension
+ globalDimension_eq_sup_projectiveDimension_finite
+ globalDimension_le_iff
+ globalDimension_le_tfae
+ globalDimension_localization_le
+ ideal_depth_quotient_regular_sequence_add_length_eq_ideal_depth
+ injective_of_subsingleton_ext_quotient_one
+ instance (I : Ideal R) (M : Type*) [AddCommGroup M] [Module R M]
+ instance [IsCohenMacaulayLocalRing R] : (ModuleCat.of R R).IsCohenMacaulay
+ instance [IsDomain R] [IsDedekindDomain R] : IsRegularRing R := by
+ 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
+ isRegularRing_iff
+ isRegularRing_of_ringEquiv
+ 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
+ projectiveDimension_ne_top_of_isRegularLocalRing
+ 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) = (26.00, 0.00)

Current number	Change	Type
6921	26	backward.isDefEq

Current commit 90ac741d80
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(RingTheory): definition of regular ring #28684
• feat(RingTheory): global dimension equals the supremum over localizations #31999
• feat(Algebra): global dimension of regular local ring #29534
  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.