Documentation

Mathlib.AlgebraicGeometry.Stalk

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