feat(Algebra): maximal Cohen Macaulay module#29533
Conversation
github-actions
Bot
added
the
large-import
PR summary b4d49cfc19
|
| Files | Import difference |
|---|---|
Mathlib.RingTheory.RegularLocalRing.Basic (new file) |
2193 |
Mathlib.RingTheory.Depth.Rees (new file) |
2298 |
Mathlib.RingTheory.Depth.Basic (new file) |
2300 |
Mathlib.RingTheory.Depth.Ischebeck (new file) |
2338 |
Mathlib.RingTheory.CohenMacaulay.Basic (new file) |
2443 |
Mathlib.RingTheory.CohenMacaulay.Maximal (new file) |
2457 |
Declarations diff (regex)
+ FiniteRingKrullDim.ringKrullDim_eq_nat
+ Ideal.depth
+ Ideal.depth_eq_of_iso
+ Ideal.depth_eq_of_linearEquiv
+ Ideal.depth_eq_top_of_subsingleton
+ Ideal.depth_quotSMulTop_succ_eq_moduleDepth
+ Ideal.span_singleton_mul_eq_self_of_isPrime
+ IsCohenMacaulayLocalRing
+ IsCohenMacaulayLocalRing.of_isLocalRing_of_isCohenMacaulayRing
+ IsCohenMacaulayRing
+ IsCohenMacaulayRing.of_isCohenMacaulayLocalRing
+ IsDiscreteValuationRing.of_isRegularLocalRing_of_ringKrullDim_eq_one
+ IsLocalRing.depth
+ IsLocalRing.depth_eq_of_algebraMap_surjective
+ IsLocalRing.depth_eq_of_iso
+ IsLocalRing.depth_eq_of_linearEquiv
+ IsLocalRing.depth_eq_of_ringEquiv
+ IsLocalRing.depth_eq_sSup_length_regular
+ IsLocalRing.depth_eq_top_of_subsingleton
+ 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
+ IsLocalRing.spanFinrank_maximalIdeal_add_finrank_eq_of_surjective
+ IsLocalRing.spanFinrank_maximalIdeal_quotient
+ LinearMapOfSemiLinearMapAlgebraMap
+ ModuleCat.IsCohenMacaulay
+ ModuleCat.IsCohenMacaulay_of_iso
+ ModuleCat.IsMaximalCohenMacaulay
+ ModuleCat.depth_eq_supportDim_of_cohenMacaulay
+ ModuleCat.depth_eq_supportDim_unbot_of_cohenMacaulay
+ ModuleCat.isCohenMacaulay_iff
+ 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
+ exists_isRegular_of_exists_subsingleton_ext
+ exists_isRegular_tfae
+ ext_subsingleton_of_lt_moduleDepth
+ free_of_isMaximalCohenMacaulay_of_isRegularLocalRing
+ ideal_depth_quotient_regular_sequence_add_length_eq_ideal_depth
+ instance (R : Type*) [CommRing R] (I : Ideal R) [IsNoetherianRing R] :
+ instance (priority := low) [IsNoetherianRing R] [IsLocalRing R] [Small.{v} R]
+ instance : RingHomSurjective (residue R) := ⟨residue_surjective⟩
+ instance [IsCohenMacaulayLocalRing R] : (ModuleCat.of R R).IsCohenMacaulay
+ 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_quotSMulTopIsLocalizedModuleMap
+ isMaximalCohenMacaulay_def
+ isRegular_of_span_eq_maximalIdeal
+ moduleDepth
+ moduleDepth_eq_depth_of_supp_eq
+ moduleDepth_eq_find
+ moduleDepth_eq_iff
+ moduleDepth_eq_of_iso_fst
+ moduleDepth_eq_of_iso_snd
+ moduleDepth_eq_of_linearEquiv
+ 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
+ quotSMulTopIsLocalizedModuleMap
+ quotSMulTop_isCohenMacaulay_iff_isCohenMacaulay
+ 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_shrink_eq
+ smul_top_quotSMulTop_ne_top_of_smul_top_ne_top
+ spanFinrank_eq_one_iff
+ subset_iUnion_iff_mem_of_isMaximal_of_finite
+ subsingleton_ext_of_exists_isRegular
+ toCotangentSpace
You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.
Declarations diff (Lean)
✅ Lean-aware diff — post-build, computed from the Lean environment (commit
b4d49cf).
- +136 new declarations
- −0 removed declarations
+FiniteRingKrullDim.ringKrullDim_eq_nat
+Ideal.depth
+Ideal.depth.congr_simp
+Ideal.depth_eq_of_iso
+Ideal.depth_eq_of_linearEquiv
+Ideal.depth_eq_top_of_subsingleton
+Ideal.depth_quotSMulTop_succ_eq_moduleDepth
+Ideal.span_singleton_mul_eq_self_of_isPrime
+Ideal.subset_iUnion_iff_mem_of_isMaximal_of_finite
+IsCohenMacaulayLocalRing
+IsCohenMacaulayLocalRing.casesOn
+IsCohenMacaulayLocalRing.depth_eq_dim
+IsCohenMacaulayLocalRing.mk
+IsCohenMacaulayLocalRing.of_isLocalRing_of_isCohenMacaulayRing
+IsCohenMacaulayLocalRing.rec
+IsCohenMacaulayLocalRing.recOn
+IsCohenMacaulayLocalRing.toIsLocalRing
+IsCohenMacaulayRing
+IsCohenMacaulayRing.CM_localize
+IsCohenMacaulayRing.casesOn
+IsCohenMacaulayRing.mk
+IsCohenMacaulayRing.of_isCohenMacaulayLocalRing
+IsCohenMacaulayRing.rec
+IsCohenMacaulayRing.recOn
+IsDiscreteValuationRing.of_isRegularLocalRing_of_ringKrullDim_eq_one
+IsLocalRing.CotangentSpace.congr_simp
+IsLocalRing.depth
+IsLocalRing.depth.congr_simp
+IsLocalRing.depth_eq_of_algebraMap_surjective
+IsLocalRing.depth_eq_of_iso
+IsLocalRing.depth_eq_of_linearEquiv
+IsLocalRing.depth_eq_of_ringEquiv
+IsLocalRing.depth_eq_sSup_length_regular
+IsLocalRing.depth_eq_top_of_subsingleton
+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
+IsLocalRing.instRingHomSurjectiveResidueFieldResidue
+IsLocalRing.spanFinrank_maximalIdeal_add_finrank_eq_of_surjective
+IsLocalRing.spanFinrank_maximalIdeal_quotient
+IsLocalRing.toCotangentSpace
+LinearMapOfSemiLinearMapAlgebraMap
+ModuleCat.IsCohenMacaulay
+ModuleCat.IsCohenMacaulay.casesOn
+ModuleCat.IsCohenMacaulay.congr_simp
+ModuleCat.IsCohenMacaulay.depth_eq_dim
+ModuleCat.IsCohenMacaulay.mk
+ModuleCat.IsCohenMacaulay.rec
+ModuleCat.IsCohenMacaulay.recOn
+ModuleCat.IsCohenMacaulay_of_iso
+ModuleCat.IsMaximalCohenMacaulay
+ModuleCat.IsMaximalCohenMacaulay.casesOn
+ModuleCat.IsMaximalCohenMacaulay.depth_eq_dim
+ModuleCat.IsMaximalCohenMacaulay.mk
+ModuleCat.IsMaximalCohenMacaulay.rec
+ModuleCat.IsMaximalCohenMacaulay.recOn
+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
+SemiLinearMapAlgebraMapOfLinearMap.congr_simp
+Submodule.comap_lt_top_of_lt_range
+Submodule.spanFinrank_eq_one_iff
+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
+free_of_isMaximalCohenMacaulay_of_isRegularLocalRing
+ideal_depth_quotient_regular_sequence_add_length_eq_ideal_depth
+instIsCohenMacaulayOf
+instIsDomainOfIsRegularLocalRing
+instNontrivialCarrierOfIsNoetherianRingOfIsMaximalCohenMacaulay
+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_quotSMulTopIsLocalizedModuleMap
+isMaximalCohenMacaulay_def
+isRegular_of_span_eq_maximalIdeal
+moduleDepth
+moduleDepth.congr_simp
+moduleDepth_eq_depth_of_supp_eq
+moduleDepth_eq_find
+moduleDepth_eq_iff
+moduleDepth_eq_of_iso_fst
+moduleDepth_eq_of_iso_snd
+moduleDepth_eq_of_linearEquiv
+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
+quotSMulTopIsLocalizedModuleMap
+quotSMulTop_isCohenMacaulay_iff_isCohenMacaulay
+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_shrink_eqIncrease in strong tech debt: (relative, absolute) = (7.00, 0.00)
| Current number | Change | Type (strong) |
|---|---|---|
| 5672 | 7 | backward.isDefEq.respectTransparency |
Increase in weak tech debt: (relative, absolute) = (3.00, 0.00)
| Current number | Change | Type (weak) |
|---|---|---|
| 4958 | 3 | exposed public sections |
Current commit b4d49cfc19
Reference commit 07f4b8dcd0
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
|
This PR/issue depends on: |
mathlib4-merge-conflict-bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
Bot
removed
the
merge-conflict
mathlib4-merge-conflict-bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
Bot
removed
the
merge-conflict
|
This pull request has conflicts, please merge |
mathlib4-merge-conflict-bot
added
the
merge-conflict
github-actions
Bot
removed
the
merge-conflict
mathlib4-merge-conflict-bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
Bot
removed
the
merge-conflict
|
This pull request has conflicts, please merge |
mathlib4-merge-conflict-bot
added
the
merge-conflict
github-actions
Bot
removed
merge-conflict
github-actions
Bot
added
large-import
mathlib4-merge-conflict-bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
Bot
removed
the
merge-conflict
mathlib4-merge-conflict-bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
4 participants
In this PR, we defined the concept of maximal Cohen Macaulay module, and proved that finitely generated maximal Cohen Macaulay module over regular local ring is free.
QuotSMulTop#38698