Documentation

TauCeti.RingTheory.GlobalDimension

The global dimension of a ring #

The (left) global dimension of a ring R is the supremum of the projective dimensions of all R-modules (Stacks, Definition 10.109.10 (00O6)). It is the invariant through which Serre's theorem characterizes regular local rings: a Noetherian local ring is regular iff its global dimension is finite, and then it equals the Krull dimension.

Main definitions #

Main results #

Implementation notes #

The definition follows the supremum form of Nailin Guan's Mathlib pull request mathlib4#29558, including its universe parameter v for the category of modules.

References #

source
noncomputable def TauCeti.globalDimension (R : Type u) [Ring R] :
WithBot ℕ∞

The global dimension of a ring R: the supremum of the projective dimensions of all R-modules in ModuleCat.{v} R. Stacks, Definition 10.109.10 (00O6).

Instances For
    source
    theorem TauCeti.globalDimension_def (R : Type u) [Ring R] :
    globalDimension R = ⨆ (M : ModuleCat R), CategoryTheory.projectiveDimension M

    Unfolds globalDimension as the supremum of the projective dimensions of all modules.

    source
    theorem ModuleCat.projectiveDimension_le_globalDimension {R : Type u} [Ring R] (M : ModuleCat R) :
    CategoryTheory.projectiveDimension M ≤ TauCeti.globalDimension R

    The projective dimension of every module is at most the global dimension of the ring.

    source
    theorem TauCeti.globalDimension_le_iff (R : Type u) [Ring R] (d : WithBot ℕ∞) :
    globalDimension R ≤ d ↔ ∀ (M : ModuleCat R), CategoryTheory.projectiveDimension M ≤ d

    The global dimension is at most d iff every module has projective dimension at most d.

    source
    theorem TauCeti.globalDimension_le_iff_hasProjectiveDimensionLE (R : Type u) [Ring R] (n : ℕ) :
    globalDimension R ≤ ↑n ↔ ∀ (M : ModuleCat R), CategoryTheory.HasProjectiveDimensionLE M n

    The global dimension is at most n iff every module has projective dimension at most n.

    source
    theorem TauCeti.globalDimension_le_iff_hasInjectiveDimensionLE (R : Type u) [Ring R] [Small.{v, u} R] (n : ℕ) :
    globalDimension R ≤ ↑n ↔ ∀ (M : ModuleCat R), CategoryTheory.HasInjectiveDimensionLE M n

    The global dimension is at most n iff every module has injective dimension at most n: both conditions say that all Ext groups vanish above degree n.

    source
    @[simp]
    theorem TauCeti.globalDimension_eq_bot_iff (R : Type u) [Ring R] [Small.{v, u} R] :
    globalDimension R = ⊥ ↔ Subsingleton R

    Only the zero ring has global dimension ⊥.

    source
    theorem TauCeti.globalDimension_le_tfae (R : Type u) [Ring R] [Small.{v, u} R] (n : ℕ) :
    [globalDimension R ≤ ↑n, ∀ (M : ModuleCat R), Module.Finite R ↑M → CategoryTheory.HasProjectiveDimensionLE M n, ∀ (I : Ideal R), CategoryTheory.HasProjectiveDimensionLE (↧(Shrink.{v, u} (R ⧸ I))) n].TFAE

    The global dimension is detected on finite and on cyclic modules. For a natural number n, the following are equivalent: the global dimension of R is at most n; every finite R-module has projective dimension at most n; every cyclic module R ⧸ I has projective dimension at most n. Stacks, Lemma 10.109.12 (065T).

    source
    theorem TauCeti.globalDimension_eq_iSup_cyclic (R : Type u) [Ring R] [Small.{v, u} R] :
    globalDimension R = ⨆ (I : Ideal R), CategoryTheory.projectiveDimension ↧(Shrink.{v, u} (R ⧸ I))

    Auslander's theorem: the global dimension is the supremum over cyclic modules. The global dimension of R is the supremum of the projective dimensions of the cyclic modules R ⧸ I, for I a left ideal. M. Auslander, On the dimension of modules and algebras III, Theorem 1.

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

    The global dimension is the supremum over finite modules. The global dimension of R is the supremum of the projective dimensions of the finite R-modules: this supremum lies between the one over the cyclic modules (TauCeti.globalDimension_eq_iSup_cyclic) and the one over all modules.

    source
    theorem TauCeti.globalDimension_eq_zero_of_isSemisimpleRing (R : Type u) [Ring R] [IsSemisimpleRing R] [Nontrivial R] [Small.{v, u} R] :
    globalDimension R = 0

    A nonzero semisimple ring, for instance a field or a division ring, has global dimension zero: every module over it is projective.

    source
    theorem TauCeti.globalDimension_eq_globalDimension (R : Type u) [Ring R] [Small.{v, u} R] [Small.{v', u} R] :
    globalDimension R = globalDimension R

    The global dimension does not depend on the universe of the modules, as long as the ring is small in both universes.

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

    Localization does not increase the global dimension. For a submonoid S of R, the global dimension of S⁻¹R is at most that of R. Stacks, Lemma 10.109.13 (00O8).

    source
    theorem TauCeti.globalDimension_le_of_faithfullyFlat {R : Type u} [CommRing R] {S : Type u} [CommRing S] [Algebra R S] [IsNoetherianRing R] [Module.FaithfullyFlat R S] :
    globalDimension R ≤ globalDimension S

    Global dimension descends along faithfully flat algebras. A noetherian ring R has global dimension at most that of any faithfully flat R-algebra S: the projective dimension of a finite R-module equals that of its base change to S (ModuleCat.hasProjectiveDimensionLE_baseChange_iff), and finite modules detect the global dimension.

    source
    theorem TauCeti.globalDimension_eq_one_of_isPrincipalIdealRing {R : Type u} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [Small.{v, u} R] (hR : ¬IsField R) :
    globalDimension R = 1

    A principal ideal domain that is not a field has global dimension one. Every module has projective dimension at most one, and a cyclic module R ⧸ (a) with a a nonzero nonunit has projective dimension exactly one (ModuleCat.projectiveDimension_quotient_span_singleton_eq_one).