equivMaximalSpectrum — Mathlib

English

There is an equivalence between the height-one spectrum and the maximal spectrum for rings of Krull dimension 1 (when R is not a field).

Русский

Существует эквивалентность между спектром высоты1 и максимальным спектром колец с размерностью Круля 1 (при условии, что R не поле).

LaTeX

$$$\\text{equivMaximalSpectrum}(hR) : \\HeightOneSpectrum(R) \\simeq \\MaximalSpectrum(R)$$$

Lean4

/-- An equivalence between the height one and maximal spectra for rings of Krull dimension 1. -/
def equivMaximalSpectrum (hR : ¬IsField R) : HeightOneSpectrum R ≃ MaximalSpectrum R
    where
  toFun v := ⟨v.asIdeal, v.isPrime.isMaximal v.ne_bot⟩
  invFun v := ⟨v.asIdeal, v.isMaximal.isPrime, Ring.ne_bot_of_isMaximal_of_not_isField v.isMaximal hR⟩

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