English
Let R be a commutative ring. If for every maximal ideal P of R the Krull dimension of the localization R_P is at most n, then the Krull dimension of R is at most n.
Русский
Пусть R — коммутативное кольцо. Если для каждого максимального идеала P кольца R локализация R_P имеет размерность Крull ≤ n, тогда размерность Крull R ≤ n.
LaTeX
$$$\forall n \in \mathbb{N},\ (\forall (P : \mathrm{Ideal}\; R)[P. IsMaximal], \mathrm{KrullDimLE}\ n (R_P P)) \Rightarrow \mathrm{KrullDimLE}\ n \; R$$$
Lean4
theorem krullDimLE_of_isLocalization_maximal {n : ℕ} (h : ∀ (P : Ideal R) [P.IsMaximal], Ring.KrullDimLE n (Rₚ P)) :
Ring.KrullDimLE n R := by
simp_rw [Ring.krullDimLE_iff] at h ⊢
nontriviality R
rw [← Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim]
refine (WithBot.coe_le_coe).mpr (iSup₂_le_iff.mpr fun P hP ↦ ?_)
rw [← Ideal.height_eq_primeHeight, ← WithBot.coe_le_coe]
rw [← IsLocalization.AtPrime.ringKrullDim_eq_height P (Rₚ P)]
exact h P
