isZariskiLocalAtTarget — Mathlib

English

IsDominant is a Zariski-local property on the target: if Y is covered by open subsets U_i and the restricted morphisms X|_{f^{-1}(U_i)} → U_i are dominant for all i, then f is dominant.

Русский

IsDominant является Zariski-локальным свойством на цели: если Y покрывается открытыми подмодулями U_i, и соответствующие ограниченные отображения доминируют на каждом i, тогда f доминирует.

LaTeX

$$$\\text{IsZariskiLocalAtTarget}(\\mathrm{IsDominant})$$$

Lean4

instance isZariskiLocalAtTarget : IsZariskiLocalAtTarget @IsDominant :=
  have : MorphismProperty.RespectsIso (topologically DenseRange) := dominant_eq_topologically ▸ IsDominant.respectsIso
  dominant_eq_topologically ▸
    topologically_isZariskiLocalAtTarget' DenseRange fun _ _ _ hU _ ↦ hU.denseRange_iff_restrictPreimage

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