English
The prime spectrum of a product ring R×S is canonically homeomorphic to the disjoint union of the prime spectra of R and S.
Русский
Спектр произвольного произведения кольца R×S естественно гомеоморфен с несмежной суммой спектров Specr(R) ⊕ Specr(S).
LaTeX
$$$$\\operatorname{PrimeSpectrum}(R\\times S) \\cong_t \\operatorname{PrimeSpectrum}(R) \\oplus \\operatorname{PrimeSpectrum}(S).$$$$
Lean4
/-- The prime spectrum of `R × S` is homeomorphic
to the disjoint union of `PrimeSpectrum R` and `PrimeSpectrum S`. -/
noncomputable def primeSpectrumProdHomeo : PrimeSpectrum (R × S) ≃ₜ PrimeSpectrum R ⊕ PrimeSpectrum S :=
by
refine ((primeSpectrumProd R S).symm.toHomeomorphOfIsInducing ?_).symm
refine (IsClosedEmbedding.of_continuous_injective_isClosedMap ?_ (Equiv.injective _) ?_).isInducing
· rw [continuous_sum_dom]
simp only [Function.comp_def, primeSpectrumProd_symm_inl, primeSpectrumProd_symm_inr]
exact ⟨(comap _).2, (comap _).2⟩
· simp_rw [isClosedMap_sum, primeSpectrumProd_symm_inl, primeSpectrumProd_symm_inr]
exact ⟨isClosedEmbedding_comap_fst.isClosedMap, isClosedEmbedding_comap_snd.isClosedMap⟩
