Mathlib Phrasebook

18.5. Stalks, residue fields and fibres🔗

To get acquainted with the scheme API, let us consider an example: Let us define the fibre of a morphism of schemes.

variable {X Y : Scheme} (f : X ⟶ Y)

The stalk 𝒪_Y,y of 𝒪_Y at the point y.

example (y : Y) : CommRingCat := Y.presheaf.stalk y

The stalk 𝒪_Y,y is a local ring.

LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf Y.toLocallyRingedSpace#synth ∀ y, IsLocalRing (Y.presheaf.stalk y)

And we may consider its residue field.

example (y : Y) : Type := IsLocalRing.ResidueField (Y.presheaf.stalk y)

The morphism Spec κ(y) ⟶ Y.

example (y : Y) : Spec (Y.residueField y) ⟶ Y := Y.fromSpecResidueField y

The fibre of f over y is, by definition, the fibre product

X ×[Y] Spec κ(y) ------> Spec κ(y)
      |                       |
      |                       |
      v                       |
      X --------------------> Y
def fiber (y : Y) : Scheme := pullback f (Y.fromSpecResidueField y)

The immersion X ×[Y] Spec κ(y) ⟶ X:

def fiberι (y : Y) : fiber f y ⟶ X := pullback.fst f (Y.fromSpecResidueField y)

The projection X ×[Y] Spec κ(y) ⟶ Spec κ(y).

def fiberToSpecResidueField (y : Y) : fiber f y ⟶ Spec (Y.residueField y) := pullback.snd f (Y.fromSpecResidueField y)

In Mathlib these are called Scheme.Hom.fiber, Scheme.Hom.fiberι and Scheme.Hom.fiberToSpecResidueField and we can for example write f.fiber.