residueField — Mathlib

English

There is a canonical evaluation map from global sections to residue fields, interpreting a global section as a function on the space and evaluating at a point.

Русский

Существует каноническое отображение оценки от глобальных секций к остаточным полям, тождественно трактующее глобальную секцию как функцию на пространстве и вычисляющее её в точке.

LaTeX

$$Γevaluation (x) : Γ(X, O_X) → κ(x)$$

Lean4

/-- The residue field of `X` at a point `x` is the residue field of the stalk of `X`
at `x`. -/
def residueField (x : X) : CommRingCat :=
  CommRingCat.of <| IsLocalRing.ResidueField (X.presheaf.stalk x)

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