universallyClosed_isZariskiLocalAtTarget

English

The property of being universally closed is local on the target in the Zariski topology: if a morphism g is universally closed, then its base-changes along Zariski-local coverings preserve universal closedness.

Русский

Свойство быть универсально замкнутым локально по цели в зариусской топологии: если морфизм g универсально замкнут, то его изменение основания вдоль зариуских локальных покрытий сохраняет это свойство.

LaTeX

$$$\operatorname{IsZariskiLocalAtTarget}(\operatorname{UniversallyClosed}).$$$

Lean4

instance universallyClosed_isZariskiLocalAtTarget : IsZariskiLocalAtTarget @UniversallyClosed :=
  by
  rw [universallyClosed_eq]
  apply universally_isZariskiLocalAtTarget
  intro X Y f ι U hU H
  simp_rw [topologically, morphismRestrict_base] at H
  exact hU.isClosedMap_iff_restrictPreimage.mpr H

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