Documentation

Mathlib.AlgebraicGeometry.Scheme

The category of schemes #

A scheme is a locally ringed space such that every point is contained in some open set where there is an isomorphism of presheaves between the restriction to that open set, and the structure sheaf of Spec R, for some commutative ring R.

A morphism of schemes is just a morphism of the underlying locally ringed spaces.

We define Scheme as an X : LocallyRingedSpace, along with a proof that every point has an open neighbourhood U so that that the restriction of X to U is isomorphic, as a locally ringed space, to Spec.toLocallyRingedSpace.obj (op R) for some R : CommRingCat.

Instances For

    A morphism between schemes is a morphism between the underlying locally ringed spaces.

    Instances For
      @[inline, reducible]

      The structure sheaf of a scheme.

      Instances For

        forgetful functor to TopCat is the same as coercion

        Instances For
          @[simp]
          theorem AlgebraicGeometry.Scheme.id_app {X : AlgebraicGeometry.Scheme} (U : (TopologicalSpace.Opens X.toPresheafedSpace)ᵒᵖ) :
          (CategoryTheory.CategoryStruct.id X).val.c.app U = X.presheaf.map (CategoryTheory.eqToHom (_ : U = U))
          theorem AlgebraicGeometry.Scheme.comp_val_base_apply {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X Y) (g : Y Z) (x : X.toPresheafedSpace) :
          (CategoryTheory.CategoryStruct.comp f g).val.base x = g.val.base (f.val.base x)
          @[simp]
          theorem AlgebraicGeometry.Scheme.comp_val_c_app {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X Y) (g : Y Z) (U : (TopologicalSpace.Opens Z.toPresheafedSpace)ᵒᵖ) :
          (CategoryTheory.CategoryStruct.comp f g).val.c.app U = CategoryTheory.CategoryStruct.comp (g.val.c.app U) (f.val.c.app ((TopologicalSpace.Opens.map g.val.base).op.obj U))
          theorem AlgebraicGeometry.Scheme.congr_app {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X Y} {g : X Y} (e : f = g) (U : (TopologicalSpace.Opens Y.toPresheafedSpace)ᵒᵖ) :
          f.val.c.app U = CategoryTheory.CategoryStruct.comp (g.val.c.app U) (X.presheaf.map (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map g.val.base).op.obj U = (TopologicalSpace.Opens.map f.val.base).op.obj U)))
          theorem AlgebraicGeometry.Scheme.app_eq {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) {U : TopologicalSpace.Opens Y.toPresheafedSpace} {V : TopologicalSpace.Opens Y.toPresheafedSpace} (e : U = V) :
          f.val.c.app (Opposite.op U) = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom (_ : V = U)).op) (CategoryTheory.CategoryStruct.comp (f.val.c.app (Opposite.op V)) (X.presheaf.map (CategoryTheory.eqToHom (_ : (TopologicalSpace.Opens.map f.val.base).obj U = (TopologicalSpace.Opens.map f.val.base).obj V)).op))
          theorem AlgebraicGeometry.Scheme.presheaf_map_eqToHom_op (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens X.toPresheafedSpace) (V : TopologicalSpace.Opens X.toPresheafedSpace) (i : U = V) :
          X.presheaf.map (CategoryTheory.eqToHom i).op = CategoryTheory.eqToHom (_ : X.presheaf.obj (Opposite.op V) = X.presheaf.obj (Opposite.op U))
          @[inline, reducible]
          abbrev AlgebraicGeometry.Scheme.Hom.appLe {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) {V : TopologicalSpace.Opens X.toPresheafedSpace} {U : TopologicalSpace.Opens Y.toPresheafedSpace} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) :
          Y.presheaf.obj (Opposite.op U) X.presheaf.obj (Opposite.op V)

          Given a morphism of schemes f : X ⟶ Y, and open sets U ⊆ Y, V ⊆ f ⁻¹' U, this is the induced map Γ(Y, U) ⟶ Γ(X, V).

          Instances For

            The spectrum of a commutative ring, as a scheme.

            Instances For

              The induced map of a ring homomorphism on the ring spectra, as a morphism of schemes.

              Instances For

                The spectrum, as a contravariant functor from commutative rings to schemes.

                Instances For
                  def AlgebraicGeometry.Scheme.basicOpen (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) :
                  TopologicalSpace.Opens X.toPresheafedSpace

                  The subset of the underlying space where the given section does not vanish.

                  Instances For
                    @[simp]
                    theorem AlgebraicGeometry.Scheme.mem_basicOpen (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) (x : { x // x U }) :
                    theorem AlgebraicGeometry.Scheme.mem_basicOpen_top' (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) (x : X.toPresheafedSpace) :
                    x AlgebraicGeometry.Scheme.basicOpen X f m, IsUnit (↑(TopCat.Presheaf.germ X.presheaf { val := x, property := m }) f)
                    @[simp]
                    theorem AlgebraicGeometry.Scheme.mem_basicOpen_top (X : AlgebraicGeometry.Scheme) (f : ↑(X.presheaf.obj (Opposite.op ))) (x : X.toPresheafedSpace) :
                    x AlgebraicGeometry.Scheme.basicOpen X f IsUnit (↑(TopCat.Presheaf.germ X.presheaf { val := x, property := trivial }) f)
                    @[simp]
                    theorem AlgebraicGeometry.Scheme.basicOpen_res (X : AlgebraicGeometry.Scheme) {V : TopologicalSpace.Opens X.toPresheafedSpace} {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) (i : Opposite.op U Opposite.op V) :
                    @[simp]
                    theorem AlgebraicGeometry.Scheme.basicOpen_res_eq (X : AlgebraicGeometry.Scheme) {V : TopologicalSpace.Opens X.toPresheafedSpace} {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : ↑(X.presheaf.obj (Opposite.op U))) (i : Opposite.op U Opposite.op V) [CategoryTheory.IsIso i] :
                    @[simp]