Documentation

Mathlib.AlgebraicGeometry.AffineScheme

Affine schemes #

We define the category of AffineSchemes as the essential image of Spec. We also define predicates about affine schemes and affine open sets.

Main definitions #

The category of affine schemes

Equations
Instances For

    A Scheme is affine if the canonical map X ⟶ Spec Γ(X) is an isomorphism.

    Instances

      The canonical isomorphism X ≅ Spec Γ(X) for an affine scheme.

      Equations
      Instances For

        Construct an affine scheme from a scheme and the information that it is affine. Also see AffineScheme.of for a typeclass version.

        Equations
        Instances For

          If f : X ⟶ Y is a morphism between affine schemes, the corresponding arrow is isomorphic to the arrow of the morphism on prime spectra induced by the map on global sections.

          Equations
          Instances For

            The category of affine schemes is equivalent to the category of commutative rings.

            Equations
            Instances For

              An open subset of a scheme is affine if the open subscheme is affine.

              Equations
              Instances For

                The set of affine opens as a subset of opens X.

                Equations
                Instances For
                  Equations
                  • =
                  instance AlgebraicGeometry.Scheme.isAffine_affineBasisCover (X : AlgebraicGeometry.Scheme) (i : X.affineBasisCover.J) :
                  AlgebraicGeometry.IsAffine (X.affineBasisCover.obj i)
                  Equations
                  • =
                  instance AlgebraicGeometry.Scheme.isAffine_affineOpenCover (X : AlgebraicGeometry.Scheme) (𝒰 : X.AffineOpenCover) (i : 𝒰.J) :
                  AlgebraicGeometry.IsAffine (𝒰.openCover.obj i)
                  Equations
                  • =
                  theorem AlgebraicGeometry.iSup_affineOpens_eq_top (X : AlgebraicGeometry.Scheme) :
                  ⨆ (i : X.affineOpens), i =

                  The open immersion Spec Γ(X, U) ⟶ X for an affine U.

                  Equations
                  Instances For
                    @[simp]

                    The affine open sets of an open subscheme corresponds to the affine open sets containing in the image.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def AlgebraicGeometry.affineOpensRestrict {X : AlgebraicGeometry.Scheme} (U : X.Opens) :
                      (U).affineOpens { V : X.affineOpens // V U }

                      The affine open sets of an open subscheme corresponds to the affine open sets containing in the subset.

                      Equations
                      Instances For
                        @[simp]
                        theorem AlgebraicGeometry.affineOpensRestrict_symm_apply_coe {X : AlgebraicGeometry.Scheme} (U : X.Opens) (V : { V : X.affineOpens // V U }) :
                        ((AlgebraicGeometry.affineOpensRestrict U).symm V) = (TopologicalSpace.Opens.map U.val.base).obj V
                        @[instance 100]
                        Equations
                        • =
                        theorem AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen' {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj (Opposite.op U))) :
                        (TopologicalSpace.Opens.map hU.fromSpec.val.base).obj (X.basicOpen f) = (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).basicOpen ((AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv f)
                        theorem AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {V : X.Opens} (x : V) (h : x U) :
                        ∃ (f : (X.presheaf.obj (Opposite.op U))), X.basicOpen f V x X.basicOpen f
                        def AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj (Opposite.op U))) :
                        X.presheaf.obj (Opposite.op (X.basicOpen f)) (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))

                        Given an affine open U and some f : U, this is the canonical map Γ(𝒪ₓ, D(f)) ⟶ Γ(Spec 𝒪ₓ(U), D(f)) This is an isomorphism, as witnessed by an IsIso instance.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          instance AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine_isIso {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj (Opposite.op U))) :
                          CategoryTheory.IsIso (hU.basicOpenSectionsToAffine f)
                          Equations
                          • =
                          theorem AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj (Opposite.op U))) :
                          IsLocalization.Away f (X.presheaf.obj (Opposite.op (X.basicOpen f)))
                          Equations
                          • =
                          theorem AlgebraicGeometry.IsAffineOpen.appLE_eq_away_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {V : X.Opens} (hV : AlgebraicGeometry.IsAffineOpen V) (e : V (TopologicalSpace.Opens.map f.val.base).obj U) (r : (Y.presheaf.obj (Opposite.op U))) :
                          AlgebraicGeometry.Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((AlgebraicGeometry.Scheme.Hom.appLE f U V e) r)) = IsLocalization.Away.map ((Y.presheaf.obj (Opposite.op (Y.basicOpen r)))) ((X.presheaf.obj (Opposite.op (X.basicOpen ((AlgebraicGeometry.Scheme.Hom.appLE f U V e) r))))) (AlgebraicGeometry.Scheme.Hom.appLE f U V e) r
                          theorem AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj (Opposite.op U))) {V : X.Opens} (i : V U) (e : V = X.basicOpen f) :
                          IsLocalization.Away f (X.presheaf.obj (Opposite.op V))
                          instance AlgebraicGeometry.Γ_restrict_isLocalization (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] (r : (X.presheaf.obj (Opposite.op ))) :
                          IsLocalization.Away r (((X.basicOpen r)).presheaf.obj (Opposite.op ))
                          Equations
                          • =
                          theorem AlgebraicGeometry.IsAffineOpen.basicOpen_basicOpen_is_basicOpen {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj (Opposite.op U))) (g : (X.presheaf.obj (Opposite.op (X.basicOpen f)))) :
                          ∃ (f' : (X.presheaf.obj (Opposite.op U))), X.basicOpen f' = X.basicOpen g
                          theorem AlgebraicGeometry.exists_basicOpen_le_affine_inter {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {V : X.Opens} (hV : AlgebraicGeometry.IsAffineOpen V) (x : X.toPresheafedSpace) (hx : x U V) :
                          ∃ (f : (X.presheaf.obj (Opposite.op U))) (g : (X.presheaf.obj (Opposite.op V))), X.basicOpen f = X.basicOpen g x X.basicOpen f
                          noncomputable def AlgebraicGeometry.IsAffineOpen.primeIdealOf {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (x : U) :
                          PrimeSpectrum (X.presheaf.obj (Opposite.op U))

                          The prime ideal of 𝒪ₓ(U) corresponding to a point x : U.

                          Equations
                          Instances For
                            theorem AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (x : U) :
                            hU.fromSpec.val.base (hU.primeIdealOf x) = x
                            theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk' {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (y : PrimeSpectrum (X.presheaf.obj (Opposite.op U))) (hy : hU.fromSpec.val.base y U) :
                            IsLocalization.AtPrime ((X.presheaf.stalk (hU.fromSpec.val.base y))) y.asIdeal
                            theorem AlgebraicGeometry.IsAffineOpen.isLocalization_stalk {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (x : U) :
                            IsLocalization.AtPrime ((X.presheaf.stalk x)) (hU.primeIdealOf x).asIdeal
                            @[simp]
                            theorem AlgebraicGeometry.Scheme.affineBasicOpen_coe (X : AlgebraicGeometry.Scheme) {U : X.affineOpens} (f : (X.presheaf.obj (Opposite.op U))) :
                            (X.affineBasicOpen f) = X.basicOpen f
                            def AlgebraicGeometry.Scheme.affineBasicOpen (X : AlgebraicGeometry.Scheme) {U : X.affineOpens} (f : (X.presheaf.obj (Opposite.op U))) :
                            X.affineOpens

                            The basic open set of a section f on an affine open as an X.affineOpens.

                            Equations
                            • X.affineBasicOpen f = X.basicOpen f,
                            Instances For
                              theorem AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (s : Set (X.presheaf.obj (Opposite.op U))) :
                              ⨆ (f : s), X.basicOpen f = U Ideal.span s =

                              In an affine open set U, a family of basic open covers U iff the sections span Γ(X, U). See iSup_basicOpen_of_span_eq_top for the inverse direction without the affine-ness assuption.

                              theorem AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (s : Set (X.presheaf.obj (Opposite.op U))) :
                              U ⨆ (f : s), X.basicOpen f Ideal.span s =
                              theorem AlgebraicGeometry.iSup_basicOpen_of_span_eq_top {X : AlgebraicGeometry.Scheme} (U : X.Opens) (s : Set (X.presheaf.obj (Opposite.op U))) (hs : Ideal.span s = ) :
                              is, X.basicOpen i = U

                              Given a spanning set of Γ(X, U), the corresponding basic open sets cover U. See IsAffineOpen.basicOpen_union_eq_self_iff for the inverse direction for affine open sets.

                              theorem AlgebraicGeometry.of_affine_open_cover {X : AlgebraicGeometry.Scheme} {P : X.affineOpensProp} {ι : Sort u_2} (U : ιX.affineOpens) (iSup_U : ⨆ (i : ι), (U i) = ) (V : X.affineOpens) (basicOpen : ∀ (U : X.affineOpens) (f : (X.presheaf.obj (Opposite.op U))), P UP (X.affineBasicOpen f)) (openCover : ∀ (U : X.affineOpens) (s : Finset (X.presheaf.obj (Opposite.op U))), Ideal.span s = (∀ (f : { x : (X.presheaf.obj (Opposite.op U)) // x s }), P (X.affineBasicOpen f))P U) (hU : ∀ (i : ι), P (U i)) :
                              P V

                              Let P be a predicate on the affine open sets of X satisfying

                              1. If P holds on U, then P holds on the basic open set of every section on U.
                              2. If P holds for a family of basic open sets covering U, then P holds for U.
                              3. There exists an affine open cover of X each satisfying P.

                              Then P holds for every affine open of X.

                              This is also known as the Affine communication lemma in The rising sea.

                              On a locally ringed space X, the preimage of the zero locus of the prime spectrum of Γ(X, ⊤) under toΓSpecFun agrees with the associated zero locus on X.

                              If X is affine, the image of the zero locus of global sections of X under toΓSpecFun is the zero locus in terms of the prime spectrum of Γ(X, ⊤).

                              theorem AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] (s : Set X.toPresheafedSpace) :
                              IsClosed s ∃ (I : Ideal (X.presheaf.obj (Opposite.op ))), s = X.zeroLocus I

                              If X is an affine scheme, every closed set of X is the zero locus of a set of global sections.

                              @[deprecated AlgebraicGeometry.IsAffineOpen.range_fromSpec]

                              Alias of AlgebraicGeometry.IsAffineOpen.range_fromSpec.

                              @[deprecated AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self]

                              Alias of AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self.

                              @[deprecated AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen']
                              theorem AlgebraicGeometry.IsAffineOpen.fromSpec_map_basicOpen' {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj (Opposite.op U))) :
                              (TopologicalSpace.Opens.map hU.fromSpec.val.base).obj (X.basicOpen f) = (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).basicOpen ((AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv f)

                              Alias of AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen'.

                              @[deprecated AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen]
                              theorem AlgebraicGeometry.IsAffineOpen.fromSpec_map_basicOpen {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (f : (X.presheaf.obj (Opposite.op U))) :
                              (TopologicalSpace.Opens.map hU.fromSpec.val.base).obj (X.basicOpen f) = PrimeSpectrum.basicOpen f

                              Alias of AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen.

                              @[deprecated AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen]

                              Alias of AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen.

                              @[deprecated AlgebraicGeometry.IsAffineOpen.basicOpen]

                              Alias of AlgebraicGeometry.IsAffineOpen.basicOpen.

                              @[deprecated AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage]

                              Alias of AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage.