Commit 2026-03-18 17:28 7bd45ed4

View on Github →

feat(Algebra): injective dimension equal supremum of localized module (#32033) In this PR, we proved that for module over Noetherian ring, projective dimension is equal to the supremum of injective dimension of localized modules over all prime/maximal ideals.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/LocalProperties/InjectiveDimension.lean

added theorem ModuleCat.hasInjectiveDimensionLE_iff_forall_maximalSpectrum

added theorem ModuleCat.hasInjectiveDimensionLE_iff_forall_primeSpectrum

added theorem ModuleCat.injectiveDimension_eq_iSup_localizedModule_maximal

added theorem ModuleCat.injectiveDimension_eq_iSup_localizedModule_prime

added theorem ModuleCat.injectiveDimension_le_injectiveDimension_of_isLocalizedModule

added theorem ModuleCat.localizedModule_hasInjectiveDimensionLE

Modified Mathlib/RingTheory/LocalProperties/ProjectiveDimension.lean