feat(Algebra): unmixed thm of Cohen-Macaulay ring

[Thmoas-Guan]

In this PR we proved for a (comm)ring R, R is Cohen-Macaulay ring iff the unmixed theorem holds (for every ideal I of height r generated by r elements, all associated primes of R/I have height r )

---

• depends on: feat(Algebra): cohen macaulay local ring is catenary #26245

[github-actions]

PR summary 52b9aaf523

Import changes exceeding 2%

%	File
+33.04%	Mathlib.RingTheory.Regular.Category
+24.94%	Mathlib.RingTheory.Regular.Depth

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Regular.Category	1468	1953	+485 (+33.04%)
Mathlib.RingTheory.Regular.Depth	1796	2244	+448 (+24.94%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Regular.Depth	448
Mathlib.RingTheory.Regular.Category	485
Mathlib.RingTheory.Regular.Ischebeck (new file)	2285
Mathlib.RingTheory.CohenMacaulay.Basic (new file)	2389
Mathlib.RingTheory.CohenMacaulay.Catenary (new file)	2390
Mathlib.RingTheory.CohenMacaulay.Unmixed (new file)	2391

---

Declarations diff

+ CategoryTheory.Abelian.Ext.pow_mono_of_mono
+ CategoryTheory.Abelian.Ext.smul_id_postcomp_eq_zero_of_mem_ann
+ Ideal.IsUnmixed
+ Ideal.depth
+ Ideal.depth_eq_height
+ Ideal.depth_eq_of_iso
+ Ideal.depth_le_height
+ Ideal.depth_quotSMulTop_succ_eq_moduleDepth
+ Ideal.exist_regular_sequence_length_eq_height
+ Ideal.height_add_ringKrullDim_quotient_eq_ringKrullDim
+ Ideal.ofList_height_eq_length_of_isWeaklyRegular
+ Ideal.ofList_height_eq_length_of_isWeaklyRegular'
+ Ideal.ofList_height_le_length
+ Ideal.ofList_isUnmixed_of_associatedPrimes_eq_minimalPrimes
+ Ideal.ofList_spanFinrank_le_length
+ Ideal.primeHeight_add_ringKrullDim_quotient_eq_ringKrullDim
+ Ideal.primeHeight_eq_ringKrullDim_localization
+ IsCohenMacaulayLocalRing
+ IsCohenMacaulayLocalRing.of_isLocalRing_of_isCohenMacaulayRing
+ IsCohenMacaulayRing
+ IsCohenMacaulayRing.of_isCohenMacaulayLocalRing
+ IsLocalRing.Ideal.ofList_height_le_length'
+ 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.height_eq_height_maximalIdeal_of_maximalIdeal_mem_minimalPrimes
+ IsLocalRing.ideal_depth_eq_sSup_length_regular
+ IsLocalRing.ideal_depth_le_depth
+ IsLocalization.height_le_height_map
+ LinearMapOfSemiLinearMapAlgebraMap
+ ModuleCat.IsCohenMacaulay
+ ModuleCat.IsCohenMacaulay_of_iso
+ 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.isCohenMacaulay_iff
+ ModuleCat.subsingleton_ext_of_exists_isRegular
+ SemiLinearMapAlgebraMapOfLinearMap
+ Submodule.comap_lt_top_of_lt_range
+ WithBot.add_le_add_natCast_left_iff
+ WithBot.add_le_add_natCast_right_iff
+ WithBot.add_le_add_one_left_iff
+ WithBot.add_le_add_one_right_iff
+ WithBot.add_natCast_cancel
+ WithBot.add_one_cancel
+ WithBot.natCast_add_cancel
+ WithBot.one_add_cancel
+ _root_.AddLECancellable.withBot
+ _root_.AddLECancellable.withTop
+ _root_.IsAddLeftRegular.withBot
+ _root_.IsAddLeftRegular.withTop
+ _root_.IsAddRightRegular.withBot
+ _root_.IsAddRightRegular.withTop
+ associatedPrimes_eq_minimalPrimes_of_isUnmixed
+ associatedPrimes_self_eq_minimalPrimes
+ associated_prime_eq_minimalPrimes_isCohenMacaulay
+ associated_prime_minimal_of_isCohenMacaulay
+ 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
+ ext_subsingleton_of_lt_moduleDepth
+ ideal_depth_quotient_regular_sequence_add_length_eq_ideal_depth
+ instance [IsCohenMacaulayLocalRing R] : (ModuleCat.of R R).IsCohenMacaulay
+ isCohenMacaulayLocalRing_def
+ isCohenMacaulayLocalRing_iff
+ isCohenMacaulayLocalRing_localization_atPrime
+ isCohenMacaulayLocalRing_of_ringEquiv
+ isCohenMacaulayLocalRing_of_ringKrullDim_le_depth
+ isCohenMacaulayRing_def
+ isCohenMacaulayRing_def'
+ isCohenMacaulayRing_iff
+ isCohenMacaulayRing_iff_unmixed
+ isCohenMacaulayRing_of_ringEquiv
+ isCohenMacaulayRing_of_unmixed
+ 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
+ isRegular_of_maximalIdeal_mem_ofList_minimalPrimes
+ isRegular_of_ofList_height_eq_length_of_isCohenMacaulayLocalRing
+ localize_at_prime_depth_eq_of_isCohenMacaulay
+ localize_at_prime_isCohenMacaulay_of_isCohenMacaulay
+ maximalIdeal_mem_minimalPrimes_of_surjective
+ maximalIdeal_mem_ofList_append_minimalPrimes_of_ofList_height_eq_length
+ 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
+ quotSMulTop_isCohenMacaulay_iff_isCohenMacaulay
+ quotSMulTop_isLocalizedModule_map
+ quotSMulTop_nontrivial
+ quotient_prime_ringKrullDim_ne_bot
+ quotient_regular_isCohenMacaulay_iff_isCohenMacaulay
+ quotient_regular_sequence_isCohenMacaulay_iff_isCohenMacaulay
+ quotient_regular_smul_top_isCohenMacaulay_iff_isCohenMacaulay
+ quotient_smul_top_lt_of_le_smul_top
+ quotient_span_regular_isCohenMacaulay_iff_isCohenMacaulay
+ ringKrullDim_quotient_eq_iSup_quotient_minimalPrimes
+ ring_depth_invariant
+ ring_depth_uLift
+ smul_top_eq_comap_smul_top_of_surjective

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 scripts/declarations_diff.sh contains some details about this script.

---

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

Current number	Change	Type
13089	10	backward.isDefEq

Current commit bd0c50d03f
Reference commit 52b9aaf523

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:

• feat(Algebra): cohen macaulay local ring is catenary #26245
  By Dependent Issues (🤖). Happy coding!

[leanprover-community-bot-assistant]

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.

[mathlib4-merge-conflict-bot]

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