Documentation

Mathlib.AlgebraicGeometry.ResidueField

Residue fields of points #

Main definitions #

The following are in the AlgebraicGeometry.Scheme namespace:

The residue field of X at a point x is the residue field of the stalk of X at x.

Equations
Instances For

    The residue map from the stalk to the residue field.

    Equations
    Instances For

      See AlgebraicGeometry.IsClosedImmersion.Spec_map_residue for the stronger result that Spec.map (X.residue x) is a closed immersion.

      If K is a field and f : 𝒪_{X, x} ⟶ K is a ring map, then this is the induced map κ(x) ⟶ K.

      Equations
      Instances For

        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
        Instances For
          @[reducible, inline]

          The global evaluation map from Γ(X, ⊤) to the residue field at x.

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

            Equations
            Instances For

              The isomorphism between residue fields of equal points.

              Equations
              Instances For

                For a field K and a scheme X, the morphisms Spec K ⟶ X bijectively correspond to pairs of points x of X and embeddings κ(x) ⟶ K.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For