primeSpectrumEquivMaximalSpectrum

English

There exists a natural equivalence between the prime spectrum and the maximal spectrum of an Artinian ring.

Русский

Существуют естественные эквивалентности между простым спектром и максимальным спектром артинова кольца.

LaTeX

$$$\text{PrimeSpectrum}(R) \simeq \text{MaximalSpectrum}(R)$$$

Lean4

/-- The prime spectrum is in bijection with the maximal spectrum. -/
@[simps]
def primeSpectrumEquivMaximalSpectrum : PrimeSpectrum R ≃ MaximalSpectrum R
    where
  toFun I := ⟨I.asIdeal, isPrime_iff_isMaximal I.asIdeal |>.mp I.isPrime⟩
  invFun I := ⟨I.asIdeal, isPrime_iff_isMaximal I.asIdeal |>.mpr I.isMaximal⟩

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