English
If P is local at the target and the base-change operation preserves P along affine morphisms, then P is stable under base change in general.
Русский
Если P локально относительно целевого объекта и преобразование по основанию сохраняет P для аффинных отображений, то P устойчиво при базовых изменениях в целом.
LaTeX
$$$[IsZariskiLocalAtTarget\\ P]\\ ( (of\\ P).IsStableUnderBaseChange )\\Rightarrow P.IsStableUnderBaseChange$$$
Lean4
/-- If `P` is local at the target, to show that `P` is stable under base change, it suffices to
check this for base change along a morphism of affine schemes. -/
theorem isStableUnderBaseChange_of_isStableUnderBaseChangeOnAffine_of_isZariskiLocalAtTarget
(P : MorphismProperty Scheme) [IsZariskiLocalAtTarget P] (hP₂ : (of P).IsStableUnderBaseChange) :
P.IsStableUnderBaseChange :=
letI := HasAffineProperty.of_isZariskiLocalAtTarget P
HasAffineProperty.isStableUnderBaseChange hP₂
