primeSpectrumProd_symm_inr — Mathlib

English

In the canonical homeomorphism between Spec(R×S) and the product Spec(R) × Spec(S), the right projection corresponds to comap with RingHom snd.

Русский

В каноническом гомеоморфизме между Spec(R×S) и произведением Spec(R) × Spec(S) правая проекция соответствует comap по RingHom snd.

LaTeX

$$(primeSpectrumProd R S).symm (Sum.inr x) = comap (RingHom.snd R S) x$$

Lean4

theorem primeSpectrumProd_symm_inr (x) : (primeSpectrumProd R S).symm (.inr x) = comap (RingHom.snd R S) x := by ext;
  simp [Ideal.prod]

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