The Projective Dimension Equal to Supremum over Localizations

In this file, we proved that projective dimension equal to supremum over localizations

Main definition and results

instance ModuleCat.instPreservesProjectiveObjectsLocalizationLocalizedModuleFunctor {R : Type u} [CommRing R] [Small.{v, u} R] (S : Submonoid R) : (localizedModuleFunctor S).PreservesProjectiveObjects

theorem ModuleCat.localizedModule_hasProjectiveDimensionLE {R : Type u} [CommRing R] [Small.{v, u} R] (n : ℕ) (S : Submonoid R) (M : ModuleCat R) [CategoryTheory.HasProjectiveDimensionLE M n] : CategoryTheory.HasProjectiveDimensionLE (M.localizedModule S) n

theorem ModuleCat.projectiveDimension_le_projectiveDimension_of_isLocalizedModule {R : Type u} [CommRing R] [Small.{v, u} R] (S : Submonoid R) (M : ModuleCat R) : CategoryTheory.projectiveDimension (M.localizedModule S) ≤ CategoryTheory.projectiveDimension M

theorem ModuleCat.hasProjectiveDimensionLE_iff_forall_maximalSpectrum {R : Type u} [CommRing R] (n : ℕ) [Small.{v, u} R] [IsNoetherianRing R] (M : ModuleCat R) [Module.Finite R ↑M] : CategoryTheory.HasProjectiveDimensionLE M n ↔ ∀ (m : MaximalSpectrum R), CategoryTheory.HasProjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n

theorem ModuleCat.hasProjectiveDimensionLE_iff_forall_primeSpectrum {R : Type u} [CommRing R] (n : ℕ) [Small.{v, u} R] [IsNoetherianRing R] (M : ModuleCat R) [Module.Finite R ↑M] : CategoryTheory.HasProjectiveDimensionLE M n ↔ ∀ (p : PrimeSpectrum R), CategoryTheory.HasProjectiveDimensionLE (M.localizedModule p.asIdeal.primeCompl) n

theorem ModuleCat.projectiveDimension_eq_iSup_localizedModule_prime {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] (M : ModuleCat R) [Module.Finite R ↑M] : CategoryTheory.projectiveDimension M = ⨆ (p : PrimeSpectrum R), CategoryTheory.projectiveDimension (M.localizedModule p.asIdeal.primeCompl)

theorem ModuleCat.projectiveDimension_eq_iSup_localizedModule_maximal {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] (M : ModuleCat R) [Module.Finite R ↑M] : CategoryTheory.projectiveDimension M = ⨆ (p : MaximalSpectrum R), CategoryTheory.projectiveDimension (M.localizedModule p.asIdeal.primeCompl)