instIsLocalOfOfIsZariskiLocalAtTarget

English

If P is local at target, then the associated HasAffineProperty instance for the target is local.

Русский

Если P локально по цели, тогда связанное свойство HasAffineProperty относительно цели также локально.

LaTeX

$$$\forall P [IsZariskiLocalAtTarget P] :\mathrm{IsLocal}((\mathrm{of} P).toProperty)$$$

Lean4

instance (P : MorphismProperty Scheme) [IsZariskiLocalAtTarget P] : (of P).IsLocal
    where
  respectsIso := inferInstance
  to_basicOpen _ _ H := IsZariskiLocalAtTarget.restrict H _
  of_basicOpenCover {_ Y} _ _ _
    hs := IsZariskiLocalAtTarget.of_iSup_eq_top _ (((isAffineOpen_top Y).basicOpen_union_eq_self_iff _).mpr hs)

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