English
If P is local at the source and extended to the target with an additional RespectsRight for open immersions, then P(f) holds exactly when for every point x ∈ X there exist opens U ⊂ Y and V ⊂ X with x ∈ V and a map e: V ≤ f^{-1}(U) such that P(f.resLE U V e).
Русский
Если P локально по источнику и сохраняется при ограничении справа открытыми вложениями, то P(f) эквивалентно существованию для каждой точки x ∈ X локальных открытых U ⊂ Y и V ⊂ X с x ∈ V и отображением e: V ≤ f^{-1}(U) так, что P(f.resLE U V e).
LaTeX
$$$[IsZariskiLocalAtSource P] [P.IsMultiplicative] [P.RespectsRight @\mathrm{IsOpenImmersion}] \Rightarrow P f \iff \forall x:\ X, \exists U\subset Y, V\subset X, x\in V, (e: V \le f^{-1} U), P (f.no)$.$$
Lean4
/-- If `P` is local at the source, local at the target and is stable under post-composition with
open immersions, then `P` can be checked locally around points. -/
theorem iff_exists_resLE [IsZariskiLocalAtTarget P] [P.RespectsRight @IsOpenImmersion] :
P f ↔ ∀ x : X, ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.1) (e : V ≤ f ⁻¹ᵁ U), P (f.resLE U V e) :=
by
refine ⟨fun hf x ↦ ⟨⊤, ⊤, trivial, by simp, resLE _ hf⟩, fun hf ↦ ?_⟩
choose U V hxU e hf using hf
rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (fun x : X ↦ V x) (P := P)]
· intro x
rw [← Scheme.Hom.resLE_comp_ι _ (e x)]
exact MorphismProperty.RespectsRight.postcomp (Q := @IsOpenImmersion) _ inferInstance _ (hf x)
· rw [eq_top_iff]
rintro x -
simp only [Opens.coe_iSup, Set.mem_iUnion, SetLike.mem_coe]
use x, hxU x
