piLocalizationToMaximalEquiv — Mathlib

English

If Krull dimension is at most 0, piLocalizationToMaximal is an isomorphism.

Русский

Если размерность Кraulла не более нуля, то piLocalizationToMaximal — изоморфизм.

LaTeX

$$$\text{If Krull-dim}(R) \le 0$, then $\piLocalizationToMaximal(R)$ is an isomorphism$$

Lean4

/-- If R has Krull dimension ≤ 0, then `piLocalizationToIsMaximal R` is an isomorphism. -/
def piLocalizationToMaximalEquiv (h : ∀ I : Ideal R, I.IsPrime → I.IsMaximal) :
    PiLocalization R ≃+* MaximalSpectrum.PiLocalization R
    where
  __ := piLocalizationToMaximal R
  invFun := Pi.ringHom fun I ↦ Pi.evalRingHom _ (⟨_, h _ I.2⟩ : MaximalSpectrum R)

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