English
Let P and Q be morphism properties with the affine-local property HasAffineProperty P Q. If i_X: UX → X and i_Y: UY → Y fit into a pullback square with f' : UX → UY and f: X → Y, and hf says that f has property P, then f' has property Q.
Русский
Пусть P и Q — свойства морфизмов между схемами, удовлетворяющие афинной локальности HasAffineProperty P Q. Если существует диаграмма-подобная в виде pullback квадрата с f' : UX → UY и f : X → Y и граничное условие h, что h образует pullback i_X, f', f, i_Y, и hf : P f, тогда f' удовлетворяет свойству Q.
LaTeX
$$$\forall P\, Q\, [\text{HasAffineProperty } P Q],\; \forall X,Y:\Scheme,\; \forall f:X\to Y, \forall i_X:UX\to X, \forall i_Y:UY\to Y,\forall f':UX\to UY,\; (h:\mathrm{IsPullback}\; i_X\; f'\; f\; i_Y)\; (hf:\, P\,f)\;\Rightarrow\; Q\,f' $$$
Lean4
theorem of_isPullback {UX UY : Scheme.{u}} [IsAffine UY] {iY : UY ⟶ Y} [IsOpenImmersion iY] {iX : UX ⟶ X} {f' : UX ⟶ UY}
(h : IsPullback iX f' f iY) (hf : P f) : Q f' :=
letI := isLocal_affineProperty P
of_targetAffineLocally_of_isPullback h (eq_targetAffineLocally (P := P) ▸ hf)
