Theorems · Theorem · commutative algebra

ModuleCat.projectiveDimension_eq_iSup_localizedModule_prime

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

Defined in: Mathlib.RingTheory.LocalProperties.ProjectiveDimension
Cited by: 0 results in Mathlib
Foundations: Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing Small IsNoetherianRing Module.Finite

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites29

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement and proof · cited by 17,173
ENatstatement and proof · cited by 4,985
Idealproof · cited by 4,748
iSupstatement and proof · cited by 2,415
WithBotstatement and proof · cited by 1,498
ModuleCatstatement and proof · cited by 1,429
Module.Finitestatement and proof · cited by 1,032
ModuleCat.carrierstatement and proof · cited by 997
PrimeSpectrumstatement and proof · cited by 625
ModuleCat.ofproof · cited by 594
Ideal.primeComplstatement and proof · cited by 462
Ideal.IsMaximalproof · cited by 452

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.