ringKrullDim_eq_height — Mathlib

English

For a prime ideal I in R and a localization A with AtPrime, the Krull dimension of A equals the height of I.

Русский

Для простого идеала I в R и локализации A с AtPrime размерность Крull A равна высоте I.

LaTeX

$$$\operatorname{ringKrullDim}(A) = \operatorname{height}(I).$$$

Lean4

theorem ringKrullDim_eq_height (I : Ideal R) [I.IsPrime] (A : Type*) [CommRing A] [Algebra R A]
    [IsLocalization.AtPrime A I] : ringKrullDim A = I.height :=
  by
  have := IsLocalization.AtPrime.isLocalRing A I
  rw [← IsLocalRing.maximalIdeal_primeHeight_eq_ringKrullDim, ← IsLocalization.primeHeight_comap I.primeCompl, ←
    IsLocalization.AtPrime.comap_maximalIdeal A I, Ideal.height_eq_primeHeight]

Похожие утверждения