Documentation

Mathlib.AlgebraicGeometry.Limits

(Co)Limits of Schemes #

We construct various limits and colimits in the category of schemes.

Todo #

Spec ℤ is the terminal object in the category of schemes.

Instances For

    The map from the empty scheme.

    Instances For

      The empty scheme is the initial object in the category of schemes.

      Instances For

        A scheme is initial if its underlying space is empty .

        Instances For

          Spec 0 is the initial object in the category of schemes.

          Instances For
            instance AlgebraicGeometry.initial_isEmpty :
            IsEmpty (⊥_ AlgebraicGeometry.Scheme).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace