Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.evaluation

(X : AlgebraicGeometry.Scheme) → (U : X.Opens) → (x : ↥X) → x ∈ U → (X.presheaf.obj (Opposite.op U) ⟶ X.residueField x)

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.

Defined in

Mathlib.AlgebraicGeometry.ResidueField

Cited by

9 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound