isOpenMap_comap_C — Mathlib

English

The morphism on primes induced by C is open; a standard corollary is that imageOfDf is open in Spec R.

Русский

Гомоморфизм на пусках, индуцированный C, открыт; следствие: imageOfDf открыто.

LaTeX

$$$IsOpenMap(\\operatorname{PrimeSpectrum.comap}(C))$ and $IsOpen(imageOfDf)$$$

Lean4

/-- The morphism `C⁺ : Spec R[x] → Spec R` is open. -/
@[stacks 00FB "First part"]
theorem isOpenMap_comap_C : IsOpenMap (PrimeSpectrum.comap (C : R →+* R[X])) :=
  by
  rintro U ⟨s, z⟩
  rw [← compl_compl U, ← z, ← iUnion_of_singleton_coe s, zeroLocus_iUnion, compl_iInter, image_iUnion]
  simp_rw [← imageOfDf_eq_comap_C_compl_zeroLocus]
  exact isOpen_iUnion fun f => isOpen_imageOfDf

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