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

    Equations
    • X.Hom Y = (X.toLocallyRingedSpace Y.toLocallyRingedSpace)
    Instances For

      Schemes are a full subcategory of locally ringed spaces.

      Equations
      • One or more equations did not get rendered due to their size.
      @[reducible, inline]

      The structure sheaf of a scheme.

      Equations
      • X.sheaf = X.sheaf
      Instances For

        forgetful functor to TopCat is the same as coercion

        Equations
        Instances For
          @[simp]
          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 ))
          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 { unop := U } = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom ).op) (CategoryTheory.CategoryStruct.comp (f.val.c.app { unop := V }) (X.presheaf.map (CategoryTheory.eqToHom ).op))
          theorem AlgebraicGeometry.Scheme.presheaf_map_eqToHom_op (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens X.toPresheafedSpace) (V : TopologicalSpace.Opens X.toPresheafedSpace) (i : U = V) :
          @[simp]
          theorem AlgebraicGeometry.Scheme.inv_val_c_app {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) [CategoryTheory.IsIso f] (U : TopologicalSpace.Opens X.toPresheafedSpace) :
          (CategoryTheory.inv f).val.c.app { unop := U } = CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom ).op) (CategoryTheory.inv (f.val.c.app { unop := (TopologicalSpace.Opens.map (CategoryTheory.inv f).val.base).obj U }))
          @[reducible, inline]
          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 { unop := U } X.presheaf.obj { unop := 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).

          Equations
          Instances For

            The spectrum of a commutative ring, as a scheme.

            Equations
            Instances For

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

              Equations
              Instances For

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

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

                  The empty scheme.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem AlgebraicGeometry.Scheme.Γ_obj_op (X : AlgebraicGeometry.Scheme) :
                    AlgebraicGeometry.Scheme.Γ.obj { unop := X } = X.presheaf.obj { unop := }
                    def AlgebraicGeometry.Scheme.basicOpen (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : (X.presheaf.obj { unop := U })) :
                    TopologicalSpace.Opens X.toPresheafedSpace

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

                    Equations
                    • X.basicOpen f = X.toRingedSpace.basicOpen f
                    Instances For
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.mem_basicOpen (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : (X.presheaf.obj { unop := U })) (x : U) :
                      x X.basicOpen f IsUnit ((X.presheaf.germ x) f)
                      theorem AlgebraicGeometry.Scheme.mem_basicOpen_top' (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : (X.presheaf.obj { unop := U })) (x : X.toPresheafedSpace) :
                      x X.basicOpen f ∃ (m : x U), IsUnit ((X.presheaf.germ x, m) f)
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.mem_basicOpen_top (X : AlgebraicGeometry.Scheme) (f : (X.presheaf.obj { unop := })) (x : X.toPresheafedSpace) :
                      x X.basicOpen f IsUnit ((X.presheaf.germ x, 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 { unop := U })) (i : { unop := U } { unop := V }) :
                      X.basicOpen ((X.presheaf.map i) f) = V X.basicOpen f
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.basicOpen_res_eq (X : AlgebraicGeometry.Scheme) {V : TopologicalSpace.Opens X.toPresheafedSpace} {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : (X.presheaf.obj { unop := U })) (i : { unop := U } { unop := V }) [CategoryTheory.IsIso i] :
                      X.basicOpen ((X.presheaf.map i) f) = X.basicOpen f
                      theorem AlgebraicGeometry.Scheme.basicOpen_le (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : (X.presheaf.obj { unop := U })) :
                      X.basicOpen f U
                      theorem AlgebraicGeometry.Scheme.basicOpen_restrict (X : AlgebraicGeometry.Scheme) {V : TopologicalSpace.Opens X.toPresheafedSpace} {U : TopologicalSpace.Opens X.toPresheafedSpace} (i : V U) (f : (X.presheaf.obj { unop := U })) :
                      X.basicOpen (TopCat.Presheaf.restrict f i) X.basicOpen f
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.preimage_basicOpen {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) {U : TopologicalSpace.Opens Y.toPresheafedSpace} (r : (Y.presheaf.obj { unop := U })) :
                      (TopologicalSpace.Opens.map f.val.base).obj (Y.basicOpen r) = X.basicOpen ((f.val.c.app { unop := U }) r)
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.basicOpen_zero (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens X.toPresheafedSpace) :
                      X.basicOpen 0 =
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.basicOpen_mul (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : (X.presheaf.obj { unop := U })) (g : (X.presheaf.obj { unop := U })) :
                      X.basicOpen (f * g) = X.basicOpen f X.basicOpen g
                      theorem AlgebraicGeometry.Scheme.basicOpen_of_isUnit (X : AlgebraicGeometry.Scheme) {U : TopologicalSpace.Opens X.toPresheafedSpace} {f : (X.presheaf.obj { unop := U })} (hf : IsUnit f) :
                      X.basicOpen f = U
                      instance AlgebraicGeometry.Scheme.algebra_section_section_basicOpen {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : (X.presheaf.obj { unop := U })) :
                      Algebra (X.presheaf.obj { unop := U }) (X.presheaf.obj { unop := X.basicOpen f })
                      Equations
                      @[simp]
                      theorem AlgebraicGeometry.basicOpen_eq_of_affine' {R : CommRingCat} (f : ((AlgebraicGeometry.Spec.toSheafedSpace.obj { unop := R }).presheaf.obj { unop := })) :
                      theorem AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} (h : U = V) (W : (TopologicalSpace.Opens (AlgebraicGeometry.Scheme.Spec.obj { unop := X.presheaf.obj { unop := V } }).toPresheafedSpace)ᵒᵖ) :
                      (AlgebraicGeometry.Scheme.Spec.map (X.presheaf.map (CategoryTheory.eqToHom h).op).op).val.c.app W = CategoryTheory.eqToHom