isOpenMap_comap_C — Mathlib

English

The contraction map comap along the canonical inclusion C: R → R[X] is an open map; it sends open sets in Spec R[X] to open sets in Spec R.

Русский

Сужение по каноническому включению C: R → R[X] сохраняет открытые множества, то есть является открытым отображением.

LaTeX

$$$\\operatorname{IsOpenMap}\\big( \\operatorname{comap}\\ (R := R)\\ (C\\ (\\sigma := \\sigma)) \\big)$$$

Lean4

theorem isOpenMap_comap_C : IsOpenMap (comap (R := R) (C (σ := σ))) :=
  by
  intro U hU
  obtain ⟨S, hS, rfl⟩ := isTopologicalBasis_basic_opens.open_eq_sUnion hU
  rw [Set.image_sUnion]
  apply isOpen_sUnion
  rintro _ ⟨t, ht, rfl⟩
  obtain ⟨r, rfl⟩ := hS ht
  simp only [image_comap_C_basicOpen]
  exact (isClosed_zeroLocus _).isOpen_compl

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