isMax_iff — Mathlib

English

For any x in PrimeSpectrum(R), x is maximal in the spectrum if and only if its associated ideal is maximal in R.

Русский

Для любого x в PrimeSpectrum(R) x максимально по спектру тогда и только тогда, когда связанный с ним идеал максимально в R.

LaTeX

$$$\\text{IsMax } x \\iff x.asIdeal \\text{ IsMaximal}$.$$

Lean4

/-- Also see `PrimeSpectrum.isClosed_singleton_iff_isMaximal` -/
theorem isMax_iff {x : PrimeSpectrum R} : IsMax x ↔ x.asIdeal.IsMaximal :=
  by
  refine ⟨fun hx ↦ ⟨⟨x.2.ne_top, fun I hI ↦ ?_⟩⟩, fun hx y e ↦ (hx.eq_of_le y.2.ne_top e).ge⟩
  by_contra e
  obtain ⟨m, hm, hm'⟩ := Ideal.exists_le_maximal I e
  exact hx.not_lt (show x < ⟨m, hm.isPrime⟩ from hI.trans_le hm')

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