feat(RingTheory): regular of finite global dimension by Thmoas-Guan · Pull Request #29796 · leanprover-community/mathlib4

Thmoas-Guan · 2025-09-19T04:18:37Z

In this PR, we proved the other half of Auslander-Buchsbaum-Serre criterion, which states that a local ring is regular if it has finite global dimension, with results in #29557, we can obtain the full theorem. More APIs would be developed based on the two.

depends on: feat(Algebra): Auslander–Buchsbaum theorem #26215
depends on: feat(Algebra): Ischebeck theorem #26217
depends on: feat(Algebra): definition of global dimension #29558
depends on: feat(RingTheory): regular local ring is domain #28683

github-actions · 2025-09-19T04:19:49Z

PR summary 4ec5d95aa6

Import changes exceeding 2%

%	File
+33.54%	`Mathlib.RingTheory.Regular.Category`
+25.21%	`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	2270	+457 (+25.21%)

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.Regular.Depth`	457
`Mathlib.RingTheory.Regular.Category`	496
`Mathlib.Algebra.Category.ModuleCat.Baer` (new file)	1917
`Mathlib.RingTheory.GlobalDimension` (new file)	1921
`Mathlib.RingTheory.RegularLocalRing.Basic` (new file)	2162
`Mathlib.RingTheory.Regular.Ischebeck` (new file)	2309
`Mathlib.RingTheory.Regular.AuslanderBuchsbaum` (new file)	2357
`Mathlib.RingTheory.RegularLocalRing.AuslanderBuchsbaumSerre` (new file)	2430

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
+ IsDiscreteValuationRing.of_isRegularLocalRing_of_ringKrullDim_eq_one
+ IsLocalRing.ResidueField.map_bijective_of_surjective
+ IsLocalRing.depth
+ IsLocalRing.depth_eq_of_iso
+ IsLocalRing.depth_eq_sSup_length_regular
+ IsLocalRing.ideal_depth_eq_sSup_length_regular
+ IsLocalRing.ideal_depth_le_depth
+ IsRegularLocalRing.of_globalDimension_lt_top
+ IsRegularLocalRing.of_maximalIdeal_hasProjectiveDimensionLE
+ IsSMulRegular.of_free
+ LinearEquiv.conj_symm_exact_iff_exact
+ LinearMap.exact_lsmul_smul_top_mkQ
+ ModuleCat.exists_isRegular_of_exists_subsingleton_ext
+ ModuleCat.exists_isRegular_tfae
+ ModuleCat.free_of_projective_of_isLocalRing
+ ModuleCat.subsingleton_ext_of_exists_isRegular
+ QuotSMulTop_map
+ QuotSMulTop_map_exact
+ QuotSMulTop_map_surjective
+ Submodule.comap_lt_top_of_lt_range
+ _root_.LinearEquiv.comp_snd_exact_iff_exact
+ _root_.LinearEquiv.fst_comp_exact_iff_exact
+ basis_lift
+ basis_lift_ker_le
+ depth_le_ringKrullDim
+ depth_le_ringKrullDim_associatedPrime
+ depth_le_supportDim
+ depth_ne_top
+ exist_isSMulRegular_of_exist_hasProjectiveDimensionLE
+ exist_isSMulRegular_of_exist_hasProjectiveDimensionLE_aux
+ 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'
+ finte_free_ext_vanish_iff
+ free_depth_eq_ring_depth
+ free_iff_quotSMulTop_free
+ generate_by_regular
+ generate_by_regular_aux
+ globalDimension
+ globalDimension_eq_bot_iff
+ globalDimension_eq_sup_injectiveDimension
+ globalDimension_eq_sup_projectiveDimension_finite
+ globalDimension_le_iff
+ globalDimension_le_tfae
+ injective_of_subsingleton_ext_quotient_one
+ instance (I : Ideal R) (M : Type*) [AddCommGroup M] [Module R M]
+ instance [IsRegularLocalRing R] : IsDomain R := isDomain_of_isRegularLocalRing R
+ isDomain_of_isRegularLocalRing
+ isRegular_of_span_eq_maximalIdeal
+ ker_mapRange_eq_smul_top
+ 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
+ nontrivial_ring_of_nontrivial_module
+ projectiveDimension_eq_quotient
+ quotient_isRegularLocalRing_tfae
+ quotient_prime_ringKrullDim_ne_bot
+ quotient_span_singleton
+ ring_depth_invariant
+ ring_depth_uLift
+ smulShortComplex_f_eq_smul_id
+ smulShortComplex_f_hom_eq_smul_id
+ smul_prod_of_smul
+ spanFinrank_maximalIdeal_quotient
+ 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) = (24.00, 0.00)

Current number	Change	Type
6919	24	backward.isDefEq

Current commit 93ef8e2ec0
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 · 2025-09-19T04:35:34Z

This PR/issue depends on:

mathlib4-merge-conflict-bot · 2025-09-23T20:27:15Z