Documentation

Mathlib.AlgebraicGeometry.StructureSheaf

The structure sheaf on PrimeSpectrum R. #

We define the structure sheaf on TopCat.of (PrimeSpectrum R), for a commutative ring R and prove basic properties about it. We define this as a subsheaf of the sheaf of dependent functions into the localizations, cut out by the condition that the function must be locally equal to a ratio of elements of R.

Because the condition "is equal to a fraction" passes to smaller open subsets, the subset of functions satisfying this condition is automatically a subpresheaf. Because the condition "is locally equal to a fraction" is local, it is also a subsheaf.

(It may be helpful to refer back to Mathlib/Topology/Sheaves/SheafOfFunctions.lean, where we show that dependent functions into any type family form a sheaf, and also Mathlib/Topology/Sheaves/LocalPredicate.lean, where we characterise the predicates which pick out sub-presheaves and sub-sheaves of these sheaves.)

We also set up the ring structure, obtaining structureSheaf : Sheaf CommRingCat (PrimeSpectrum.Top R).

We then construct two basic isomorphisms, relating the structure sheaf to the underlying ring R. First, StructureSheaf.stalkIso gives an isomorphism between the stalk of the structure sheaf at a point p and the localization of R at the prime ideal p. Second, StructureSheaf.basicOpenIso gives an isomorphism between the structure sheaf on basicOpen f and the localization of R at the submonoid of powers of f.

References #

The prime spectrum, just as a topological space.

Equations
Instances For

    The type family over PrimeSpectrum R consisting of the localization over each point.

    Equations
    Instances For

      The predicate saying that a dependent function on an open U is realised as a fixed fraction r / s in each of the stalks (which are localizations at various prime ideals).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem AlgebraicGeometry.StructureSheaf.IsFraction.eq_mk' {R : Type u} [CommRing R] {U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)} {f : (x : U) → AlgebraicGeometry.StructureSheaf.Localizations R x} (hf : AlgebraicGeometry.StructureSheaf.IsFraction f) :
        ∃ (r : R) (s : R), ∀ (x : U), ∃ (hs : s(↑x).asIdeal), f x = IsLocalization.mk' (Localization.AtPrime (↑x).asIdeal) r s, hs

        The predicate IsFraction is "prelocal", in the sense that if it holds on U it holds on any open subset V of U.

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

          We will define the structure sheaf as the subsheaf of all dependent functions in Π x : U, Localizations R x consisting of those functions which can locally be expressed as a ratio of (the images in the localization of) elements of R.

          Quoting Hartshorne:

          For an open set $U ⊆ Spec A$, we define $𝒪(U)$ to be the set of functions $s : U → ⨆_{𝔭 ∈ U} A_𝔭$, such that $s(𝔭) ∈ A_𝔭$ for each $𝔭$, and such that $s$ is locally a quotient of elements of $A$: to be precise, we require that for each $𝔭 ∈ U$, there is a neighborhood $V$ of $𝔭$, contained in $U$, and elements $a, f ∈ A$, such that for each $𝔮 ∈ V, f ∉ 𝔮$, and $s(𝔮) = a/f$ in $A_𝔮$.

          Now Hartshorne had the disadvantage of not knowing about dependent functions, so we replace his circumlocution about functions into a disjoint union with Π x : U, Localizations x.

          Equations
          Instances For
            @[simp]
            theorem AlgebraicGeometry.StructureSheaf.isLocallyFraction_pred (R : Type u) [CommRing R] {U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)} (f : (x : U) → AlgebraicGeometry.StructureSheaf.Localizations R x) :
            (AlgebraicGeometry.StructureSheaf.isLocallyFraction R).pred f = ∀ (x : U), ∃ (V : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (_ : x V) (i : V U) (r : R) (s : R), ∀ (y : V), s(↑y).asIdeal f ((fun (x : V) => x, ) y) * (algebraMap R (AlgebraicGeometry.StructureSheaf.Localizations R ((fun (x : V) => x, ) y))) s = (algebraMap R (AlgebraicGeometry.StructureSheaf.Localizations R ((fun (x : V) => x, ) y))) r

            The functions satisfying isLocallyFraction form a subring.

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

              The structure presheaf, valued in CommRingCat, constructed by dressing up the Type valued structure presheaf.

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

                Some glue, verifying that the structure presheaf valued in CommRingCat agrees with the Type valued structure presheaf.

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

                  The structure sheaf on $Spec R$, valued in CommRingCat.

                  This is provided as a bundled SheafedSpace as Spec.SheafedSpace R later.

                  Equations
                  Instances For
                    @[simp]
                    theorem AlgebraicGeometry.StructureSheaf.res_apply (R : Type u) [CommRing R] (U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (V : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (i : V U) (s : ((AlgebraicGeometry.Spec.structureSheaf R).val.obj (Opposite.op U))) (x : V) :
                    (((AlgebraicGeometry.Spec.structureSheaf R).val.map i.op) s) x = s ((fun (x : V) => x, ) x)
                    def AlgebraicGeometry.StructureSheaf.const (R : Type u) [CommRing R] (f : R) (g : R) (U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (hu : xU, g x.asIdeal.primeCompl) :

                    The section of structureSheaf R on an open U sending each x ∈ U to the element f/g in the localization of R at x.

                    Equations
                    Instances For
                      @[simp]
                      theorem AlgebraicGeometry.StructureSheaf.const_apply (R : Type u) [CommRing R] (f : R) (g : R) (U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (hu : xU, g x.asIdeal.primeCompl) (x : U) :
                      theorem AlgebraicGeometry.StructureSheaf.const_apply' (R : Type u) [CommRing R] (f : R) (g : R) (U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (hu : xU, g x.asIdeal.primeCompl) (x : U) (hx : g (↑x).asIdeal.primeCompl) :
                      @[simp]
                      theorem AlgebraicGeometry.StructureSheaf.res_const (R : Type u) [CommRing R] (f : R) (g : R) (U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (hu : xU, g x.asIdeal.primeCompl) (V : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (hv : xV, g x.asIdeal.primeCompl) (i : Opposite.op U Opposite.op V) :
                      theorem AlgebraicGeometry.StructureSheaf.const_add (R : Type u) [CommRing R] (f₁ : R) (f₂ : R) (g₁ : R) (g₂ : R) (U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (hu₁ : xU, g₁ x.asIdeal.primeCompl) (hu₂ : xU, g₂ x.asIdeal.primeCompl) :
                      AlgebraicGeometry.StructureSheaf.const R f₁ g₁ U hu₁ + AlgebraicGeometry.StructureSheaf.const R f₂ g₂ U hu₂ = AlgebraicGeometry.StructureSheaf.const R (f₁ * g₂ + f₂ * g₁) (g₁ * g₂) U
                      theorem AlgebraicGeometry.StructureSheaf.const_mul (R : Type u) [CommRing R] (f₁ : R) (f₂ : R) (g₁ : R) (g₂ : R) (U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (hu₁ : xU, g₁ x.asIdeal.primeCompl) (hu₂ : xU, g₂ x.asIdeal.primeCompl) :
                      theorem AlgebraicGeometry.StructureSheaf.const_ext (R : Type u) [CommRing R] {f₁ : R} {f₂ : R} {g₁ : R} {g₂ : R} {U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)} {hu₁ : xU, g₁ x.asIdeal.primeCompl} {hu₂ : xU, g₂ x.asIdeal.primeCompl} (h : f₁ * g₂ = f₂ * g₁) :
                      theorem AlgebraicGeometry.StructureSheaf.const_congr (R : Type u) [CommRing R] {f₁ : R} {f₂ : R} {g₁ : R} {g₂ : R} {U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)} {hu : xU, g₁ x.asIdeal.primeCompl} (hf : f₁ = f₂) (hg : g₁ = g₂) :
                      theorem AlgebraicGeometry.StructureSheaf.const_mul_rev (R : Type u) [CommRing R] (f : R) (g : R) (U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (hu₁ : xU, g x.asIdeal.primeCompl) (hu₂ : xU, f x.asIdeal.primeCompl) :
                      theorem AlgebraicGeometry.StructureSheaf.const_mul_cancel (R : Type u) [CommRing R] (f : R) (g₁ : R) (g₂ : R) (U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (hu₁ : xU, g₁ x.asIdeal.primeCompl) (hu₂ : xU, g₂ x.asIdeal.primeCompl) :
                      theorem AlgebraicGeometry.StructureSheaf.const_mul_cancel' (R : Type u) [CommRing R] (f : R) (g₁ : R) (g₂ : R) (U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (hu₁ : xU, g₁ x.asIdeal.primeCompl) (hu₂ : xU, g₂ x.asIdeal.primeCompl) :

                      The canonical ring homomorphism interpreting an element of R as a section of the structure sheaf.

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

                        The canonical ring homomorphism interpreting an element of R as an element of the stalk of structureSheaf R at x.

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

                          The canonical ring homomorphism from the localization of R at p to the stalk of the structure sheaf at the point p.

                          Equations
                          Instances For

                            The ring homomorphism that takes a section of the structure sheaf of R on the open set U, implemented as a subtype of dependent functions to localizations at prime ideals, and evaluates the section on the point corresponding to a given prime ideal.

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

                              The ring homomorphism from the stalk of the structure sheaf of R at a point corresponding to a prime ideal p to the localization of R at p, formed by gluing the openToLocalization maps.

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

                                The ring isomorphism between the stalk of the structure sheaf of R at a point p corresponding to a prime ideal in R and the localization of R at p.

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

                                  The canonical ring homomorphism interpreting s ∈ R_f as a section of the structure sheaf on the basic open defined by f ∈ R.

                                  Equations
                                  Instances For
                                    theorem AlgebraicGeometry.StructureSheaf.normalize_finite_fraction_representation (R : Type u) [CommRing R] (U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (s : ((AlgebraicGeometry.Spec.structureSheaf R).val.obj (Opposite.op U))) {ι : Type u_1} (t : Finset ι) (a : ιR) (h : ιR) (iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) U) (h_cover : U it, PrimeSpectrum.basicOpen (h i)) (hs : ∀ (i : ι), AlgebraicGeometry.StructureSheaf.const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) = ((AlgebraicGeometry.Spec.structureSheaf R).val.map (iDh i).op) s) :
                                    ∃ (a' : ιR) (h' : ιR) (iDh' : (i : ι) → PrimeSpectrum.basicOpen (h' i) U), U it, PrimeSpectrum.basicOpen (h' i) (∀ it, jt, a' i * h' j = h' i * a' j) it, ((AlgebraicGeometry.Spec.structureSheaf R).val.map (iDh' i).op) s = AlgebraicGeometry.StructureSheaf.const R (a' i) (h' i) (PrimeSpectrum.basicOpen (h' i))

                                    The ring isomorphism between the structure sheaf on basicOpen f and the localization of R at the submonoid of powers of f.

                                    Equations
                                    Instances For

                                      Stalk of the structure sheaf at a prime p as localization of R

                                      Equations
                                      • =

                                      Sections of the structure sheaf of Spec R on a basic open as localization of R

                                      Equations
                                      • =

                                      Given a ring homomorphism f : R →+* S, an open set U of the prime spectrum of R and an open set V of the prime spectrum of S, such that V ⊆ (comap f) ⁻¹' U, we can push a section s on U to a section on V, by composing with Localization.localRingHom _ _ f from the left and comap f from the right. Explicitly, if s evaluates on comap f p to a / b, its image on V evaluates on p to f(a) / f(b).

                                      At the moment, we work with arbitrary dependent functions s : Π x : U, Localizations R x. Below, we prove the predicate isLocallyFraction is preserved by this map, hence it can be extended to a morphism between the structure sheaves of R and S.

                                      Equations
                                      Instances For

                                        For a ring homomorphism f : R →+* S and open sets U and V of the prime spectra of R and S such that V ⊆ (comap f) ⁻¹ U, the induced ring homomorphism from the structure sheaf of R at U to the structure sheaf of S at V.

                                        Explicitly, this map is given as follows: For a point p : V, if the section s evaluates on p to the fraction a / b, its image on V evaluates on p to the fraction f(a) / f(b).

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[simp]
                                          theorem AlgebraicGeometry.StructureSheaf.comap_apply {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (U : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top R)) (V : TopologicalSpace.Opens (AlgebraicGeometry.PrimeSpectrum.Top S)) (hUV : V.carrier (PrimeSpectrum.comap f) ⁻¹' U.carrier) (s : ((AlgebraicGeometry.Spec.structureSheaf R).val.obj (Opposite.op U))) (p : V) :
                                          ((AlgebraicGeometry.StructureSheaf.comap f U V hUV) s) p = (Localization.localRingHom ((PrimeSpectrum.comap f) p).asIdeal (↑p).asIdeal f ) (s (PrimeSpectrum.comap f) p, )

                                          For an inclusion i : V ⟶ U between open sets of the prime spectrum of R, the comap of the identity from OO_X(U) to OO_X(V) equals as the restriction map of the structure sheaf.

                                          This is a generalization of the fact that, for fixed U, the comap of the identity from OO_X(U) to OO_X(U) is the identity.

                                          The comap of the identity is the identity. In this variant of the lemma, two open subsets U and V are given as arguments, together with a proof that U = V. This is useful when U and V are not definitionally equal.