primeSpectrumProd_symm_inl — Mathlib

English

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

Русский

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

LaTeX

$$(primeSpectrumProd R P).symm (Sum.inl x) = comap (RingHom.fst R S) x$$

Lean4

theorem primeSpectrumProd_symm_inl (x) : (primeSpectrumProd R S).symm (.inl x) = comap (RingHom.fst R S) x := by ext;
  simp [Ideal.prod]

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