instFiniteRingKrullDimOfIsNoetherianRingOfIsLocalRing

English

In a Noetherian local ring R, FiniteRingKrullDim R holds.

Русский

В локальном кольце Ноetherian R выполняется свойство FiniteRingKrullDim R.

LaTeX

$$$\text{FiniteRingKrullDim}(R)$$$

Lean4

instance [IsNoetherianRing R] [IsLocalRing R] : FiniteRingKrullDim R :=
  by
  apply finiteRingKrullDim_iff_ne_bot_and_top.mpr
  rw [← IsLocalRing.maximalIdeal_height_eq_ringKrullDim]
  constructor
  · exact WithBot.coe_ne_bot
  · rw [← WithBot.coe_top, ne_eq, WithBot.coe_inj]
    exact
      ((IsLocalRing.maximalIdeal R).finiteHeight_iff.mp
            (IsLocalRing.maximalIdeal R).finiteHeight_of_isNoetherianRing).resolve_left
        Ideal.IsPrime.ne_top'

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