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.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

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.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 ⋯

@[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