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
    @[reducible, inline]

    The type of open sets of a scheme.

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

        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

          Pretty printer defined by notation3 command.

          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 : Y.Opens) :
                  Y.presheaf.obj (Opposite.op U) X.presheaf.obj (Opposite.op ((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
                  Instances For
                    theorem AlgebraicGeometry.Scheme.Hom.naturality_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : Y.Opens} {U' : Y.Opens} (i : Opposite.op U' Opposite.op U) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op ((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 : Y.Opens} {U' : Y.Opens} (i : Opposite.op U' Opposite.op 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 : Y.Opens) (V : X.Opens) (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).

                    Equations
                    Instances For
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.Hom.appLE_map_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : Y.Opens} {V : X.Opens} {V' : X.Opens} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (i : Opposite.op V Opposite.op V') {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op V') Z) :
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.Hom.appLE_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : Y.Opens} {V : X.Opens} {V' : X.Opens} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (i : Opposite.op V Opposite.op 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 : Y.Opens} {V : X.Opens} {V' : X.Opens} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (i : V = V') {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op V) Z) :
                      theorem AlgebraicGeometry.Scheme.Hom.appLE_map' {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : Y.Opens} {V : X.Opens} {V' : X.Opens} (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 : Y.Opens} {U' : Y.Opens} {V : X.Opens} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (i : Opposite.op U' Opposite.op U) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op V) Z) :
                      @[simp]
                      theorem AlgebraicGeometry.Scheme.Hom.map_appLE {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : Y.Opens} {U' : Y.Opens} {V : X.Opens} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (i : Opposite.op U' Opposite.op 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 : Y.Opens} {U' : Y.Opens} {V : X.Opens} (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (i : U' = U) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op V) Z) :
                      theorem AlgebraicGeometry.Scheme.Hom.map_appLE' {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : Y.Opens} {U' : Y.Opens} {V : X.Opens} (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 : Y.Opens} :
                      f.app U = f.appLE U ((TopologicalSpace.Opens.map f.val.base).obj U)
                      theorem AlgebraicGeometry.Scheme.Hom.appLE_eq_app {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : Y.Opens} :
                      f.appLE U ((TopologicalSpace.Opens.map f.val.base).obj U) = f.app U
                      theorem AlgebraicGeometry.Scheme.Hom.appLE_congr {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {U : Y.Opens} {U' : Y.Opens} {V : X.Opens} {V' : X.Opens} (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' )
                      noncomputable def AlgebraicGeometry.Scheme.Hom.homeomorph {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [CategoryTheory.IsIso f] :
                      X.toPresheafedSpace ≃ₜ Y.toPresheafedSpace

                      An isomorphism of schemes induces a homeomorphism of the underlying topological spaces.

                      Equations
                      Instances For
                        theorem AlgebraicGeometry.Scheme.Hom.ext {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X Y} {g : X Y} (h_base : f.val.base = g.val.base) (h_app : ∀ (U : Y.Opens), CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U) (X.presheaf.map (CategoryTheory.eqToHom ).op) = AlgebraicGeometry.Scheme.Hom.app g U) :
                        f = g
                        theorem AlgebraicGeometry.Scheme.Hom.preimage_iSup {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {ι : Sort u_1} (U : ιY.Opens) :
                        (TopologicalSpace.Opens.map f.val.base).obj (iSup U) = ⨆ (i : ι), (TopologicalSpace.Opens.map f.val.base).obj (U i)
                        theorem AlgebraicGeometry.Scheme.Hom.preimage_iSup_eq_top {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {ι : Sort u_1} {U : ιY.Opens} (hU : iSup U = ) :
                        ⨆ (i : ι), (TopologicalSpace.Opens.map f.val.base).obj (U i) =

                        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 : X.Opens) (V : X.Opens) (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

                                  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 : X.Opens} (f : (X.presheaf.obj (Opposite.op U))) :
                                      X.Opens

                                      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 : X.Opens} (f : (X.presheaf.obj (Opposite.op U))) (x : U) :
                                        x X.basicOpen f IsUnit ((X.presheaf.germ x) f)
                                        theorem AlgebraicGeometry.Scheme.mem_basicOpen_top' (X : AlgebraicGeometry.Scheme) {U : X.Opens} (f : (X.presheaf.obj (Opposite.op 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 (Opposite.op ))) (x : X.toPresheafedSpace) :
                                        x X.basicOpen f IsUnit ((X.presheaf.germ x, trivial) f)
                                        @[simp]
                                        theorem AlgebraicGeometry.Scheme.basicOpen_res (X : AlgebraicGeometry.Scheme) {V : X.Opens} {U : X.Opens} (f : (X.presheaf.obj (Opposite.op U))) (i : Opposite.op U Opposite.op V) :
                                        X.basicOpen ((X.presheaf.map i) f) = V X.basicOpen f
                                        @[simp]
                                        theorem AlgebraicGeometry.Scheme.basicOpen_res_eq (X : AlgebraicGeometry.Scheme) {V : X.Opens} {U : X.Opens} (f : (X.presheaf.obj (Opposite.op U))) (i : Opposite.op U Opposite.op V) [CategoryTheory.IsIso i] :
                                        X.basicOpen ((X.presheaf.map i) f) = X.basicOpen f
                                        theorem AlgebraicGeometry.Scheme.basicOpen_le (X : AlgebraicGeometry.Scheme) {U : X.Opens} (f : (X.presheaf.obj (Opposite.op U))) :
                                        X.basicOpen f U
                                        theorem AlgebraicGeometry.Scheme.basicOpen_restrict (X : AlgebraicGeometry.Scheme) {V : X.Opens} {U : X.Opens} (i : V U) (f : (X.presheaf.obj (Opposite.op 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 : Y.Opens} (r : (Y.presheaf.obj (Opposite.op U))) :
                                        (TopologicalSpace.Opens.map f.val.base).obj (Y.basicOpen r) = X.basicOpen ((AlgebraicGeometry.Scheme.Hom.app f U) r)
                                        theorem AlgebraicGeometry.Scheme.basicOpen_appLE {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) (U : X.Opens) (V : Y.Opens) (e : U (TopologicalSpace.Opens.map f.val.base).obj V) (s : (Y.presheaf.obj (Opposite.op V))) :
                                        X.basicOpen ((AlgebraicGeometry.Scheme.Hom.appLE f V U e) s) = U (TopologicalSpace.Opens.map f.val.base).obj (Y.basicOpen s)
                                        @[simp]
                                        theorem AlgebraicGeometry.Scheme.basicOpen_zero (X : AlgebraicGeometry.Scheme) (U : X.Opens) :
                                        X.basicOpen 0 =
                                        @[simp]
                                        theorem AlgebraicGeometry.Scheme.basicOpen_mul (X : AlgebraicGeometry.Scheme) {U : X.Opens} (f : (X.presheaf.obj (Opposite.op U))) (g : (X.presheaf.obj (Opposite.op U))) :
                                        X.basicOpen (f * g) = X.basicOpen f X.basicOpen g
                                        theorem AlgebraicGeometry.Scheme.basicOpen_pow (X : AlgebraicGeometry.Scheme) {U : X.Opens} (f : (X.presheaf.obj (Opposite.op U))) {n : } (h : 0 < n) :
                                        X.basicOpen (f ^ n) = X.basicOpen f
                                        theorem AlgebraicGeometry.Scheme.basicOpen_of_isUnit (X : AlgebraicGeometry.Scheme) {U : X.Opens} {f : (X.presheaf.obj (Opposite.op U))} (hf : IsUnit f) :
                                        X.basicOpen f = U
                                        instance AlgebraicGeometry.Scheme.algebra_section_section_basicOpen {X : AlgebraicGeometry.Scheme} {U : X.Opens} (f : (X.presheaf.obj (Opposite.op U))) :
                                        Algebra (X.presheaf.obj (Opposite.op U)) (X.presheaf.obj (Opposite.op (X.basicOpen f)))
                                        Equations
                                        def AlgebraicGeometry.Scheme.zeroLocus (X : AlgebraicGeometry.Scheme) {U : X.Opens} (s : Set (X.presheaf.obj (Opposite.op U))) :
                                        Set X.toPresheafedSpace

                                        The zero locus of a set of sections s over an open set U is the closed set consisting of the complement of U and of all points of U, where all elements of f vanish.

                                        Equations
                                        • X.zeroLocus s = X.toRingedSpace.zeroLocus s
                                        Instances For
                                          theorem AlgebraicGeometry.Scheme.zeroLocus_def (X : AlgebraicGeometry.Scheme) {U : X.Opens} (s : Set (X.presheaf.obj (Opposite.op U))) :
                                          X.zeroLocus s = fs, (X.basicOpen f).carrier
                                          theorem AlgebraicGeometry.Scheme.zeroLocus_isClosed (X : AlgebraicGeometry.Scheme) {U : X.Opens} (s : Set (X.presheaf.obj (Opposite.op U))) :
                                          IsClosed (X.zeroLocus s)
                                          theorem AlgebraicGeometry.Scheme.zeroLocus_singleton (X : AlgebraicGeometry.Scheme) {U : X.Opens} (f : (X.presheaf.obj (Opposite.op U))) :
                                          X.zeroLocus {f} = (X.basicOpen f).carrier
                                          @[simp]
                                          theorem AlgebraicGeometry.Scheme.zeroLocus_empty_eq_univ (X : AlgebraicGeometry.Scheme) {U : X.Opens} :
                                          X.zeroLocus = Set.univ
                                          @[simp]
                                          theorem AlgebraicGeometry.Scheme.mem_zeroLocus_iff (X : AlgebraicGeometry.Scheme) {U : X.Opens} (s : Set (X.presheaf.obj (Opposite.op U))) (x : X.toPresheafedSpace) :
                                          x X.zeroLocus s fs, xX.basicOpen f