English
Let P be a morphism-property of schemes that is local on the source (Zariski-local on the source). Then P is preserved when precomposing with an open immersion on the left: if P holds for f: X → Y and i: U → X is an open immersion, then P holds for i ≫ f.
Русский
Пусть P — свойство морфизмов между схемами, локальное по источнику (Zariski-локальное по источнику). Тогда оно сохраняется при левом композиционном оборачивании открытым вложением: если P(f) выполнено для f: X → Y и i: U → X открытое вложение, то P(i ≫ f).
LaTeX
$$$\forall {P : \mathrm{MorphismProperty}(\mathrm{Scheme})} [\mathrm{IsZariskiLocalAtSource} P],\; \forall X,Y : \mathrm{Scheme}, \forall f : X \to Y, \forall UX : \mathrm{Scheme}, \forall i : UX \to X, [\mathrm{IsOpenImmersion} i],\\ P f \Rightarrow P (i \circ f).$$$$
Lean4
theorem comp {UX : Scheme.{u}} (H : P f) (i : UX ⟶ X) [IsOpenImmersion i] : P (i ≫ f) :=
(P.iff_of_zeroHypercover_source (X.affineCover.add i)).mp H .none
