Stalks of a Scheme #
Given a scheme X
and a point x : X
, AlgebraicGeometry.Scheme.fromSpecStalk X x
is the
canonical scheme morphism from Spec(O_x)
to X
. This is helpful for constructing the canonical
map from the spectrum of the residue field of a point to the original scheme.
noncomputable def
AlgebraicGeometry.IsAffineOpen.fromSpecStalk
{X : AlgebraicGeometry.Scheme}
{U : X.Opens}
(hU : AlgebraicGeometry.IsAffineOpen U)
{x : ↑↑X.toPresheafedSpace}
(hxU : x ∈ U)
:
AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ X
A morphism from Spec(O_x)
to X
, which is defined with the help of an affine open
neighborhood U
of x
.
Equations
- hU.fromSpecStalk hxU = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.germ ⟨x, hxU⟩)) hU.fromSpec
Instances For
theorem
AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq
{X : AlgebraicGeometry.Scheme}
(x : ↑↑X.toPresheafedSpace)
{U : X.Opens}
{V : X.Opens}
(hU : AlgebraicGeometry.IsAffineOpen U)
(hV : AlgebraicGeometry.IsAffineOpen V)
(hxU : x ∈ U)
(hxV : x ∈ V)
:
hU.fromSpecStalk hxU = hV.fromSpecStalk hxV
The morphism from Spec(O_x)
to X
given by IsAffineOpen.fromSpec
does not depend on the affine
open neighborhood of x
we choose.
noncomputable def
AlgebraicGeometry.Scheme.fromSpecStalk
(X : AlgebraicGeometry.Scheme)
(x : ↑↑X.toPresheafedSpace)
:
AlgebraicGeometry.Scheme.Spec.obj (Opposite.op (X.presheaf.stalk x)) ⟶ X
If x
is a point of X
, this is the canonical morphism from Spec(O_x)
to X
.
Equations
- X.fromSpecStalk x = ⋯.fromSpecStalk ⋯
Instances For
@[simp]
theorem
AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk
{X : AlgebraicGeometry.Scheme}
{U : X.Opens}
(hU : AlgebraicGeometry.IsAffineOpen U)
{x : ↑↑X.toPresheafedSpace}
(hxU : x ∈ U)
:
hU.fromSpecStalk hxU = X.fromSpecStalk x