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 #

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
        @[simp]
        theorem AlgebraicGeometry.AffineScheme.mk_obj (X : Scheme) (x✝ : IsAffine X) :
        (mk X x✝).obj = X

        Construct an affine scheme from a scheme. Also see AffineScheme.mk for a non-typeclass version.

        Equations
        Instances For

          Type check a morphism of schemes as a morphism in AffineScheme.

          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

                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
                    noncomputable def AlgebraicGeometry.Scheme.Opens.toSpecΓ {X : Scheme} (U : X.Opens) :

                    The canonical map U ⟶ Spec Γ(X, U) for an open U ⊆ X.

                    Equations
                    Instances For

                      The isomorphism U ≅ Spec Γ(X, U) for an affine U.

                      Equations
                      Instances For
                        @[deprecated AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop (since := "2024-11-16")]

                        Alias of AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop.

                        @[deprecated AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop (since := "2024-11-16")]

                        Alias of AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop.

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

                        Equations
                        Instances For

                          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

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

                            Equations
                            Instances For
                              @[simp]
                              theorem AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le {X : Scheme} {U : X.Opens} (hU : 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
                              Equations
                              • One or more equations did not get rendered due to their size.

                              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

                                f.app (Y.basicOpen r) is isomorphic to map induced on localizations Γ(Y, Y.basicOpen r) ⟶ Γ(X, X.basicOpen (f.app U r))

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  theorem AlgebraicGeometry.exists_basicOpen_le_affine_inter {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {V : X.Opens} (hV : 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 : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (x : U) :

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

                                  Equations
                                  Instances For

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

                                    Equations
                                    Instances For
                                      theorem AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff {X : Scheme} {U : X.Opens} (hU : 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.

                                      The restriction of Spec.map f to a basic open D(r) is isomorphic to Spec.map of the localization of f away from r.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        theorem AlgebraicGeometry.iSup_basicOpen_of_span_eq_top {X : 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 : 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][RisingSea].

                                        On a scheme X, the preimage of the zero locus of the prime spectrum of Γ(X, ⊤) under X.toSpecΓ : X ⟶ Spec Γ(X, ⊤) agrees with the associated zero locus on X.

                                        @[deprecated AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus (since := "2025-01-17")]

                                        Alias of AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus.


                                        On a scheme X, the preimage of the zero locus of the prime spectrum of Γ(X, ⊤) under X.toSpecΓ : X ⟶ Spec Γ(X, ⊤) agrees with the associated zero locus on X.

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

                                        @[deprecated AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus (since := "2025-01-17")]

                                        Alias of AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus.


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

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

                                        theorem AlgebraicGeometry.Scheme.zeroLocus_inf (X : Scheme) {U : X.Opens} (I J : Ideal (X.presheaf.obj (Opposite.op U))) :
                                        X.zeroLocus ↑(I J) = X.zeroLocus I X.zeroLocus J
                                        theorem AlgebraicGeometry.Scheme.zeroLocus_biInf {X : Scheme} {U : X.Opens} {ι : Type u_1} (I : ιIdeal (X.presheaf.obj (Opposite.op U))) {t : Set ι} (ht : t.Finite) :
                                        X.zeroLocus (⨅ it, I i) = (⋃ it, X.zeroLocus (I i)) (↑U)
                                        theorem AlgebraicGeometry.Scheme.zeroLocus_biInf_of_nonempty {X : Scheme} {U : X.Opens} {ι : Type u_1} (I : ιIdeal (X.presheaf.obj (Opposite.op U))) {t : Set ι} (ht : t.Finite) (ht' : t.Nonempty) :
                                        X.zeroLocus (⨅ it, I i) = it, X.zeroLocus (I i)
                                        theorem AlgebraicGeometry.Scheme.zeroLocus_iInf {X : Scheme} {U : X.Opens} {ι : Type u_1} (I : ιIdeal (X.presheaf.obj (Opposite.op U))) [Finite ι] :
                                        X.zeroLocus (⨅ (i : ι), I i) = (⋃ (i : ι), X.zeroLocus (I i)) (↑U)
                                        theorem AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty {X : Scheme} {U : X.Opens} {ι : Type u_1} (I : ιIdeal (X.presheaf.obj (Opposite.op U))) [Finite ι] [Nonempty ι] :
                                        X.zeroLocus (⨅ (i : ι), I i) = ⋃ (i : ι), X.zeroLocus (I i)

                                        Given f : X ⟶ Spec A and some ideal I ≤ ker(A ⟶ Γ(X, ⊤)), this is the lift to X ⟶ Spec (A ⧸ I).

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

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

                                                    The induced morphism from X to the scheme-theoretic image of a morphism f : X ⟶ Y with affine target.

                                                    Equations
                                                    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