primeSpectrumProdOfSum — Mathlib

English

The prime spectrum of a direct product R × S is in bijection with the disjoint union of the prime spectra of R and S.

Русский

Спектр простых идеалов произведения R × S биективно эквивален спектра R и спектра S (дисъюнктное объединение).

LaTeX

$$$\\\\operatorname{PrimeSpectrum}(R \\\\times S) \\\\cong \\\\operatorname{PrimeSpectrum}(R) \\\\oplus \\\\operatorname{PrimeSpectrum}(S)$$$

Lean4

/-- The map from the direct sum of prime spectra to the prime spectrum of a direct product. -/
@[simp]
def primeSpectrumProdOfSum : PrimeSpectrum R ⊕ PrimeSpectrum S → PrimeSpectrum (R × S)
  | Sum.inl ⟨I, _⟩ => ⟨Ideal.prod I ⊤, Ideal.isPrime_ideal_prod_top⟩
  | Sum.inr ⟨J, _⟩ => ⟨Ideal.prod ⊤ J, Ideal.isPrime_ideal_prod_top'⟩

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