Residue fields of points #
Any point x
of a locally ringed space X
comes with a natural residue field, namely the residue
field of the stalk at x
. Moreover, for every open subset of X
containing x
, we have a
canonical evaluation map from Γ(X, U)
to the residue field of X
at x
.
Main definitions #
The following are in the AlgebraicGeometry.LocallyRingedSpace
namespace:
residueField
: the residue field of the stalk atx
.evaluation
: for open subsetsU
ofX
containingx
, the evaluation map from sections overU
to the residue field atx
.evaluationMap
: a morphism of locally ringed spaces induces a morphism, i.e. extension, of residue fields.
The residue field of X
at a point x
is the residue field of the stalk of X
at x
.
Equations
- X.residueField x = CommRingCat.of (LocalRing.ResidueField ↑(X.presheaf.stalk x))
Instances For
Equations
- X.instFieldαCommRingResidueField x = inferInstanceAs (Field (LocalRing.ResidueField ↑(X.presheaf.stalk 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
.
Equations
- X.evaluation x = CategoryTheory.CategoryStruct.comp (X.presheaf.germ x) (LocalRing.residue ↑(X.presheaf.stalk ↑x))
Instances For
The global evaluation map from Γ(X, ⊤)
to the residue field at x
.
Equations
- X.Γevaluation x = X.evaluation ⟨x, ⋯⟩
Instances For
If X ⟶ Y
is a morphism of locally ringed spaces and x
a point of X
, we obtain
a morphism of residue fields in the other direction.