Relation of Injective Dimension with Localizations

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

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

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

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

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

theorem ModuleCat.injectiveDimension_eq_iSup_localizedModule_prime {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] (M : ModuleCat R) : CategoryTheory.injectiveDimension M = ⨆ (p : PrimeSpectrum R), CategoryTheory.injectiveDimension (M.localizedModule p.asIdeal.primeCompl)

theorem ModuleCat.injectiveDimension_eq_iSup_localizedModule_maximal {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] (M : ModuleCat R) : CategoryTheory.injectiveDimension M = ⨆ (p : MaximalSpectrum R), CategoryTheory.injectiveDimension (M.localizedModule p.asIdeal.primeCompl)