instIsZariskiLocalAtTarget — Mathlib

English

UniversallyOpen is a Zariski-local property on the target: if a morphism is universally open after restricting to a Zariski cover of the target, then it is universally open.

Русский

Sвойство универсально открытости локально по цели: если морфизм является универсально открытым после ограничений на покрытии поЗарски цели, то он таковым и является.

LaTeX

$$$\IsZariskiLocalAtTarget(\mathsf{UniversallyOpen}).$$$

Lean4

instance : IsZariskiLocalAtTarget @UniversallyOpen := by
  rw [eq]
  apply universally_isZariskiLocalAtTarget
  intro X Y f ι U hU H
  simp_rw [topologically, morphismRestrict_base] at H
  exact hU.isOpenMap_iff_restrictPreimage.mpr H

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