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

            If f : A ⟶ B is a ring homomorphism, the corresponding arrow is isomorphic to the arrow of the morphism induced on global sections by the map on prime spectra.

            Equations
            • One or more equations did not get rendered due to their size.
            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 assumption.

                                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.

                                theorem AlgebraicGeometry.Scheme.toΓSpec_preimage_zeroLocus_eq {X : AlgebraicGeometry.Scheme} (s : Set (X.presheaf.obj (Opposite.op ))) :
                                X.toSpecΓ.val.base ⁻¹' PrimeSpectrum.zeroLocus s = X.zeroLocus s

                                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.

                                If X ⟶ Spec A is a morphism of schemes, then Spec of A ⧸ specTargetImage f is the scheme-theoretic image of f. For this quotient as an object of CommRingCat see specTargetImage below.

                                Equations
                                Instances For

                                  If X ⟶ Spec A is a morphism of schemes, then Spec of specTargetImage f is the scheme-theoretic image of f and f factors as specTargetImageFactorization f ≫ Spec.map (specTargetImageRingHom f) (see specTargetImageFactorization_comp).

                                  Equations
                                  Instances For

                                    If f : X ⟶ Spec A is a morphism of schemes, then f factors via the inclusion of Spec (specTargetImage f) into X.

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

                                      If f : X ⟶ Spec A is a morphism of schemes, the induced morphism on spectra of specTargetImageRingHom f is the inclusion of the scheme-theoretic image of f into Spec A.

                                      Equations
                                      Instances For

                                        The inclusion of the scheme-theoretic image of a morphism with affine target.

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

                                          Given a morphism of rings f : R ⟶ S, the stalk map of Spec S ⟶ Spec R at a prime of S is isomorphic to the localized ring homomorphism.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[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.