primeSpectrumProd — Mathlib

English

The prime spectrum of R × S is bijective to the disjoint union of PrimeSpectrum R and PrimeSpectrum S.

Русский

Спектр простых идеалов R × S образует биективное соответствие с объединением спектров R и S.

LaTeX

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

Lean4

/-- The prime spectrum of `R × S` is in bijection with the disjoint unions of the prime spectrum of
`R` and the prime spectrum of `S`. -/
noncomputable def primeSpectrumProd : PrimeSpectrum (R × S) ≃ PrimeSpectrum R ⊕ PrimeSpectrum S :=
  Equiv.symm <|
    Equiv.ofBijective (primeSpectrumProdOfSum R S)
      (by
        constructor
        · rintro (⟨I, hI⟩ | ⟨J, hJ⟩) (⟨I', hI'⟩ | ⟨J', hJ'⟩) h <;>
            simp only [mk.injEq, Ideal.prod_inj, primeSpectrumProdOfSum] at h
          · simp only [h]
          · exact False.elim (hI.ne_top h.left)
          · exact False.elim (hJ.ne_top h.right)
          · simp only [h]
        · rintro ⟨I, hI⟩
          rcases (Ideal.ideal_prod_prime I).mp hI with (⟨p, ⟨hp, rfl⟩⟩ | ⟨p, ⟨hp, rfl⟩⟩)
          · exact ⟨Sum.inl ⟨p, hp⟩, rfl⟩
          · exact ⟨Sum.inr ⟨p, hp⟩, rfl⟩)

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