ringKrullDim_le_iff_isMaximal_height_le

English

The Krull dimension is bounded by n iff all maximal ideals have height ≤ n.

Русский

Размерность Крull ограничена сверху n тогда и только тогда, когда каждая максимальная идеал имеет высоту ≤ n.

LaTeX

$$$\operatorname{ringKrullDim}(R) \le n \iff \forall m,\; m \text{ maximal }\Rightarrow \operatorname{height}(m) \le n.$$$

Lean4

/-- `dim R ≤ n` if and only if the height of all maximal ideals is less than `n`. -/
theorem ringKrullDim_le_iff_isMaximal_height_le {R : Type*} [CommRing R] (n : WithBot ℕ∞) :
    ringKrullDim R ≤ n ↔ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m.height ≤ n :=
  by
  rw [ringKrullDim_le_iff_height_le]
  refine ⟨fun h m hm ↦ h hm.isPrime, fun h p hp ↦ ?_⟩
  obtain ⟨m, hm, hle⟩ := p.exists_le_maximal hp.ne_top
  refine le_trans ?_ (h hm)
  norm_cast
  exact Ideal.height_mono hle

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