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]