evaluation — Mathlib

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 _

Похожие утверждения