WIP: any regular local ring is a UFD

[mbkybky]

Show that any regular local ring is a unique factorization domain.

• depends on: feat(Algebra/RingTheory): Auslander–Buchsbaum–Serre criterion and its corollaries #29802
• depends on: [Merged by Bors] - feat(RingTheory): UFD criteria via height 1 prime ideals and localization #36739
• depends on: feat(Algebra/Module): define modules admitting finite free resolutions #39067
• depends on: feat(RingTheory/LocalProperties): Module.Invertible is a local property #39420
• depends on: feat(Algebra/Module): flat base change of modules admitting finite free resolutions #40290
• depends on: feat(CategoryTheory/ObjectProperty): define objects admitting finite resolutions by objects satisfying P : ObjectProperty C #41880

---

Prepared with Codex

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[github-actions]

PR summary a277a2ff8e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.ObjectProperty.HasFiniteResolution.Basic (new file)	802
Mathlib.CategoryTheory.ObjectProperty.HasFiniteResolution.Exact (new file)	999
Mathlib.Algebra.Module.FiniteFreeResolution.Basic (new file)	1666
Mathlib.Algebra.Module.FiniteFreeResolution.Exact (new file)	1684
Mathlib.Algebra.Module.StablyFree.HasFiniteFreeResolution (new file)	1686
Mathlib.Algebra.Module.FiniteFreeResolution.BaseChange (new file)	1767
Mathlib.Algebra.Category.ModuleCat.Ext.Baer (new file)	1945
Mathlib.RingTheory.GlobalDimension (new file)	2138
Mathlib.RingTheory.RegularLocalRing.Basic (new file)	2218
Mathlib.RingTheory.LocalProperties.Invertible (new file)	2228
Mathlib.Algebra.Module.FiniteFreeResolution.HasProjectiveDimensionLE (new file)	2236
Mathlib.RingTheory.Depth.Basic (new file)	2324
Mathlib.RingTheory.Depth.Ischebeck (new file)	2360
Mathlib.RingTheory.Depth.AuslanderBuchsbaum (new file)	2411
Mathlib.RingTheory.CohenMacaulay.Basic (new file)	2465
Mathlib.RingTheory.CohenMacaulay.Maximal (new file)	2479
Mathlib.RingTheory.RegularLocalRing.AuslanderBuchsbaumSerre (new file)	2494
Mathlib.RingTheory.RegularLocalRing.GlobalDimension (new file)	2501
Mathlib.RingTheory.RegularLocalRing.Localization (new file)	2503
Mathlib.RingTheory.RegularLocalRing.UFD (new file)	2615

---

Declarations diff (regex)

+ AuslanderBuchsbaum
+ AuslanderBuchsbaum_one
+ Auslander_Buchsbaum_Serre
+ FinitePresentation.of_finite_of_flat_of_rankAtStalk_constant
+ FiniteRingKrullDim.ringKrullDim_eq_nat
+ HasFiniteFreeResolution
+ HasFiniteFreeResolution.iff_isStablyFree
+ HasFiniteFreeResolution.isStablyFree
+ HasFiniteFreeResolution.localizedModule
+ HasFiniteFreeResolution.of_flat_baseChange
+ HasFiniteFreeResolution.of_isBaseChange_of_flat
+ HasFiniteFreeResolution.of_projectiveDimension_ne_top
+ HasFiniteFreeResolutionOfLength
+ HasFiniteFreeResolutionOfLength.isStablyFree_of_projective
+ HasFiniteFreeResolutionOfLength.localizedModule
+ HasFiniteFreeResolutionOfLength.of_flat_baseChange
+ HasFiniteFreeResolutionOfLength.of_hasProjectiveDimensionLE
+ HasFiniteFreeResolutionOfLength.of_isBaseChange_of_flat
+ HasFiniteResolution
+ HasFiniteResolutionOfLength
+ HasFiniteResolutionOfLength.biprod_right
+ 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.isPrincipal_of_free
+ Ideal.span_singleton_mul_eq_self_of_isPrime
+ Invertible.of_isLocalized_maximal
+ Invertible.of_localized_maximal
+ 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
+ IsLocalization.AtPrime.ringKrullDim_lt_of_lt_maximalIdeal
+ IsRegularLocalRing.globalDimension_eq_ringKrullDim
+ IsRegularLocalRing.of_globalDimension_lt_top
+ IsRegularLocalRing.of_isLocalization
+ IsRegularLocalRing.of_maximalIdeal_hasProjectiveDimensionLE
+ IsRegularRing.globalDimension_eq_ringKrullDim
+ IsSMulRegular.of_free
+ LinearMapOfSemiLinearMapAlgebraMap
+ ModuleCat.IsCohenMacaulay
+ ModuleCat.IsCohenMacaulay_of_iso
+ ModuleCat.IsMaximalCohenMacaulay
+ ModuleCat.depth_eq_supportDim_of_cohenMacaulay
+ ModuleCat.depth_eq_supportDim_unbot_of_cohenMacaulay
+ ModuleCat.free_of_projective_of_isLocalRing
+ ModuleCat.isCohenMacaulay_iff
+ QuotSMulTopMap
+ SemiLinearMapAlgebraMapOfLinearMap
+ Submodule.comap_lt_top_of_lt_range
+ _root_.CategoryTheory.ShortComplex.ShortExact.pullback
+ _root_.CategoryTheory.ShortComplex.ShortExact.pullback_symm
+ 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
+ elim
+ exist_isSMulRegular_of_exist_hasProjectiveDimensionLE
+ exist_isSMulRegular_of_exist_hasProjectiveDimensionLE_aux
+ extQuotientBotZeroEquiv
+ ext_hom_zero_of_mem_ideal_smul
+ ext_quotient_one_subsingleton_iff
+ ext_subsingleton_of_lt_moduleDepth
+ finiteFree
+ finiteFree_isClosedUnderBinaryProducts
+ finiteFree_isClosedUnderIsomorphisms
+ finiteFree_le_projective
+ finiteFree_of
+ finite_projectiveDimension_of_isRegularLocalRing_aux
+ finte_free_ext_vanish_iff
+ free_depth_eq_ring_depth
+ free_of_isMaximalCohenMacaulay_of_isRegularLocalRing
+ generate_by_regular
+ generate_by_regular_aux
+ 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
+ hasFiniteResolution
+ hasInjectiveDimensionLE_of_quotients
+ hasInjectiveDimensionLT_iff_quotients
+ hasInjectiveDimensionLT_of_quotients
+ horseshoe_middle_shortExact
+ ideal_depth_quotient_regular_sequence_add_length_eq_ideal_depth
+ induction_on
+ injective_iff_subsingleton_ext_quotient_one
+ injective_of_subsingleton_ext_quotient_one
+ instance (I : Ideal R) (M : Type*) [AddCommGroup M] [Module R M]
+ instance (R : Type*) [CommRing R] (I : Ideal R) [IsNoetherianRing R] :
+ instance (priority := low) [IsNoetherianRing R] [IsLocalRing R] [Small.{v} R]
+ instance (priority := low) uniqueFactorizationMonoid [IsRegularLocalRing R] :
+ instance : RingHomSurjective (residue R) := ⟨residue_surjective⟩
+ instance [IsCohenMacaulayLocalRing R] : (ModuleCat.of R R).IsCohenMacaulay
+ instance [IsRegularLocalRing R] : IsDomain R := isDomain_of_isRegularLocalRing R
+ instance [P.Is X] : P.HasFiniteResolution X
+ instance [Small.{max w v} R] [HasFiniteFreeResolution R M] :
+ instance [Small.{w} R] [Small.{w} M] [HasFiniteFreeResolution R M] :
+ 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
+ isRegularLocalRing_localization
+ isRegularRing_of_globalDimension_lt_top
+ isRegularRing_of_isRegularLocalRing
+ isRegularRing_of_localization_maximal_isRegularLocalRing
+ isRegular_of_span_eq_maximalIdeal
+ left_of_right
+ mem_smul_top_of_range_le_smul_top
+ middle_of_right
+ 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
+ module_finite
+ nontrivial_ring_of_nontrivial_module
+ of_finite_of_free
+ of_property
+ of_shortExact
+ of_shrink
+ of_ulift
+ one_subsingleton_iff_of_projective
+ out
+ pairCone
+ pairConeIsLimit
+ projectiveDimension_eq_quotient
+ projectiveDimension_ne_top_of_isRegularLocalRing
+ prop_biprod_of_isClosedUnderBinaryProducts
+ property_of_zero
+ quotSMulTopIsLocalizedModuleMap
+ quotSMulTopMap_exact
+ quotSMulTopMap_surjective
+ 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_prod_of_smul
+ spanFinrank_maximalIdeal_quotient
+ subsingleton_of_ext_quotient_bot_zero
+ subsingleton_of_pi
+ succ
+ toCotangentSpace
+ ufd_localization_away_of_prime_of_nonmaximal_localizations_ufd
+ zero
++ map_exactFunctor
++ mono
++ of_iso
++ of_linearEquiv
++ of_shortExact_of_left_of_middle
++ of_shortExact_of_left_of_right
++ of_shortExact_of_middle_of_right
++ property
++ property_of_le

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

• +267 new declarations
• −0 removed declarations

(showing first 200 of 267 lines)

+AuslanderBuchsbaum
+AuslanderBuchsbaum_one
+Auslander_Buchsbaum_Serre
+CategoryTheory.Abelian.Ext.one_subsingleton_iff_of_projective
+CategoryTheory.ObjectProperty.HasFiniteResolution
+CategoryTheory.ObjectProperty.HasFiniteResolution.casesOn
+CategoryTheory.ObjectProperty.HasFiniteResolution.elim
+CategoryTheory.ObjectProperty.HasFiniteResolution.instOfIs
+CategoryTheory.ObjectProperty.HasFiniteResolution.map_exactFunctor
+CategoryTheory.ObjectProperty.HasFiniteResolution.mk
+CategoryTheory.ObjectProperty.HasFiniteResolution.mono
+CategoryTheory.ObjectProperty.HasFiniteResolution.of_iso
+CategoryTheory.ObjectProperty.HasFiniteResolution.of_property
+CategoryTheory.ObjectProperty.HasFiniteResolution.of_shortExact
+CategoryTheory.ObjectProperty.HasFiniteResolution.of_shortExact_of_left_of_middle
+CategoryTheory.ObjectProperty.HasFiniteResolution.of_shortExact_of_left_of_right
+CategoryTheory.ObjectProperty.HasFiniteResolution.of_shortExact_of_middle_of_right
+CategoryTheory.ObjectProperty.HasFiniteResolution.out
+CategoryTheory.ObjectProperty.HasFiniteResolution.property
+CategoryTheory.ObjectProperty.HasFiniteResolution.property_of_le
+CategoryTheory.ObjectProperty.HasFiniteResolution.rec
+CategoryTheory.ObjectProperty.HasFiniteResolution.recOn
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.below
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.below.casesOn
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.below.rec
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.below.succ
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.below.zero
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.biprod_right
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.brecOn
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.casesOn
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.hasFiniteResolution
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.map_exactFunctor
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.mono
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.of_iso
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.property
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.property_of_le
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.property_of_zero
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.rec
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.recOn
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.succ
+CategoryTheory.ObjectProperty.HasFiniteResolutionOfLength.zero
+CategoryTheory.ObjectProperty.horseshoe_middle_shortExact
+CategoryTheory.ObjectProperty.prop_biprod_of_isClosedUnderBinaryProducts
+CategoryTheory.ShortComplex.ShortExact.pullback
+CategoryTheory.ShortComplex.ShortExact.pullback_symm
+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.isPrincipal_of_free
+Ideal.span_singleton_mul_eq_self_of_isPrime
+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
+IsLocalization.AtPrime.ringKrullDim_lt_of_lt_maximalIdeal
+IsRegularLocalRing.globalDimension_eq_ringKrullDim
+IsRegularLocalRing.of_globalDimension_lt_top
+IsRegularLocalRing.of_isLocalization
+IsRegularLocalRing.of_maximalIdeal_hasProjectiveDimensionLE
+IsRegularLocalRing.uniqueFactorizationMonoid
+IsRegularRing.globalDimension_eq_ringKrullDim
+IsSMulRegular.of_free
+LinearMapOfSemiLinearMapAlgebraMap
+Module.FinitePresentation.of_finite_of_flat_of_rankAtStalk_constant
+Module.HasFiniteFreeResolution
+Module.HasFiniteFreeResolution.iff_isStablyFree
+Module.HasFiniteFreeResolution.instShrinkOfSmall
+Module.HasFiniteFreeResolution.instULiftOfSmall
+Module.HasFiniteFreeResolution.isStablyFree
+Module.HasFiniteFreeResolution.localizedModule
+Module.HasFiniteFreeResolution.module_finite
+Module.HasFiniteFreeResolution.of_finite_of_free
+Module.HasFiniteFreeResolution.of_flat_baseChange
+Module.HasFiniteFreeResolution.of_isBaseChange_of_flat
+Module.HasFiniteFreeResolution.of_linearEquiv
+Module.HasFiniteFreeResolution.of_projectiveDimension_ne_top
+Module.HasFiniteFreeResolution.of_shortExact_of_left_of_middle
+Module.HasFiniteFreeResolution.of_shortExact_of_left_of_right
+Module.HasFiniteFreeResolution.of_shortExact_of_middle_of_right
+Module.HasFiniteFreeResolution.of_shrink
+Module.HasFiniteFreeResolution.of_ulift
+Module.HasFiniteFreeResolution.out
+Module.HasFiniteFreeResolutionOfLength
+Module.HasFiniteFreeResolutionOfLength.induction_on
+Module.HasFiniteFreeResolutionOfLength.isStablyFree_of_projective
+Module.HasFiniteFreeResolutionOfLength.localizedModule
+Module.HasFiniteFreeResolutionOfLength.module_finite
+Module.HasFiniteFreeResolutionOfLength.of_flat_baseChange
+Module.HasFiniteFreeResolutionOfLength.of_hasProjectiveDimensionLE
+Module.HasFiniteFreeResolutionOfLength.of_isBaseChange_of_flat
+Module.HasFiniteFreeResolutionOfLength.of_linearEquiv
+Module.HasFiniteFreeResolutionOfLength.succ
+Module.HasFiniteFreeResolutionOfLength.zero
+Module.Invertible.of_isLocalized_maximal
+Module.Invertible.of_localized_maximal
+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.ext_quotient_one_subsingleton_iff
+ModuleCat.finiteFree
+ModuleCat.finiteFree_isClosedUnderBinaryProducts
+ModuleCat.finiteFree_isClosedUnderIsomorphisms
+ModuleCat.finiteFree_le_projective
+ModuleCat.finiteFree_of
+ModuleCat.free_of_projective_of_isLocalRing
+ModuleCat.hasInjectiveDimensionLE_of_quotients
+ModuleCat.hasInjectiveDimensionLT_iff_quotients
+ModuleCat.hasInjectiveDimensionLT_of_quotients
+ModuleCat.injective_iff_subsingleton_ext_quotient_one
+ModuleCat.injective_of_subsingleton_ext_quotient_one
+ModuleCat.isCohenMacaulay_iff
+ModuleCat.shortComplexOfConj.congr_simp
+QuotSMulTopMap
+SemiLinearMapAlgebraMapOfLinearMap
+SemiLinearMapAlgebraMapOfLinearMap.congr_simp
+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_isSMulRegular_of_exist_hasProjectiveDimensionLE
+exist_isSMulRegular_of_exist_hasProjectiveDimensionLE_aux
+ext_hom_zero_of_mem_ideal_smul
+ext_subsingleton_of_lt_moduleDepth
+finite_projectiveDimension_of_isRegularLocalRing_aux
+finte_free_ext_vanish_iff
+free_depth_eq_ring_depth
+free_of_isMaximalCohenMacaulay_of_isRegularLocalRing
+generate_by_regular
+generate_by_regular_aux
+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
+instFiniteQuotientIdealSubmoduleHSMulTop
+instIsCohenMacaulayOf

---

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

Current number	Change	Type (strong)
499	1	erw
7133	8	backward.isDefEq.respectTransparency

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

Current number	Change	Type (weak)
5023	10	exposed public sections

Current commit a277a2ff8e
Reference commit abb22825db

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

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Algebra/RingTheory): Auslander–Buchsbaum–Serre criterion and its corollaries #29802
• [Merged by Bors] - feat(RingTheory): UFD criteria via height 1 prime ideals and localization #36739
• feat(Algebra/Module): define modules admitting finite free resolutions #39067
• feat(RingTheory/LocalProperties): Module.Invertible is a local property #39420
• feat(Algebra/Module): flat base change of modules admitting finite free resolutions #40290
• feat(CategoryTheory/ObjectProperty): define objects admitting finite resolutions by objects satisfying P : ObjectProperty C #41880
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

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