feat(Algebra): definition of cohen macaulay by Thmoas-Guan · Pull Request #26218 · leanprover-community/mathlib4

Thmoas-Guan · 2025-06-20T12:15:47Z

In this PR, we added the definition of CM module, CM local ring (extending local ring), and CM ring.
We also proved Theorem 30, Chater 6, Commutative Algebra, Matsumura.

depends on: [Merged by Bors] - feat(RingTheory/KrullDimension): Krull Dimension of quotient regular sequence #26219
depends on: feat(Algebra): Ischebeck theorem #26217
depends on: feat(Algebra): depth of QuotSMulTop #26216
depends on: [Merged by Bors] - feat(Data): some lemmas about WithBot ENat #28582

Thmoas-Guan · 2025-06-20T12:22:45Z

This PR is originally from #25230

mathlib4-dependent-issues-bot · 2025-06-20T12:44:22Z

This PR/issue depends on:

github-actions · 2025-06-20T12:48:54Z

PR summary 2ff88851d5

Import changes exceeding 2%

%	File
+25.29%	`Mathlib.RingTheory.Regular.Depth`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Regular.Depth	1815	2274	+459 (+25.29%)
Mathlib.RingTheory.Regular.Category	1480	1343	-137 (-9.26%)

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.Regular.Category`	-137
`Mathlib.RingTheory.Regular.Depth`	459
`Mathlib.RingTheory.Depth.Basic` (new file)	2273
`Mathlib.RingTheory.Depth.Ischebeck` (new file)	2312
`Mathlib.RingTheory.CohenMacaulay.Basic` (new file)	2417

Declarations diff

+ CategoryTheory.Abelian.Ext.pow_mono_of_mono
+ 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
+ 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.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
+ 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_of_ringEquiv
+ 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
+ localize_at_prime_depth_eq_of_isCohenMacaulay
+ localize_at_prime_isCohenMacaulay_of_isCohenMacaulay
+ 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
+ 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
+ ring_depth_invariant
+ ring_depth_uLift
+ smulShortComplex_f_eq_smul_id
+ smulShortComplex_f_hom_eq_smul_id

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

Current number	Change	Type
6428	13	backward.isDefEq.respectTransparency

Current commit 051317c652
Reference commit 2ff88851d5

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

leanprover-community-bot-assistant · 2025-07-05T04:54:29Z