ringKrullDim_quotient — Mathlib

English

For any ideal I of R, the Krull dimension of the quotient ring R/I equals the Krull dimension of the corresponding zero locus: ringKrullDim(R/I) = Order.krullDim(PrimeSpectrum.zeroLocus(I)).

Русский

Для любого идеала I кольца R размерность Крулля кольца R/I равна размерности нулевой локации, т.е. ringKrullDim(R/I) = Order.krullDim(PrimeSpectrum.zeroLocus(I)).

LaTeX

$$$\\operatorname{ringKrullDim}(R/I) = \\operatorname{Order.krullDim}(\\operatorname{PrimeSpectrum.zeroLocus}(I))$$$

Lean4

theorem ringKrullDim_quotient (I : Ideal R) :
    ringKrullDim (R ⧸ I) = Order.krullDim (PrimeSpectrum.zeroLocus (R := R) I) := by
  rw [ringKrullDim, Order.krullDim_eq_of_orderIso I.primeSpectrumQuotientOrderIsoZeroLocus]

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