English
Every property local at the target can be associated to an affine-target variant; this correspondence is functorial in the property.
Русский
Каждое свойство, локальное по цели, можно связать с аффинно-целью; соответствие свойств ведет себя функториально.
LaTeX
$$$\mathrm{HasAffineProperty}\ P (\mathrm{AffineTargetMorphismProperty}.of P)$ for [IsZariskiLocalAtTarget P].$$
Lean4
/-- Every property local at the target can be associated with an affine target property.
This is not an instance as the associated property can often take on simpler forms. -/
theorem of_isZariskiLocalAtTarget (P : MorphismProperty Scheme.{u}) [IsZariskiLocalAtTarget P] :
HasAffineProperty P (AffineTargetMorphismProperty.of P)
where
isLocal_affineProperty := inferInstance
eq_targetAffineLocally' := by
ext X Y f
constructor
· intro hf ⟨U, hU⟩
exact IsZariskiLocalAtTarget.restrict hf _
· intro hf
exact
P.of_zeroHypercover_target Y.affineCover fun i ↦ of_targetAffineLocally_of_isPullback (.of_hasPullback _ _) hf
