English
Over an affine basic open, a global section x that vanishes on that basic open becomes nilpotent after multiplying by a suitable power of the local function f.
Русский
На AFFINE-базовом открытом множестве выполнено: секция x, обращённая на базовый открытый D(f), нулируется; затем существует n, такое что f^n x = 0.
LaTeX
$$$\\exists n:\\mathbb{N}, f^{n} \\cdot x = 0$ under the given vanishing condition$$
Lean4
theorem exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen (X : Scheme) {U : X.Opens} (hU : IsAffineOpen U)
(x f : Γ(X, U)) (H : x |_ (X.basicOpen f) = 0) : ∃ n : ℕ, f ^ n * x = 0 :=
by
rw [← map_zero (X.presheaf.map (homOfLE <| X.basicOpen_le f : X.basicOpen f ⟶ U).op).hom] at H
obtain ⟨n, e⟩ := (hU.isLocalization_basicOpen f).exists_of_eq _ H
exact ⟨n, by simpa [mul_comm x] using e⟩
