English
The evaluation at x is zero precisely when x is not in the basic open of f.
Русский
Значение оценки в точке x равно нулю тогда и только тогда, когда x не лежит в базовом открытом множестve f.
LaTeX
$$$$ X.\mathrm{evaluation}(U, x, hx, f) = 0 \iff x \notin X.\mathrm{basicOpen}(f). $$$$
Lean4
/-- If `U` is an open of `X` containing `x`, we have a canonical ring map from the sections
over `U` to the residue field of `x`.
If we interpret sections over `U` as functions of `X` defined on `U`, then this ring map
corresponds to evaluation at `x`.
-/
def evaluation (U : X.Opens) (x : X) (hx : x ∈ U) : Γ(X, U) ⟶ X.residueField x :=
X.presheaf.germ U x hx ≫ X.residue _