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.

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

    The map from the empty scheme.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem AlgebraicGeometry.Scheme.emptyTo_val_base_apply (X : AlgebraicGeometry.Scheme) (x : .toPresheafedSpace) :
      X.emptyTo.val.base x = PEmpty.elim x
      @[simp]
      theorem AlgebraicGeometry.Scheme.emptyTo_val_c_app (X : AlgebraicGeometry.Scheme) (U : (TopologicalSpace.Opens X.toPresheafedSpace)ᵒᵖ) :
      X.emptyTo.val.c.app U = CommRingCat.punitIsTerminal.from (X.presheaf.obj U)
      Equations
      • X.hom_unique_of_empty_source = { default := X.emptyTo, uniq := }

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

      Equations
      Instances For
        @[instance 100]
        Equations
        • =
        @[instance 100]
        noncomputable instance AlgebraicGeometry.isIso_of_isEmpty {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) [IsEmpty Y.toPresheafedSpace] :
        Equations
        • =

        A scheme is initial if its underlying space is empty .

        Equations
        Instances For

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[instance 100]
            noncomputable instance AlgebraicGeometry.isAffine_of_isEmpty {X : AlgebraicGeometry.Scheme} [IsEmpty X.toPresheafedSpace] :
            Equations
            • =