The Global Dimension of a Ring

In this file, we define the global dimension of ring and proved some of its basic properties.

Main definition and results

• globalDimension : The global (homological) dimension of a (commutative) ring defined as the supremum of projective dimension over all modules.

• globalDimension_le_tfae : For natrual number n, globalDimension R ≤ n iff all finitely generated modules over R has projective dimension not exceeding n iff for all Ext N M (n + 1) vanish.

• globalDimension_eq_sup_projectiveDimension_finite : Global dimension is equal to the supremum of projective dimension over finitely generated modules.

noncomputable def globalDimension (R : Type u) [CommRing R] : WithBot ℕ∞

The global (homological) dimension of a (commutative) ring defined as the supremum of projective dimension over all modules.

Equations

• globalDimension R = ⨆ (M : ModuleCat R), CategoryTheory.projectiveDimension M

theorem globalDimension_eq_bot_iff (R : Type u) [CommRing R] [Small.{v, u} R] : globalDimension R = ⊥ ↔ Subsingleton R

theorem globalDimension_le_iff (R : Type u) [CommRing R] (n : ℕ) : globalDimension R ≤ ↑n ↔ ∀ (M : ModuleCat R), CategoryTheory.HasProjectiveDimensionLE M n

theorem globalDimension_le_tfae (R : Type u) [CommRing R] [Small.{v, u} R] (n : ℕ) : [globalDimension R ≤ ↑n, ∀ (M : ModuleCat R) [Module.Finite R ↑M], CategoryTheory.HasProjectiveDimensionLE M n, ∀ (N M : ModuleCat R), Subsingleton (CategoryTheory.Abelian.Ext N M (n + 1)), ∀ (M : ModuleCat R), CategoryTheory.HasInjectiveDimensionLE M n].TFAE

theorem globalDimension_eq_sup_projectiveDimension_finite (R : Type u) [CommRing R] [Small.{v, u} R] : globalDimension R = ⨆ (M : ModuleCat R), ⨆ (_ : Module.Finite R ↑M), CategoryTheory.projectiveDimension M

theorem globalDimension_eq_sup_injectiveDimension (R : Type u) [CommRing R] [Small.{v, u} R] : globalDimension R = ⨆ (M : ModuleCat R), CategoryTheory.injectiveDimension M

theorem globalDimension_eq_of_small (R : Type u) [CommRing R] [Small.{v, u} R] : globalDimension R = globalDimension R

Global dimension is invariant of universe level when assume ring itself small.

theorem globalDimension_eq_of_ringEquiv (R : Type u) [CommRing R] (R' : Type u') [CommRing R'] (e : R ≃+* R') : globalDimension R = globalDimension R'

theorem globalDimension_localization_le {R : Type u} [CommRing R] [Small.{v, u} R] (S : Submonoid R) : globalDimension (Localization S) ≤ globalDimension R

theorem globalDimension_eq_iSup_loclization_prime (R : Type u) [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] : globalDimension R = ⨆ (p : PrimeSpectrum R), globalDimension (Localization.AtPrime p.asIdeal)

theorem globalDimension_eq_iSup_loclization_maximal (R : Type u) [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] : globalDimension R = ⨆ (p : MaximalSpectrum R), globalDimension (Localization.AtPrime p.asIdeal)