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.

      Pretty printer defined by notation3 command.

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

        f ⁻¹ᵁ U is notation for (Opens.map f.1.base).obj U, the preimage of an open set U under f.

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

          Γ(X, U) is notation for X.presheaf.obj (op U).

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

            Pretty printer defined by notation3 command.

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

              The structure sheaf of a scheme.

              Equations
              • X.sheaf = X.sheaf
              Instances For
                @[reducible, inline]
                abbrev AlgebraicGeometry.Scheme.Hom.app {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) (U : TopologicalSpace.Opens Y.toPresheafedSpace) :
                Y.presheaf.obj { unop := U } X.presheaf.obj { unop := (TopologicalSpace.Opens.map f.val.base).obj U }

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

                Equations
                • f.app U = f.val.c.app { unop := U }
                Instances For
                  theorem AlgebraicGeometry.Scheme.Hom.naturality_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : TopologicalSpace.Opens Y.toPresheafedSpace} {U' : TopologicalSpace.Opens Y.toPresheafedSpace} (i : { unop := U' } { unop := U }) {Z : CommRingCat} (h : X.presheaf.obj { unop := (TopologicalSpace.Opens.map f.val.base).obj U } Z) :
                  theorem AlgebraicGeometry.Scheme.Hom.naturality {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : TopologicalSpace.Opens Y.toPresheafedSpace} {U' : TopologicalSpace.Opens Y.toPresheafedSpace} (i : { unop := U' } { unop := U }) :
                  CategoryTheory.CategoryStruct.comp (Y.presheaf.map i) (f.app U) = CategoryTheory.CategoryStruct.comp (f.app U') (X.presheaf.map ((TopologicalSpace.Opens.map f.val.base).map i.unop).op)
                  def AlgebraicGeometry.Scheme.Hom.appLE {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) (U : TopologicalSpace.Opens Y.toPresheafedSpace) (V : TopologicalSpace.Opens X.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
                    @[simp]
                    theorem AlgebraicGeometry.Scheme.Hom.appLE_map_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : TopologicalSpace.Opens Y.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} {V' : TopologicalSpace.Opens X.toPresheafedSpace} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (i : { unop := V } { unop := V' }) {Z : CommRingCat} (h : X.presheaf.obj { unop := V' } Z) :
                    @[simp]
                    theorem AlgebraicGeometry.Scheme.Hom.appLE_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : TopologicalSpace.Opens Y.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} {V' : TopologicalSpace.Opens X.toPresheafedSpace} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (i : { unop := V } { unop := V' }) :
                    CategoryTheory.CategoryStruct.comp (f.appLE U V e) (X.presheaf.map i) = f.appLE U V'
                    theorem AlgebraicGeometry.Scheme.Hom.appLE_map'_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : TopologicalSpace.Opens Y.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} {V' : TopologicalSpace.Opens X.toPresheafedSpace} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (i : V = V') {Z : CommRingCat} (h : X.presheaf.obj { unop := V } Z) :
                    theorem AlgebraicGeometry.Scheme.Hom.appLE_map' {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : TopologicalSpace.Opens Y.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} {V' : TopologicalSpace.Opens X.toPresheafedSpace} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (i : V = V') :
                    CategoryTheory.CategoryStruct.comp (f.appLE U V' ) (X.presheaf.map (CategoryTheory.eqToHom i).op) = f.appLE U V e
                    @[simp]
                    theorem AlgebraicGeometry.Scheme.Hom.map_appLE_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : TopologicalSpace.Opens Y.toPresheafedSpace} {U' : TopologicalSpace.Opens Y.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (i : { unop := U' } { unop := U }) {Z : CommRingCat} (h : X.presheaf.obj { unop := V } Z) :
                    @[simp]
                    theorem AlgebraicGeometry.Scheme.Hom.map_appLE {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : TopologicalSpace.Opens Y.toPresheafedSpace} {U' : TopologicalSpace.Opens Y.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (i : { unop := U' } { unop := U }) :
                    CategoryTheory.CategoryStruct.comp (Y.presheaf.map i) (f.appLE U V e) = f.appLE U' V
                    theorem AlgebraicGeometry.Scheme.Hom.map_appLE'_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : TopologicalSpace.Opens Y.toPresheafedSpace} {U' : TopologicalSpace.Opens Y.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (i : U' = U) {Z : CommRingCat} (h : X.presheaf.obj { unop := V } Z) :
                    theorem AlgebraicGeometry.Scheme.Hom.map_appLE' {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : TopologicalSpace.Opens Y.toPresheafedSpace} {U' : TopologicalSpace.Opens Y.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (i : U' = U) :
                    CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom i).op) (f.appLE U' V ) = f.appLE U V e
                    theorem AlgebraicGeometry.Scheme.Hom.app_eq_appLE {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : TopologicalSpace.Opens Y.toPresheafedSpace} :
                    f.app U = f.appLE U ((TopologicalSpace.Opens.map f.val.base).obj U)
                    theorem AlgebraicGeometry.Scheme.Hom.appLE_congr {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : TopologicalSpace.Opens Y.toPresheafedSpace} {U' : TopologicalSpace.Opens Y.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} {V' : TopologicalSpace.Opens X.toPresheafedSpace} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (e₁ : U = U') (e₂ : V = V') (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop) :
                    P (f.appLE U V e) P (f.appLE U' V' )

                    forgetful functor to TopCat is the same as coercion

                    Equations
                    Instances For
                      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)
                      theorem AlgebraicGeometry.Scheme.presheaf_map_eqToHom_op (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens X.toPresheafedSpace) (V : TopologicalSpace.Opens X.toPresheafedSpace) (i : U = V) :

                      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 := }

                              The counit (SpecΓIdentity.inv.op) of the adjunction ΓSpec as an isomorphism. This is almost never needed in practical use cases. Use ΓSpecIso instead.

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

                                The global sections of Spec R is isomorphic to R.

                                Equations
                                Instances For
                                  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 ((AlgebraicGeometry.Scheme.Hom.app f 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
                                    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.Spec (X.presheaf.obj { unop := V })).toPresheafedSpace) :